The traditional ground-and-solve approach to Answer Set programming (ASP) suffers from the grounding bottleneck, which makes large-scale problem instances unsolvable. Lazy grounding is an alternative approach that int...
详细信息
ISBN:
(纸本)9783030205287;9783030205270
The traditional ground-and-solve approach to Answer Set programming (ASP) suffers from the grounding bottleneck, which makes large-scale problem instances unsolvable. Lazy grounding is an alternative approach that interleaves grounding with solving and thus uses space more efficiently. The limited view on the search space in lazy grounding poses unique challenges, however, and can have adverse effects on solving performance. In this paper we present a novel characterization of degrees of laziness in grounding for ASP, i.e. of compromises between lazily grounding as little as possible and the traditional full grounding upfront. We investigate how these degrees of laziness compare to each other formally as well as, by means of an experimental analysis using a number of benchmarks, in terms of their effects on solving performance. Our contributions are the introduction of a range of novel lazy grounding strategies, a formal account on their relationships and their correctness, and an investigation of their effects on solving performance. Experiments show that our approach performs significantly better than state-of-the-art lazy grounding in many cases.
In this paper, we introduce novel algorithms to solve projected answer set counting (#PAs). #PAs asks to count the number of answer sets with respect to a given set of projection atoms, where multiple answer sets that...
详细信息
ISBN:
(纸本)9783030205287;9783030205270
In this paper, we introduce novel algorithms to solve projected answer set counting (#PAs). #PAs asks to count the number of answer sets with respect to a given set of projection atoms, where multiple answer sets that are identical when restricted to the projection atoms count as only one projected answer set. Our algorithms exploit small treewidth of the primal graph of the input instance by dynamic programming (DP). We establish a new algorithm for head-cycle-free (HCF) programs and lift very recent results from projected model counting to #PAs when the input is restricted to HCF programs. Further, we show how established DP algorithms for tight, normal, and disjunctive answer set programs can be extended to solve #PAs. Our algorithms run in polynomial time while requiring double exponential time in the treewidth for tight, normal, and HCF programs, and triple exponential time for disjunctive programs. Finally, we take the exponential time hypothesis (ETH) into account and establish lower bounds of bounded treewidth algorithms for #PAs. Under ETH, one cannot significantly improve our obtained worst-case runtimes.
This special issue of theory and practice of logic programming (TPLP) contains the regular papers accepted for presentation at the 34-th International Conference on logicprogramming (ICLP 2018), held in Oxford, Unite...
This special issue of theory and practice of logic programming (TPLP) contains the regular papers accepted for presentation at the 34-th International Conference on logicprogramming (ICLP 2018), held in Oxford, United Kingdom, from July 14th to July 17th, 2018.
We present a system of session types based on adjoint logic which generalize standard binary session types [14]. Our system allows us to uniformly capture several new behaviors in the space of asynchronous message-pas...
详细信息
We present a system of session types based on adjoint logic which generalize standard binary session types [14]. Our system allows us to uniformly capture several new behaviors in the space of asynchronous message-passing communication, including multicast, where a process sends a single message to multiple clients, replicable services, which have multiple clients and replicate themselves on-demand to handle requests from those clients, and cancellation, where a process discards a channel without communicating along it. We provide session fidelity and deadlock-freedom results for this system, from which we then derive a logically justified form of garbage collection.
Description logics (DLs) are well-known knowledge representation formalisms focused on the representation of terminological knowledge. Due to their first-order semantics, these languages (in their classical form) are ...
详细信息
The termination and complexity competition (termCOMP) focuses on automated termination and complexity analysis for various kinds of programming paradigms, including categories for term rewriting, integer transition sy...
详细信息
ISBN:
(纸本)9783030175023;9783030175016
The termination and complexity competition (termCOMP) focuses on automated termination and complexity analysis for various kinds of programming paradigms, including categories for term rewriting, integer transition systems, imperative programming, logicprogramming, and functional programming. In all categories, the competition also welcomes the participation of tools providing certifiable output. The goal of the competition is to demonstrate the power and advances of the state-of-the-art tools in each of these areas.
New generations of distributed systems are opening novel perspectives for logicprogramming (LP): On the one hand, service-oriented architectures represent nowadays the standard approach for distributed systems engine...
详细信息
New generations of distributed systems are opening novel perspectives for logicprogramming (LP): On the one hand, service-oriented architectures represent nowadays the standard approach for distributed systems engineering;on the other hand, pervasive systems mandate for situated intelligence. In this paper, we introduce the notion of logicprogramming as a Service (LPaaS) as a means to address the needs of pervasive intelligent systems through logic engines exploited as a distributed service. First, we define the abstract architectural model by re-interpreting classical LP notions in the new context;then we elaborate on the nature of LP interpreted as a service by describing the basic LPaaS interface. Finally, we show how LPaaS works in practice by discussing its implementation in terms of distributed tuProlog engines, accounting for basic issues such as interoperability and configurability.
This paper introduces a new categorical structure that is a model of a variant of the i/o-typed pi-calculus, in the same way that a cartesian closed category is a model of the lambda-calculus. To the best of our knowl...
详细信息
ISBN:
(纸本)9783030171841;9783030171834
This paper introduces a new categorical structure that is a model of a variant of the i/o-typed pi-calculus, in the same way that a cartesian closed category is a model of the lambda-calculus. To the best of our knowledge, no categorical model has been given for the i/o-typed pi-calculus, in contrast to session-typed calculi, to which corresponding logic and categorical structure were given. The categorical structure introduced in this paper has a simple definition, combining two well-known structures, namely, closed Freyd category and compact closed category. The former is a model of effectful computation in a general setting, and the latter describes connections via channels, which cause the effect we focus on in this paper. To demonstrate the relevance of the categorical model, we show by a semantic consideration that the pi-calculus is equivalent to a core calculus of Concurrent ML.
Concurrent and distributed programming is notoriously hard. Modern languages and toolkits ease this difficulty by offering message-passing abstractions, such as actors (e.g., Erlang, Akka, Orleans) or processes (e.g.,...
详细信息
ISBN:
(纸本)9781450367127
Concurrent and distributed programming is notoriously hard. Modern languages and toolkits ease this difficulty by offering message-passing abstractions, such as actors (e.g., Erlang, Akka, Orleans) or processes (e.g., Go): they allow for simpler reasoning w.r.t. shared-memory concurrency, but do not ensure that a program implements a given specification. To address this challenge, it would be desirable to specify and verify the intended behaviour of message-passing applications using types, and ensure that, if a program type-checks and compiles, then it will run and communicate as desired. We develop this idea in theory and practice. We formalise a concurrent functional language lambda(pi)(<=), with a new blend of behavioural types (from pi-calculus theory), and dependent function types (from the Dotty programming language, a.k.a. the future Scala 3). Our theory yields four main payoffs: (1) it verifies safety and liveness properties of programs via types-level model checking;(2) unlike previous work, it accurately verifies channel-passing (covering a typical pattern of actor programs) and higher-order interaction (i.e., sending/receiving mobile code);(3) it is directly embedded in Dotty, as a toolkit called Effpi, offering a simplified actor-based API;(4) it enables an efficient runtime system for Effpi, for highly concurrent programs with millions of processes/actors.
We propose an interpretation of the first-order answer set programming (FOASP) in terms of intuitionistic proof theory. It is obtained by two polynomial translations between FOASP and the bounded-arity fragment of the...
详细信息
We propose an interpretation of the first-order answer set programming (FOASP) in terms of intuitionistic proof theory. It is obtained by two polynomial translations between FOASP and the bounded-arity fragment of the Sigma(1) level of the Mints hierarchy in first-order intuitionistic logic. It follows that Sigma(1) formulas using predicates of fixed arity (in particular unary) is of the same strength as FOASP. Our construction reveals a close similarity between constructive provability and stable entailment, or equivalently, between the construction of an answer set and an intuitionistic refutation. This paper is under consideration for publication in theory and practice of logic programming.
暂无评论