In this note, we introduce the notion of support graph to define explanations for any model of a logic program. An explanation is an acyclic support graph that, for each true atom in the model, induces a proof in term...
详细信息
In this note, we introduce the notion of support graph to define explanations for any model of a logic program. An explanation is an acyclic support graph that, for each true atom in the model, induces a proof in terms of program rules represented by labels. A classical model may have zero, one or several explanations: when it has at least one, it is called a justified model. We prove that all stable models are justified, whereas, for disjunctive programs, some justified models may not be stable. We also provide a meta-programming encoding in Answer Set programming that generates the explanations for a given stable model of some program. We prove that the encoding is sound and complete, that is, there is a one-to-one correspondence between each answer set of the encoding and each explanation for the original stable model.
We present the Answer Set programming (ASP)-based visualization tool clingraph, which aims at visualizing various concepts of ASP by means of ASP itself. This idea traces back to the aspviz tool and clingraph redevelo...
详细信息
We present the Answer Set programming (ASP)-based visualization tool clingraph, which aims at visualizing various concepts of ASP by means of ASP itself. This idea traces back to the aspviz tool and clingraph redevelops and extends it in the context of modern ASP systems. More precisely, clingraph takes graph specifications in terms of ASP facts and hands them over to the graph visualization system graphviz. The use of ASP provides a great interface between logic programs and/or answer sets and their visualization. Also, clingraph offers a Python application programming interface (API) that extends this ease of interfacing to clingo's API and in turn to connect and monitor various aspects of the solving process.
Solving a decision theory problem usually involves finding the actions, among a set of possible ones, which optimize the expected reward, while possibly accounting for the uncertainty of the environment. In this paper...
详细信息
Solving a decision theory problem usually involves finding the actions, among a set of possible ones, which optimize the expected reward, while possibly accounting for the uncertainty of the environment. In this paper, we introduce the possibility to encode decision theory problems with Probabilistic Answer Set programming under the credal semantics via decision atoms and utility attributes. To solve the task, we propose an algorithm based on three layers of Algebraic Model Counting, that we test on several synthetic datasets against an algorithm that adopts answer set enumeration. Empirical results show that our algorithm can manage non-trivial instances of programs in a reasonable amount of time.
Answer set programming is a declarative logicprogramming paradigm geared towards solving difficult combinatorial search problems. While different logic programs can encode the same problem, their performance may vary...
详细信息
Answer set programming is a declarative logicprogramming paradigm geared towards solving difficult combinatorial search problems. While different logic programs can encode the same problem, their performance may vary significantly. It is not always easy to identify which version of the program performs the best. We present the system Predictor (and its algorithmic backend) for estimating the grounding size of programs, a metric that can influence a performance of a system processing a program. We evaluate the impact of Predictor when used as a guide for rewritings produced by the answer set programming rewriting tools Projector and Lpopt. The results demonstrate potential to this approach.
When we want to compute the probability of a query from a probabilistic answer set program, some parts of a program may not influence the probability of a query, but they impact on the size of the grounding. Identifyi...
详细信息
When we want to compute the probability of a query from a probabilistic answer set program, some parts of a program may not influence the probability of a query, but they impact on the size of the grounding. Identifying and removing them is crucial to speed up the computation. Algorithms for SLG resolution offer the possibility of returning the residual program which can be used for computing answer sets for normal programs that do have a total well-founded model. The residual program does not contain the parts of the program that do not influence the probability. In this paper, we propose to exploit the residual program for performing inference. Empirical results on graph datasets show that the approach leads to significantly faster inference. The paper has been accepted at the ICLP2024 conference and under consideration in theory and practice of logic programming (TPLP).
Formal reasoning about finite sets and cardinality is important for many applications. including software verification, where very often one needs to reason about the size of a given data structure. The Constraint Log...
详细信息
Formal reasoning about finite sets and cardinality is important for many applications. including software verification, where very often one needs to reason about the size of a given data structure. The Constraint logicprogramming tool {log} provides a decision procedure for deciding the satisfiability of formulas involving very general forms of finite sets, although it does not provide cardinality constraints. In this paper we adapt and integrate a decision procedure for a theory of finite sets with cardinality into {log}. The proposed solver is proved to be a decision procedure for its formulas. Besides, the new CLP instance is implemented as part of the {log} tool. In turn, the implementation uses Howe and King's Prolog SAT solver and Prolog's CLP(Q) library. as an integer linear programming solver. The empirical evaluation of this implementation based on +250 real verification conditions shows that it can be useful in practice.
In previous work, summarized in this paper, we proposed an operation of parallel composition for rewriting-logic theories, allowing compositional specification of systems and reusability of components. The present pap...
详细信息
In previous work, summarized in this paper, we proposed an operation of parallel composition for rewriting-logic theories, allowing compositional specification of systems and reusability of components. The present paper focuses on compositional verification. We show how the assume/guarantee technique can be transposed to our setting, by giving appropriate definitions of satisfaction based on transition structures and path semantics. We also show that simulation and equational abstraction can be done componentwise. Appropriate concepts of fairness and deadlock for our composition operation are discussed, as they affect satisfaction of temporal formulas. We keep in parallel a distributed and a global view of composed systems. We show that these views are equivalent and interchangeable, which may help our intuition and also has practical uses as, for example, it allows global-style verification of a modularly specified system. Under consideration in theory and practice of logic programming (TPLP).
In temporal extensions of answer set programming (ASP) based on linear time, the behavior of dynamic systems is captured by sequences of states. While this representation reflects their relative order, it abstracts aw...
详细信息
In temporal extensions of answer set programming (ASP) based on linear time, the behavior of dynamic systems is captured by sequences of states. While this representation reflects their relative order, it abstracts away the specific times associated with each state. However, timing constraints are important in many applications like, for instance, when planning and scheduling go hand in hand. We address this by developing a metric extension of linear-time temporal equilibrium logic, in which temporal operators are constrained by intervals over natural numbers. The resulting Metric Equilibrium logic (MEL) provides the foundation of an ASP-based approach for specifying qualitative and quantitative dynamic constraints. To this end, we define a translation of metric formulas into monadic first-order formulas and give a correspondence between their models in MEL and Monadic Quantified Equilibrium logic, respectively. Interestingly, our translation provides a blue print for implementation in terms of ASP modulo difference constraints.
Parameter learning is a crucial task in the field of Statistical Relational Artificial Intelligence: given a probabilistic logic program and a set of observations in the form of interpretations, the goal is to learn t...
详细信息
Parameter learning is a crucial task in the field of Statistical Relational Artificial Intelligence: given a probabilistic logic program and a set of observations in the form of interpretations, the goal is to learn the probabilities of the facts in the program such that the probabilities of the interpretations are maximized. In this paper, we propose two algorithms to solve such a task within the formalism of Probabilistic Answer Set programming, both based on the extraction of symbolic equations representing the probabilities of the interpretations. The first solves the task using an off-the-shelf constrained optimization solver while the second is based on an implementation of the Expectation Maximization algorithm. Empirical results show that our proposals often outperform existing approaches based on projected answer set enumeration in terms of quality of the solution and in terms of execution time.
theory of stable models is the mathematical basis of answer set programming. Several results in that theory refer to the concept of the positive dependency graph of a logic program. We describe a modification of that ...
详细信息
theory of stable models is the mathematical basis of answer set programming. Several results in that theory refer to the concept of the positive dependency graph of a logic program. We describe a modification of that concept and show that the new understanding of positive dependency makes it possible to strengthen some of these results.
暂无评论