Answer set programming (ASP) has demonstrated its potential as an effective tool for concisely representing and reasoning about real-world problems. In this paper, we present an application in which ASP has been succe...
详细信息
Answer set programming (ASP) has demonstrated its potential as an effective tool for concisely representing and reasoning about real-world problems. In this paper, we present an application in which ASP has been successfully used in the context of dynamic traffic distribution for urban networks, within a more general framework devised for solving such a real-world problem. In particular, ASP has been employed for the computation of the "optimal" routes for all the vehicles in the network. We also provide an empirical analysis of the performance of the whole framework, and of its part in which ASP is employed, on two European urban areas, which shows the viability of the framework and the contribution ASP can give.
Tau Prolog is a client-side Prolog interpreter fully implemented in JavaScript, which aims at implementing the ISO Prolog Standard. Tau Prolog has been developed to be used with either *** or a browser seamlessly, and...
详细信息
Tau Prolog is a client-side Prolog interpreter fully implemented in JavaScript, which aims at implementing the ISO Prolog Standard. Tau Prolog has been developed to be used with either *** or a browser seamlessly, and therefore, it has been developed following a non-blocking, callback-based approach to avoid blocking web browsers. Taking the best from JavaScript and Prolog, Tau Prolog allows the programmer to handle browser events and manipulate the Document Object Model (DOM) of a web using Prolog predicates. In this paper we describe the architecture of Tau Prolog and its main packages for interacting with the Web, and we present its programming environment.
Answer set programming (ASP), a well-known declarative logicprogramming paradigm, has recently found practical application in Process Mining. In particular, ASP has been used to model tasks involving declarative spec...
详细信息
Answer set programming (ASP), a well-known declarative logicprogramming paradigm, has recently found practical application in Process Mining. In particular, ASP has been used to model tasks involving declarative specifications of business processes. In this area, Declare stands out as the most widely adopted declarative process modeling language, offering a means to model processes through sets of constraints valid traces must satisfy, that can be expressed in linear temporal logic over finite traces (LTL$_{\text {f}}$). Existing ASP-based solutions encode Declare constraints by modeling the corresponding LTL$_{\text {f}}$ formula or its equivalent automaton which can be obtained using established techniques. In this paper, we introduce a novel encoding for Declare constraints that directly models their semantics as ASP rules, eliminating the need for intermediate representations. We assess the effectiveness of this novel approach on two Process Mining tasks by comparing it with alternative ASP encodings and a Python library for Declare.
Approximation fixpoint theory (AFT) is an abstract and general algebraic framework for studying the semantics of non-monotonic logics. In recent work, AFT was generalized to non-deterministic operators, that is, opera...
详细信息
Approximation fixpoint theory (AFT) is an abstract and general algebraic framework for studying the semantics of non-monotonic logics. In recent work, AFT was generalized to non-deterministic operators, that is, operators whose range are sets of elements rather than single elements. In this paper, we make three further contributions to non-deterministic AFT: (1) we define and study ultimate approximations of non-deterministic operators, (2) we give an algebraic formulation of the semi-equilibrium semantics by Amendola et al., and (3) we generalize the characterizations of disjunctive logic programs to disjunctive logic programs with aggregates.
Many inductive logicprogramming (ILP) methods are incapable of learning programs from probabilistic background knowledge, for example, coming from sensory data or neural networks with probabilities. We propose Proppe...
详细信息
Many inductive logicprogramming (ILP) methods are incapable of learning programs from probabilistic background knowledge, for example, coming from sensory data or neural networks with probabilities. We propose Propper, which handles flawed and probabilistic background knowledge by extending ILP with a combination of neurosymbolic inference, a continuous criterion for hypothesis selection (binary cross-entropy) and a relaxation of the hypothesis constrainer (NoisyCombo). For relational patterns in noisy images, Propper can learn programs from as few as 8 examples. It outperforms binary ILP and statistical models such as a graph neural network.
We provide a comprehensive elaboration of the theoretical foundations of variable instantiation, or grounding, in Answer Set programming (ASP). Building on the semantics of ASP's modeling language, we introduce a ...
详细信息
We provide a comprehensive elaboration of the theoretical foundations of variable instantiation, or grounding, in Answer Set programming (ASP). Building on the semantics of ASP's modeling language, we introduce a formal characterization of grounding algorithms in terms of (fixed point) operators. A major role is played by dedicated well-founded operators whose associated models provide semantic guidance for delineating the result of grounding along with on-the-fly simplifications. We address an expressive class of logic programs that incorporates recursive aggregates and thus amounts to the scope of existing ASP modeling languages. This is accompanied with a plain algorithmic framework detailing the grounding of recursive aggregates. The given algorithms correspond essentially to the ones used in the ASP grounder gringo.
Property-based testing (PBT) is a technique for validating code against an executable specification by automatically generating test-data. We present a proof-theoretical reconstruction of this style of testing for rel...
详细信息
Property-based testing (PBT) is a technique for validating code against an executable specification by automatically generating test-data. We present a proof-theoretical reconstruction of this style of testing for relational specifications and employ the Foundational Proof Certificate framework to describe test generators. We do this by encoding certain kinds of "proof outlines" as proof certificates that can describe various common generation strategies in the PBT literature, ranging from random to exhaustive, including their combination. We also address the shrinking of counterexamples as a first step toward their explanation. Once generation is accomplished, the testing phase is a standard logic programing search. After illustrating our techniques on simple, first-order (algebraic) data structures, we lift it to data structures containing bindings by using the lambda-tree syntax approach to encode bindings. The lambda Prolog programing language can perform both generating and checking of tests using this approach to syntax. We then further extend PBT to specifications in a fragment of linear logic.
We propose a stable model semantics for higher-order logic programs. Our semantics is developed using Approximation Fixpoint theory (AFT), a powerful formalism that has successfully been used to give meaning to divers...
详细信息
We propose a stable model semantics for higher-order logic programs. Our semantics is developed using Approximation Fixpoint theory (AFT), a powerful formalism that has successfully been used to give meaning to diverse non-monotonic formalisms. The proposed semantics generalizes the classical two-valued stable model semantics of Gelfond and Lifschitz as well as the three-valued one of Przymusinski, retaining their desirable properties. Due to the use of AFT, we also get for free alternative semantics for higher-order logic programs, namely supported model, Kripke-Kleene, and well-founded. Additionally, we define a broad class of stratified higher-order logic programs and demonstrate that they have a unique two-valued higher-order stable model which coincides with the well-founded semantics of such programs. We provide a number of examples in different application domains, which demonstrate that higher-order logicprogramming under the stable model semantics is a powerful and versatile formalism, which can potentially form the basis of novel ASP systems.
Refactoring is modifying a program without changing its external behavior. In this paper, we make the concept of external behavior precise for a simple answer set programming language. Then we describe a proof assista...
详细信息
Refactoring is modifying a program without changing its external behavior. In this paper, we make the concept of external behavior precise for a simple answer set programming language. Then we describe a proof assistant for the task of verifying that refactoring a program in that language is performed correctly.
暂无评论