Published: 12th September 2023 DOI: 10.4204/EPTCS.385 ISSN: 2075-2180 |
The International Conference on Logic Programming (ICLP) is the premiere international scientific venue for presenting, discussing, and disseminating fundamental and applied research in the field of logic programming and in related interdisciplinary areas. The conference was launched in 1982, with its first edition in Marseille, France, and continues to serve the broad international logic programming community.
ICLP 2023 was a special edition of the conference as it represented the closing event of the "Year of Prolog" a year-long celebration of the 50th anniversary of the introduction of the Prolog programming language. The conference included a dedicated session to discuss the achievements accomplished throughout the year and the assignment of the 2023 Alan Colmerauer Prize, as well as an event on "Teaching Prolog: the Next 50 Years."
ICLP 2023 also included an Industry Event, with the participation of representatives of several for-profit organizations engaged in the use of logic programming technologies. The event consisted of a panel discussion on the role of symbolic AI in today's AI industrial landscape. The Conference featured Invited Speakers: Marco Maratea (University of Calabria, Italy), presenting on applications of answer set programming; Jan Wielemaker (Centrum Wiskunde & Informatica, The Netherlands), presenting on the rise, fall, and future of Prolog; Keith Stenning (The University of Edinburgh, Scotland) for the special track on Logic Programming and Machine Learning; Gopal Gupta (University of Texas at Dallas, USA) for the special track on Logic Programming and Explainability, Ethics and Trustworthiness; Mehul Bhatt (Orebro University, Sweden), tutorialist speaking on Cognitive Vision; and Joseph Townsend (Fujitsu Research of Europe, UK), tutorialist speaking on medical applications of neuro symbolic AI.
TCs also include accepted short papers, summaries of system presentations, and accepted extended abstracts from the Recently Published Research Track. In particular: 26 papers have been accepted for regular TC publication; 5 papers have been accepted as short papers in the TC category; 8 papers have been accepted as system demonstrations. In addition, we received and accepted 11 abstracts for the Recently Published Research track. All of them received an allocation of time in the conference program for presentation. In order to foster the engagement of students and their precious contribution to the research community, ICLP also hosted a doctoral consortium with 9 accepted submissions, two of which by women. A mentoring lunch event with a dedicated panel session were specifically held in order to facilitate exchange of ideas and networking.
ICLP 2023 gratefully received generous funding from the following sponsors.
In this extended abstract we report about new results about reasoning on weighted knowledge bases for Description Logics (DLs) with typicality under a ``concept-wise'' multi-preferential semantics, which have been shown to provide a logical interpretation of MultiLayer Perceptrons [18]. In particular, we provided a completeness result for the complexity of the problem, and new Answer Set Programming encodings in the same complexity class, that are shown to be able to deal with weighted knowledge bases with large search spaces. A detailed description in available in the full paper [1].
Description logics are widely used for knowledge representation, often to verify and discover properties of individuals in a concept by means of DLs inference services [2, 22]. Many properties of real world concepts, however, are defeasible, that is, they are not universally true, but have exceptions, and actually hold only for some prototypical individuals in the concept. This led to research on defeasible DLs [8,15,10,16]. Specifically, to represent the defeasible properties of a concept, DLs have been extended with a typicality operator $\bf{T}$ that is applied to concepts to obtain typicality inclusions of the form ${\bf{T}}(C) \sqsubseteq D$ [15,16}]. Intuitively, ${\bf{T}}(C) \sqsubseteq D$ means that the typical individuals in the concept $C$ also belong to concept $D$ (that, normally C's are D's), and corresponds to a conditional implication $C {\mathrel{{\scriptstyle\mid\!\sim}}} D$ in KLM preferential logics [24, 25]. From the semantic point of view a preference relation is considered as in KLM preferential semantics, to select the most typical individuals in a class (concept). A (conditional) knowledge base (KB) comprising typicality inclusions enables defeasible reasoning, as in fact properties holding for typical individuals in $C$ are not necessarily enforced on all individuals in $C$.
Based on the idea that each concept $C$ can be associated a set of prototypical properties, ranked DL knowledge bases [17] --- reminiscent of ranked KBs by Brewka [6] --- and weighted DL KBs with typicality [18] have been proposed. In particular, in weighted knowledge bases, a set ${\cal T}_C$ of weighted typicality inclusions $({\bf{T}}(C) \sqsubseteq D_1, \ w_1),$ $\ldots,$ $( {\bf{T}}(C) \sqsubseteq D_k, \ w_k)$ is associated to a concept $C$ to describe the prototypical properties of C-elements. For each property, the associated weight $w_i$ is a real number, representing the plausibility/implausibility of the property $D_i$ for $C$-elements.
Semantically, these formalisms have led to a concept-wise multi-preferential semantics, as the relative typicality of two domain individuals usually depends on the aspects we are considering for comparison [20, 17]: Bob may be a more typical as sport lover than Jim ($\mathit{bob <_{SportLover} jim}$), but Jim may be a more typical than Bob as a swimmer ($\mathit{jim <_{Swimmer} bob}$). It has been proven that this semantics has interesting properties in both the two-valued and in the fuzzy case (e.g., it is able to deal with specificity, irrelevance and satisfies the KLM properties).
The concept-wise multi-preferential semantics has been used to provide a logical interpretation to some neural network models, such as Self-Organising Maps [23], psychologically and biologically plausible neural network models, and for MultiLayer Perceptrons (MLPs) [21]. In both cases, a preferential interpretation can be constructed from a trained network (see [14] and [18]) and exploited for verification of typicality properties of the network through model checking. For MLPs a trained network can as well be regarded as a weighted knowledge base by encoding synaptic connections as weighted typicality inclusions under a fuzzy semantics [18, 13]. This concrete application and the widespread interest in neural networks strongly motivates the development of proof methods for reasoning with weighted KBs.
Entailment for fuzzy DLs is in general undecidable [11,4], and this motivates the investigation of many-valued approximations of fuzzy multi-preferential entailment. In particular, the finitely many-valued case is widely studied [12,3,5], and has been recently considered in the context of weighted DL KBs [19] by means of the notions of coherent, faithful and $\varphi$-coherent models of such KBs, previously considered in the fuzzy case [18, 13]. A proof-of-concept implementation in Answer Set Programming (ASP) and asprin [7] has been provided for the $\cal{LC}$ fragment of $\cal{ALC}$, which is obtained by disabling roles, and universal and existential restrictions. The approach adopts Gödel (alternatively, Łukasiewicz) connectives and addresses $\varphi$-coherent entailment, a form of defeasible reasoning based on canonical $\varphi$-coherent models. The $\varphi$-coherence condition makes weighted KBs correspond to MLPs with $\varphi$ as activation function; here a finitely many-valued approximation of such a function is used. As concerns the complexity of the problem, a $\Pi^p_2$ upper bound was given [19], but the exact complexity was unknown.
We briefly describe here two significant advancements with respect to the earlier work [19], from a theoretical point of view and on the practical side, for the $\varphi$-coherent entailment of typicality inclusions [1]. The complexity upper bound can be improved to ${ P}^{ NP[log]}$ by showing an algorithm running in polynomial time and performing parallel queries to an NP oracle ($ P^{||NP}$). As $ P^{||NP}$ is known to coincide with $ P^{NP[log]}$ [9], while $\Pi^p_2 = P^{NP[log]}$ is unlikely to hold (unless the polynomial hierarchy collapses to $ P^{NP[log]}$), there was space for improving the proof-of-concept implementation.
Different ASP encodings have been considered. For the enforcement of $\varphi$-coherence (where grounding explosion should be avoided) the best results are obtained using weight constraints. Weak constraints are used to encode the preferential semantics, relying on an order encoding to stay in the $P^{NP[log]}$ class. Further improvements at an asymptotic level are unlikely, as the problem is shown to be ${ P}^{ NP[log]}$-complete by giving a polynomial-time reduction of the MAX SAT ODD problem [26], which amounts to determining whether the maximum number of jointly satisfiable clauses among a given set is an odd number.
The scalability of the ASP encodings has been assessed empirically on defeasible entailment queries over synthetic weighted DL KBs to show that the redesigned ASP encoding can go beyond the small KBs and search spaces processable by the earlier proof-of-concept implementation [1].
This work was partially supported by GNCS-INdAM. Mario Alviano was partially supported by Italian Ministry of Research (MUR) under PNRR project FAIR ``Future AI Research'', CUP H23C22000860006 and by the LAIA lab (part of the SILA labs).
Abstract interpretation [3] allows constructing sound program analysis tools which can extract properties of a program by safely approximating its semantics. Static analysis tools are a crucial component of the development environments for many programming languages. Abstract interpretation proved practical and effective in the context of (Constraint) Logic Programming ((C)LP) [15,12,14,13,1,10,9] which was one of its first application areas (see[6]), and the techniques developed in this context have also been applied to the analysis and verification of other programming paradigms by using semantic translation to Horn Clauses (see the recent survey [4]). Unfortunately, the implementation of (sound, precise, efficient) abstract domains usually requires coding from scratch a large number of domain-related operations. Moreover, due to undecidability, a loss of precision is inevitable, which makes the design (and implementation) of more domains, as well as their combinations, eventually necessary to successfully prove arbitrary program properties. In this paper we focus on the latter problem by proposing a rule-based methodology for the design and rapid prototyping of new domains for logic programs, as well as composing and combining existing ones. Our techniques are inspired by those used in logic-based languages for implementing constraint domains at different abstraction levels.
Proposal. The construction of analyses based on abstract interpretation requires the defintion of some basic domain operations ($\subseteq$,$\sqcap$,$\sqcup$ and, optionally, the widening $\nabla$ operator); the abstract semantics of the primitive constraints (representing the built-ins, or basic operations of the source language) via transfer functions ($f(\alpha)$); and possibly some other additional instrumental operations over abstract substitutions. In addition, the classical top-down analysis approach requires a number of additional definitions of derived operations used by the analysis framework to implement procedure call, return, recursion, etc. Detailed descriptions of all these operations can be found in[12,11,2,7,5]. We propose a rule language inspired in rewriting to derive, script, and combine abstract domains. The objective is to reduce the time and effort required to write new abstract domains, both from scratch and as combinations of other domains
The proposed rule-based language. Given $s+1$ sets of constraints, $\mathcal{L}, \mathcal{C}_{1},\ldots, \mathcal{C}_{s}$, we define $AND(\mathcal{L}, \mathcal{C}_{1},\ldots, \mathcal{C}_{s})$ as the set of rules of the form $l_{1},\dots,l_{n} \,\, | \,\, g_{1},\ldots,g_{l} \,\, \Rightarrow \,\, r_{1},\ldots,r_{m} \,\, \# \,\, label$, where $s$, $n$, $m$, and $l$ are arbitrary positive integers, and the rule meets the following condition: \begin{equation*} \forall i, j, k \text{ s.t. } i \in \{1,\ldots,n\}, j \in \{1,\ldots,m\} \text{ and } k \in \{1,\ldots,l\} : (l_{i}, r_{j} \in \mathcal{L} \text{ and } \exists u \in \{1,\ldots,s\} \text{ s.t. } g_{k} \in \mathcal{C}_{u}) \end{equation*} The elements $l_{1},\dots,l_{n}$ constitute the left side of the rule; $r_{1},\ldots,r_{m}$ the right side; and $g_{1},\ldots,g_{l}$ the guards. Given $t+s$ sets of constraints $\mathcal{L}_{1}, \ldots, \mathcal{L}_{t}, \mathcal{C}_{1}, \ldots, \mathcal{C}_{s}$ such that $\forall v \in \{1,\ldots,t\} : \mathcal{L}_{v} \subseteq \mathcal{L}$, we define $OR(\mathcal{L}, \mathcal{C}_{1}, \ldots, \mathcal{C}_{n})$ as the set of rules of the form $ l_{1};\ldots;l_{n} \,\, | \,\, g_{1},\dots,g_{l} \,\, \Rightarrow \,\, r_{1},\ldots,r_{m} \,\, \# \,\, label$, where $s$, $t$, $n$, $m$, and $l$ are arbitrary positive integers, and the rule meets the following condition: $ \begin{array}{ll} \forall i, j, k & \text{ s.t. } i \in \{1,\ldots,n\}, j \in \{1,\ldots,m\} \text{ and } k \in \{1,\ldots,l\} : \\ % & \exists v \in \{1,\ldots,t\} \: \exists u \in \{1,\ldots,s\} % : \text{ s.t. } (l_{i} \in \mathcal{L}_{v}, r_{j} \in \mathcal{L} \text{ and } g_{k} \in \mathcal{C}_{u}) \end{array} $
Notice that while in $\mathit{AND}$-rules all the elements $l_{i}$ belong to the same set of constraints $\mathcal{L}$ in the $\mathit{OR}$-rules they belong to (possibly) different subsets of a set of constraints $\mathcal{L}$. The operational meaning of $\mathit{AND}$-rules is similar to that of rewriting rules. If the left side holds in the set where the rule is being applied to, and the guards also hold, then the left-side elements are replaced by the right-side elements. The operational meaning of $\mathit{OR}$-rules is similar, but instead of rewriting over the "same" set the right-side elements are written in a "new" set. When no more rules can be applied, different strategies can be followed. In general we can rewrite the pending elements to a given element or simply delete them.
In the context of abstract interpretation the sets of constraints that we have mentioned have to be seen as abstract domains being the rules applied then over abstract substitutions/constraints. AND-rules are intended to capture the behaviour of operations over one abstract substitution with the knowledge that can be inferred from other substitutions that meet the guards. This is useful for example when defining the greatest lower bound. Moreover, these rules are also useful for refining abstract substitutions, performing abstractions, combining different abstract domains, etc. On the other hand, OR-rules are intended to capture the behaviour of operations applied over multiple abstract substitutions of an abstract domain, such as the least upper bound or the widening.
partition([], _, [], []).
partition([E|R], C, Left, [E|Right1]) :-
E >= C,
partition(R, C, Left, Right1).
partition([E|R], C, [E|Left1], Right) :-
E < C,
partition(R, C, Left,1 Right).
An example. Fig.1 shows a classic Prolog predicate for partitioning a list. A call partition(L, X, L1, L2) is expected to satisfy some properties; for example, that $\forall v \in L2, X \leq v$, which we can express as inf(L2, X). With the help of two auxiliary domains to deal with structures containing variables and with constraints (resp. $\mathit{depth-k}$ and $\mathit{polyhedra}$) we can derive an abstract domain for the inf/2 property. A subset of the rules can be seen in Fig.2. These rules allow, when connected with the abstract domain operations, to exploit the information gathered from the previous domains and use it to infer inf(L2, X). Similarly, we can also capture the equivalent sup(L1, X), or multiset properties capturing that $L \subseteq L1 \cup L2$ and $L1 \cup L2 \subseteq L$. Moreover, we can infer the sortedness property for the classical quicksort implementation.
Conclusions & future work. We have presented a framework for simplifying the development of abstract domains for logic programs in the context of abstract interpretation frameworks, and concretely that ofCiaoPP. While some domains are easier to specify with a rule-based language, keeping a constraint-based representation for abstract substitutions may not be efficient compared with specialized representations and operations. In this respect, we plan to explore as future work the use of rules both as an input language for abstract domain compilation and as a specification language for debugging or verifying properties of hand-written domains. In our experience so far, the proposed approach seems promising for prototyping and experimenting with new domains, enhancing the precision for particular programs, and adding domain combination rules, without the need for understanding the analysis framework internals.
[1]M.García de la Banda, M.Hermenegildo, M.Bruynooghe, V.Dumortier, G.Janssens & W.Simoens (1996): Global Analysis of Constraint Logic Programs. ACM Transactions on Programming Languages and Systems 18(5), pp. 564−615.
[2]M.Bruynooghe (1991): A Practical Framework for the Abstract Interpretation of Logic Programs. Journal of Logic Programming 10, pp. 91 −124.
[3]P.Cousot & R.Cousot (1977): Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In: ACM Symposium on Principles of Programming Languages (POPL'77), ACM Press, pp. 238−252, doi:10.1145/512950.512973.
[4]Emanuele De Angelis, Fabio Fioravanti, JohnP. Gallagher, ManuelV. Hermenegildo, Alberto Pettorossi & Maurizio Proietti (2021): Analysis and Transformation of Constrained Horn Clauses for Program Verification. Theory and Practice of Logic Programming FirstView, pp. 1−69, doi:10.1017/S1471068421000211. Available at http://arxiv.org/abs/2108.00739.
[5]I.Garcia-Contreras, J.F. Morales & M.V. Hermenegildo (2021): Incremental and Modular Context-sensitive Analysis. Theory and Practice of Logic Programming 21(2), pp. 196−243, doi:10.1017/S1471068420000496. Available at https://arxiv.org/abs/1804.01839.
[6]R.Giacobazzi & F.Ranzato (2022): History of Abstract Interpretation. IEEE Ann. Hist. Comput. 44(2), pp. 33−43. Available at https://doi.org/10.1109/MAHC.2021.3133136.
[7]M.V. Hermenegildo, G.Puebla, K.Marriott & P.Stuckey (2000): Incremental Analysis of Constraint Logic Programs. ACM Transactions on Programming Languages and Systems 22(2), pp. 187−223.
[8]D.Jurjo, J.F. Morales, P.Lopez-Garcia & M.V. Hermenegildo (2022): A Rule-based Approach for Designing and Composing Abstract Domains. Technical Report, CLIP Lab, IMDEA Software Institute. Available at https://cliplab.org/papers/jurjo-domcons-tr.pdf.
[9]A.Kelly, K.Marriott, H.Søndergaard & P.J. Stuckey (1998): A Practical Object-Oriented Analysis Engine for CLP. Software: Practice and Experience 28(2), pp. 188−224.
[10]B.Le Charlier & P.Van Hentenryck (1994): Experimental Evaluation of a Generic Abstract Interpretation Algorithm for Prolog. ACM Transactions on Programming Languages and Systems 16(1), pp. 35−101.
[11]K.Muthukumar & M.Hermenegildo (1989): Determination of Variable Dependence Information at Compile-Time Through Abstract Interpretation. In: 1989 North American Conference on Logic Programming, MIT Press, pp. 166−189.
[12]K.Muthukumar & M.Hermenegildo (1990): Deriving A Fixpoint Computation Algorithm for Top-down Abstract Interpretation of Logic Programs. Technical Report ACT-DC-153-90, Microelectronics and Computer Technology Corporation (MCC), Austin, TX 78759. Available at http://cliplab.org/papers/mcctr-fixpt.pdf.
[13]K.Muthukumar & M.Hermenegildo (1992): Compile-time Derivation of Variable Dependency Using Abstract Interpretation. Journal of Logic Programming 13(2/3), pp. 315−347.
[14]P.Van Roy & A.M. Despain (1990): The Benefits of Global Dataflow Analysis for an Optimizing Prolog Compiler. In: North American Conference on Logic Programming, MIT Press, pp. 501−515.
[15]R.Warren, M.Hermenegildo & S.K. Debray (1988): On the Practicality of Global Flow Analysis of Logic Programs. In: Fifth International Conference and Symposium on Logic Programming, MIT Press, pp. 684−699.
Constrained Horn Clauses (CHCs) are a logical formalism very well suited for automatic program verification and analysis [1]. Indeed, many verification problems can be reduced to problems of checking satisfiability of CHCs and several effective CHC solvers are currently available as back-end tools for program verification purposes [5,6].
Following the CHC-based verification approach, a program is translated into a set of definite CHCs (that is, clauses whose head is different from $\mathit{false}$), which capture the semantics of the program, together with a set of queries (that is, clauses whose head is $\mathit{false}$), which specify the program properties to be verified. Very often the program includes several functions, each one having its own contract (that is, a pair of a pre-condition and a post-condition) and the CHC translation of the verification problem generates several queries.
CHC solvers try to show the satisfiability of a set of CHCs of the form: $P \cup \{\mathit{false}\!\leftarrow\! G_1,\,\ldots,\, \mathit{false}\!\leftarrow\! G_n\}$, where $P$ is a set of definite CHCs, and $\mathit{false}\!\leftarrow\! G_1,\,\ldots,\,\mathit{false}\!\leftarrow\! G_n$ are queries, by trying to show in a separate way the satisfiability of each set $P\cup\{\mathit{false}\!\leftarrow\! G_i\}$, for $i\!=\!1,\ldots,n$. This approach may not always be effective, as the solver may not be able to exploit, possibly mutual, dependencies among the various queries.
In this paper we propose a CHC transformation technique that, given a set $P\cup\{\mbox{$\mathit{false} \!\leftarrow\! G_1,$}$ $\ldots,\,\mathit{false}\!\leftarrow\! G_n\}$ of CHCs, derives an equisatisfiable set $P'\cup\{\mathit{false}\!\leftarrow\! G'_1,\ldots,$ $\mathit{false}\!\leftarrow\! G'_n\}$, for whose satisfiability proof a CHC solver may exploit the mutual interactions among the $n$ satisfiability proofs, one for each query.
The CHC transformation algorithm ${\mathit T}_{\mathit{mq}}$ we present here, is based on adaptations of the usual unfold/fold transformation rules for CHCs (and CLP programs), and on a novel rule, called Query-based Strengthening, specifically designed for incorporating into the clauses relative to a particular query $Q$ some additional properties and constraints derived from other queries that are relative to predicates on which the predicates occurring in $Q$ depend.
Algorithm ${\mathit T}_{\mathit{mq}}$ is both sound and complete, that is, the transformed clauses are satisfiable if and only if so are the original ones. The completeness of ${\mathit T}_{\mathit{mq}}$ is very important because if a property does not hold, it allows us to infer the unsatisfiability of the original clauses, and hence to deduce the invalidity of the property to be verified.
The proposed algorithm improves over the ${\mathit T}_{\mathit{cata}}$ algorithm presented in a previous paper [4] which works by eliminating ADTs from sets of CHCs. ${\mathit T}_{\mathit{cata}}$ is only sound (indeed, it can be understood as computing an abstraction over the initial clauses), and thus if the transformed clauses are unsatisfiable we cannot infer anything about the satisfiability of the initial CHCs. The new algorithm ${\mathit T}_{\mathit{mq}}$ does not eliminate ADT variables, but the additional constraints it discovers are often very beneficial to the CHC solvers when trying to check the satisfiability of a given set of clauses, thereby enhancing their ability to verify program properties.
In order to define a class of CHCs for which our transformation algorithm always terminates, we have considered predicates for expressing properties that are catamorphisms, that is, predicates that are total and functional with respect to some of their arguments, and have a somewhat restricted recursive structure.
We have implemented algorithm ${\mathit T}_{\mathit{mq}}$ in a tool, called VeriCaT$_{mq}$, which extends VeriCaT [4] by guaranteeing a sound and complete transformation. VeriCaT$_{mq}$ is based on: (i) VeriMAP [2] for transforming CHCs, and (ii) SPACER [6] (with Z3 4.11.2) to check the satisfiability of the transformed CHCs.
We have considered 170 problems, as sets of CHCs, with 470 queries in total, equally divided between the class of satisfiable (sat) problems and unsatisfiable (unsat) problems (for each class we have 85 problems and 235 queries).
The problems we considered refer to programs that manipulate: (i) lists of integers by performing concatenation, permutation, reversal, and sorting, and (ii) binary search trees, by inserting and deleting elements. For list manipulating programs, we have considered properties encoded by catamorphisms such as: list length, minimum and maximum element, sum of elements, list content as sets or multisets of elements, and list sortedness (in ascending or descending order). For trees, we have considered tree size, tree height, minimum and maximum element, tree content and the binary search tree property.
In addition to satisfiable problems, we have also considered unsatisfiable problems that have been obtained from their satisfiable counterparts by introducing bugs in the programs: for instance, by not inserting an element in a list, or adding an extra constraint, or replacing a non-empty tree by an empty one.
In summary, VeriCaT$_{mq}$ was able to prove all the 170 considered problems whereas SPACER was able to prove the properties of 84 'unsat' problems out of 85, and none of the 'sat' problems. The total time needed for transforming the CHCs was 275 seconds (1.62 s per problem, on average), and checking the satisfiability of the transformed CHCs took about 174 s in total (about 1s average time, 0.10 s median time). For comparison, SPACER took 30.27 s for checking the unsatisfiability of 84 problems (0.36 s average time, 0.15 s median time). The benchmark and the tool are available at https://fmlab.unich.it/vericatmq.
Program | Problems | Queries | Spacer | VeriCaT$_{mq}$ | ||
---|---|---|---|---|---|---|
sat | unsat | sat | unsat | |||
List Membership | 2 | 6 | 0 | 1 | 1 | 1 |
List Permutation | 8 | 24 | 0 | 4 | 4 | 4 |
List Concatenation | 18 | 18 | 0 | 8 | 9 | 9 |
Reverse | 20 | 40 | 0 | 10 | 10 | 10 |
Double Reverse | 4 | 12 | 0 | 2 | 2 | 2 |
Reverse w/Accumulator | 6 | 18 | 0 | 3 | 3 | 3 |
Bubblesort | 12 | 36 | 0 | 6 | 6 | 6 |
Heapsort | 8 | 48 | 0 | 4 | 4 | 4 |
Insertionsort | 12 | 24 | 0 | 6 | 6 | 6 |
Mergesort | 18 | 84 | 0 | 9 | 9 | 9 |
Quicksort (version 1) | 12 | 38 | 0 | 6 | 6 | 6 |
Quicksort (version 2) | 12 | 36 | 0 | 6 | 6 | 6 |
Selectionsort | 14 | 42 | 0 | 7 | 7 | 7 |
Treesort | 4 | 20 | 0 | 2 | 2 | 2 |
Binary Search Tree | 20 | 24 | 0 | 10 | 10 | 10 |
Total | 170 | 470 | 0 | 84 | 85 | 85 |
For instance, for all the list sorting programs we have considered (Bubblesort, Heapsort, Insertionsort, Mergesort, Quicksort, Selectionsort and Treesort), VeriCaT$_{mq}$ was able to prove properties stating that the output list is sorted and has the same multiset of elements of the input list. Similarly, VeriCaT$_{mq}$ was able to prove that those properties do not hold, if extra elements are added to the output list, or some elements are not copied from the input list to the output list, or a wrong comparison operator is used.
The results obtained by the prototype implementation of our method are encouraging and show that, when used in combination with state-of-the-art CHC solvers, it can greatly improve their effectiveness to prove satisfiability of sets of CHCs with multiple queries, while it does not inhibit their remarkable ability to prove unsatisfiability, although some extra time due to the transformation process may be required.
Full details about the contributions of this paper can be found in the original publication [3].
Probabilistic Answer Set Programming under the Credal Semantics is a recently introduced formalism to express uncertainty with answer set programming where the probability of a query is described by a range. We propose to extend it to encode decision theory problems.
Probabilistic Answer Set Programming under the Credal Semantics [5] extends answer set programming [3] with ProbLog [6] probabilistic facts of the form \(\Pi::f\), where \(\Pi\) is a floating point value (between 0 and 1) representing the probability of \(f\) of being true. A selection of a truth value for every probabilistic fact identifies a world whose probability is the product of the probabilities of the probabilistic facts true times the product of one minus the probability of every probability fact false. In formula: $$ P(w) = \prod_{f_i \ \text{true} \in w} \Pi_i \cdot \prod_{f_i \ \text{false} \in w} (1-\Pi_i). $$ In Probabilistic Logic Programming [6] (PLP), a world is a Prolog program, so it has exactly one model. In Probabilistic Answer Set Programming under the credal semantics (PASP), every world is an answer set program [8], so it has zero or more (stable) models. Every world is required to have at least one stable model. In PASP, the probability of a query (i.e., a conjunction of ground atoms) is represented with a probability range, composed of a lower and upper bound. A world contributes to both the lower and upper bounds if the query is true in every answer set while it contributes only to the upper bound if it is true in some of the answer sets. That is, \(P(q) = [\underline{P}(q), \overline{P}(q)]\) where $$ \underline{P}(q) = \sum_{w_i \mid \forall m \in AS(w_i), \ m \models q} P(w_i),\ \overline{P}(q) = \sum_{w_i \mid \exists m \in AS(w_i), \ m \models q} P(w_i). $$ The probability bounds can be computed with, for example, the tool described in [1]. The DTProbLog framework [4] allows to express decision theory problems with a ProbLog [6] program. It introduces a set \(U\) of utility atoms of the form \(utility(a,r)\) where \(r\) is the reward obtained to satisfy \(a\) (i.e., when \(a\) is true) and a set of decision atoms \(D\). Every subset of decision atoms defines a strategy \(\sigma\) (a ProbLog program) and its utility is computed as $$ Util(\sigma) = \sum_{(a,r) \in U} r \cdot P_{\sigma}(a) $$ where \(P_{\sigma}(a)\) is the probability of \(a\) computed in the ProbLog program identified by fixing the decision atoms in \(\sigma\) to true. The goal is to find the strategy \(\sigma^*\) that maximizes the utility, i.e., \(\sigma^* = argmax_{\sigma}Util(\sigma)\).
We apply this framework to PASP, where every world has one or more stable models.
Thus, the utility is described by a lower and an upper bound:
$$
Util(\mathcal{\sigma}) = \left[\underline{Util}(\mathcal{\sigma}), \overline{Util}(\mathcal{\sigma})\right] = \left[
\sum_{(a,r) \in U} r \cdot \underline{P}_{\sigma}(a),\sum_{(a,r) \in U} r \cdot \overline{P}_{\sigma}(a) \right]
$$
We have now to select whether to optimize the lower or upper utility, and so there are two possible goals:
$$
\sigma^{*} = argmax_{\sigma}(\underline{Util}(\sigma)).
$$
or
$$
\sigma^{*} = argmax_{\sigma}(\overline{Util}(\sigma)).
$$
depending on the considered target probability.
Note that with this representation the lower utility can be greater than the upper utility, when, for example, there are
both positive and negative rewards.
We consider here only the strategies where the lower utility is less or equal than the upper utility.
To clarify, consider this simple program:
0.7::pa. 0.2::pb.
decision da. decision db.
utility(r0,3). utility(r1,-11).
r0:- pa, da.
r0;r1:- pb, db.
\(pa\) and \(pb\) are two probabilistic facts and \(da\) and \(db\) two decision atoms.
The rewards we get to satisfy \(r0\) and \(r1\) are respectively 3 and -11.
There are 4 possible strategies (no decision atoms selected, only one decision atom selected, and both decision atoms
selected).
Each of these have 4 worlds (no probabilistic facts true, only one probabilistic fact true, and both probabilistic facts
true).
If we consider the strategy \(\sigma_{da} = \{da\}\), we have \(P_{\sigma_{da}}(r0) = [0.7,0.7]\) and \(P_{\sigma_{da}}(r1) =
[0,0]\) (only the first rule is considered), and \(Util(\sigma_{da}) = [3 \cdot 0.7 + (-11) \cdot 0,3 \cdot 0.7 + (-11)
\cdot 0] = [2.1,2.1]\).
If we repeat this process for all the strategies and we consider the upper utility as target, we get that \(\sigma_{da} =
\{da\}\) is the one that maximizes the upper utility.
A naive algorithm consists in enumerating all the possible strategies and then computing the lower and upper probability for every decision atom [1]. However, this clearly cannot scale, since the number of possible strategies is \(2^{|D|}\). Moreover, the algorithm of [1] adopts enumeration of stable models and projection on probabilistic facts [7], that also requires the generation of an exponential number of answer sets. Thus, a practical solution should adopt both approximate methods for the generation of the possible strategies and for inference. For the former, greedy algorithms such as genetic algorithms [9] can be a possible solution. For inference, approximate methods based on sampling, such as the one proposed in [2] can be of interest.
This research was partly supported by TAILOR, a project funded by EU Horizon 2020 research and innovation programme under GA No. 952215.
When modelling expert knowledge as logic programs, default negation is very useful, but might lead to there being no stable models. Detecting the exact causes of the incoherence in the logic program manually can become quite cumbersome, especially in larger programs. Moreover, establishing coherence requires expertise regarding the modelled knowledge as well as technical knowledge about the program and its rules. In this demo, we present the implementation of a workflow that enables knowledge experts to obtain a coherent logic program by modifying it in interaction with a system that explains the causes of the incoherence and provides possible solutions to choose from.
Figure 1: Amendment Workflow
Figure 1 shows the general workflow that is implemented in this prototype for establishing the coherence in a given incoherent program $\cal{P}$.
In the following, we will describe the general workflow for this application, and how it helps the knowledge expert to gradually restore coherence. For this consider the following program $\cal{P^1}$ inspired by the medical domain will be used as a running example^{2}:
$r_1 : fever \leftarrow highTemp, {\sim}sunstrk.$
$r_2 : fatigue \leftarrow lowEnergy, {\sim}stress, {\sim}sports.$
$r_3 : highTemp \leftarrow temp > 37.$
$r_4 : sunstrk \leftarrow highTemp, {\sim}fever.$
$r_5 : allrg \leftarrow pollenSeason, fatigue, {\sim}flu, {\sim}cold.$
$r_6 : cold \leftarrow fatigue, soreThroat, {\sim}migrn.$
$r_7 : flu \leftarrow fatigue, {\sim}migrn.$
$r_8 : migrn \leftarrow headache, {\sim}allrg.$
$r_9 : soreThroat.$
$r_{10} : headache.$
$r_{11} : pollenSeason.$
$r_{12} : lowEnergy.$
$r_{13} : temp > 37.$
Figure 2: SCUP visualisation
Figure 3: Amendment selection
Figure 4: Explanation component
The process starts with the knowledge expert providing an extended logic program ([7]), e.g. $P^1$, via the interface^{3}. For each $P^i$, the regular models are computed using an ASP encoding for abstract argumentation frameworks presented in ([8]). If the program is already coherent, the total stable interpretations are shown accordingly. If not, the user can choose the regular model $M^i$ that is closest to an intended total stable interpretation of $P$ (see Figure 2 (1)). On the basis of the labelling that corresponds to $M^i$, the argumentation graph for $P^i$ is computed and shown to the user alongside the subgraphs responsible for incoherence (called SCUPS) (see Figure 2 (2)). The system then displays the argumentation graph, where nodes are coloured according to their label where gray nodes stand for undefined atoms, green ones for true atoms, and red nodes for false atoms. Likewise, nodes that are part of a SCUP have red dashed border. Figure 2 shows that $P^1$ contains a SCUP involving the atoms $allrg$, $cold$, $flu$, and $migrn$. The user is then shown the list of SCUPs and can choose the SCUP they want to resolve (first) (see Figure 2 (3)). For the chosen SCUP, the interface shows all involved atoms and rules (see Figure 2 (4)). Advantage is taken of the high explanatory potential of computational argumentation by implementing explanation methods inspired by the dialogue games for argumentation ([2][3]) to explain (non-)acceptability of atoms in a regular model, via the explanation of the (non-)acceptability of an argument for that atom w.r.t. the corresponding preferred labelling of the argumentation framework. This component contains explanations for the label of each atom (set) in ${\tt AF}(\cal{P}^i)$. It uses an approach derived from argumentative dialogue games to tackle the following explanation task: Given the regular interpretation $\langle I, I'\rangle$ of $\cal{P}$ and $A\in\cal{A}$, explain ${\tt Int2Lab}(\langle I, I'\rangle)({\sim}A)$. If the user wishes to see explanations for the labels of certain atom sets, they can choose the respective set in this component (see Figure 4 (1)). For the chosen atom set, the application will present the list of their attackers and explain each of their labels. It furthermore shows the rules that are associated with the atom set and their labelling. Figure 4 (2) shows the explanation why the assumption ${\sim}allrg$ is labelled undecided in the chosen model. If an explanation for an attacker is additionally available, the user can analyze these as well. In Figure 4 (3) the presented explanation is illustrated if the user decides to inspect the attackers of ${\sim}cold$.
In a next step, on the basis of the explanations for the labelling of ${\tt AF}(\cal{P}^i )$, the user can explore the amendments that are suitable for resolving for resolution of the chosen SCUP. The amendments are computed using the approach defined in ([11]). The list of amendments can additionally be filtered by a strategy as even relatively small programs can have a vast amount of possible amendments (see Figure 3). For each amendment, its used strategy, the amended rule and amendment are shown. The chosen amendment is directly applied on the given input program $P^i$ and the modified program $\cal{P}^{i+1}$ is solved. In our running example, applying the first suggested amendment that is shown in Figure 3 would replace $r_7$ in $\cal{P}^1$ by a fact ${\sim}migrn.$, which results in a coherent program as this modification dissolves the unique SCUP in $\cal{P}^1$. If otherwise $\cal{P}^{i+1}$ is still incoherent, the remaining SCUPs can be resolved by starting a new iteration of this process again with the modified program $\cal{P}^{i+1}$. The result of this workflow is a coherent program $\cal{P}^n$ that represents professionally adequate knowledge.
The presented system was implemented using Python 3.10 and clingo 5.6 ([6]) with asprin 3.1.2beta ([9]).
^{1}The implementation is available on icarus.cs.tu-dortmund.de.
^{2}Here, the atoms $sunstrk$, $migrn$ and $allrg$ denote that a person suffers from a sunstroke, migraine, or allergies, respectively.
^{3}Future work will include the support of ASP extensions such as aggregates and cardinality atoms ([1]).
14th of August, 2023 | Andre Thevapalan Jesse Heyninck |
PASTA is a novel framework to perform inference, both exact and approximate, in Probabilistic Answer Set Programming under the Credal Semantics and to solve other related tasks, such as abduction, decision theory, maximum a posteriori inference, and parameter learning. Moreover, it also allows the expression of statistical statements. This paper shows the overall structure of the PASTA tool as well as some of the main options.
Answer Set Programming (ASP) is a logic-based language useful in describing complex combinatorial domains. Most of ASP research focuses on deterministic programs. There are some semantics that extend ASP and allow uncertainty on data, mainly LPMLN [15], P-log [7], and the credal semantics [9]. The PASTA tool considers the last.
A probabilistic answer set program under the credal semantics is an answer set program extended with probabilistic facts [10], i.e., constructs of the form \(\Pi::a.\) where \(a\) is an atom and \(\Pi \in [0,1]\) is its probability value.
The intuitive meaning is that \(a\) is true with probability \(\Pi\).
We assume that probabilistic facts cannot appear as head of rules.
The following is an example of a program:
0.4:: a.
0.7:: b.
qr : - a.
qr ; nqr : - b.
A selection of a truth value for every probabilistic fact defines a world \(w\), i.e., an answer set program, whose probability can be computed as \(P(w) = \prod_{f_i \ \text{selected}} \Pi_i \cdot \prod_{f_i \ \text{not selected}} (1-\Pi_i)\). The previously shown program has \(2^2 = 4\) worlds. The probability of the world, for example, where both \(a\) and \(b\) are true is \(0.4 \cdot 0.7 = 0.28\). Since every world is an answer set program [14], every world has zero or more answer sets. The credal semantics requires that every world has at least one answer set. The probability of a query (conjunction of ground atoms) \(P(q)\) is defined by a range, with a lower and upper probability, i.e., \(P(q) = [\underline{P}(q),\overline{P}(q)]\). A world contributes to the upper probability if it has at least one answer set where the query is true and it contributes to both the lower and upper probability if the query is true in all the answer sets. That is, the lower probability is the sum of the probabilities of the worlds where the query is true in all the answer sets while the upper probability is the sum of the probabilities of the worlds where the query is true in at least one answer set. In formula \begin{equation} \underline{P}(q) = \sum_{w_i \mid \forall m \in AS(w_i), \ m \models q} P(w_i),\ \overline{P}(q) = \sum_{w_i \mid \exists m \in AS(w_i), \ m \models q} P(w_i). \end{equation} Consider the query \(qr\) in the previous program. The world where both \(a\) and \(b\) are false has one empty answer set, so it does not contribute to the probability. The world where \(a\) is false and \(b\) is true has two answer sets, \(\{\{b \ qr\}, \{b \ nqr\}\}\). The query is true in only one of the two, so we have a contribution only to the upper probability of \(0.6 \cdot 0.7 = 0.42\). The world where \(a\) is true and \(b\) is false has one answer set, \(\{\{a \ qr\}\}\). The query is true in all the answer sets, so we have a contribution of \(0.4 \cdot 0.3 = 0.12\) to both the lower and upper probability. Lastly, the world where both \(a\) and \(b\) are true has one answer set, \(\{\{a \ b \ qr\}\}\). The query is true in all the answer sets, so we have a contribution of \(0.4 \cdot 0.7 = 0.28\) to both the lower and upper probability. Overall, \(P(q) = [0.12 + 0.28, 0.42 + 0.12 + 0.28] = [0.4, 0.82]\).
Currently, the PASTA tool performs exact inference [2], whose algorithm is based on projected answer set enumeration [13], approximate inference via sampling [3], abduction [1] (i.e., computing the minimal set, in terms of set inclusion, of abducible facts such that the probability of the query is maximized), MAP/MPE [5] (finding an assignment to a subset of probabilistic facts that maximizes the sum of the probabilities of the identified worlds while evidence is satisfied), decision theory [6] (finding a subset of decision atoms that maximizes a reward), and parameter learning [4] (learning the probability of the probabilistic facts such that the likelihood of the examples is maximized). It allows to express statistical statements of the form [2] \((C | A)[\Pi_l, \Pi_u]\) meaning that the fraction of \(A\)s that are also \(C\)s is between \(\Pi_l\) and \(\Pi_u\). Moreover, it adopts normalization [11] to perform inference in probabilistic answer set programs where some worlds have no answer sets. That is, the lower and upper probability bounds are divided by the sum of the probabilities of the worlds with no answer sets.
The system is written in Python, is open source, and is available on GitHub. It can be installed via the Python package installer pip and provides a command line interface with several options to select the task to solve. Moreover, a web interface exposes some of the most relevant options in a more intuitive way. It is also possible to use the system as a Python library. PASTA leverages the clingo ASP solver [12] to compute answer sets. The system is structured in multiple modules: the pasta module parses the command line arguments and selects the subsequent functions and methods to call. The generator module parses the program into an ASP version that can be interpreted by the clingo solver. The interface with clingo is managed by the asp_interface module and the resulting answer sets are analyzed with the models_handler module which also computes the various probabilities. There are some reserved keywords: \(abducible\), that denotes abducible facts in the context of abduction (for example, \(abducible\ a\) states that the atom \(a\) is an abducible); \(map\), that denotes facts to be considered for the MAP/MPE task (for example, \(map\ 0.4::a\) states that \(a\) is a probabilistic fact whose probability is 0.4 and that can be selected to be included in the solution set for the MAP/MPE task); and \(decision\) and \(utility\), that mark decision facts and utility attributes [8] for the decision theory task (for example, \(decision\ a\) states that \(a\) is a decision atom and \(utility(f,2.3)\) states that the reward obtained when \(f\) is true is 2.3).
This research was partly supported by TAILOR, a project funded by EU Horizon 2020 research and innovation programme under GA No. 952215.
Logical English (LE) is a natural language syntax for pure Prolog and other logic programming languages, such as ASP and s(CASP). Its main applications until now have been to explore the representation of a wide range of legal texts, helping to identify ambiguities, explore alternative representations of the same text, and compare the logical consequences of the alternatives. The texts include portions of loan agreements, accountancy law, Italian citizenship, EU law on criminal rights, International Swaps and Derivative contracts, and insurance contracts. The current implementation in SWI Prolog can be accessed at https://logicalenglish.logicalcontracts.com.
The basic form of LE is simply syntactic sugar for pure Prolog[2], with predicates written in infix form and declared by means of templates, as in:
*a borrower* defaults on *a date*
where asterisks delimit the argument places of the predicate. Variables are signalled by the use of one of the determiners "a", "an" or "the". An indefinite determiner, "a" or "an", introduces the first occurrence of a variable in a sentence. All later occurrences of the same variable in the same sentence are prefixed by the definite determiner "the".
LE has only minimal linguistic knowledge of English. Its knowledge of English vocabulary is restricted to the determiners; the logical connectives "if", "and", "or" and "it is not the case that"; the logical pattern "for all cases in which — it is the case that —"; and the logical keyword "that". The keyword "that" identifies the use of a meta-predicate, for representing such "propositional attitudes as prohibition, obligation, belief, desire, fear, notification, etc. Indentation, rather than parentheses, is used to indicate the relative strength of binding of the logical connectives. LE has virtually no knowledge of English grammar. In particular, it does not distinguish between singular and plural nouns and verbs, and it does not know about the relationship between the different tenses of verbs. Despite these restrictions, and because it has the same expressiveness as pure Prolog, it can be used to represent a broad range of knowledge, as shown by its application to the representation of legal texts [3,4,5,6,7]. Here is an example based on the loan agreement in [1]. The SWISH implementation of the example can be found at https://logicalenglish.logicalcontracts.com/p/new_loan_with_cure.pl.
the borrower defaults on a date D2 if the borrower has the obligation that an eventuality and the borrower fails to satisfy the obligation that the eventuality and the lender notifies the borrower on a date D1 that the borrower fails to satisfy the obligation that the eventuality and D2 is 2 days after D1 and it is not the case that the borrower cures on or before D2 the failure to satisfy the obligation that the eventuality.
defaults_on(the_borrower, A) :- has_the_obligation_that(the_borrower, B), fails_to_satisfy_the_obligation_that(the_borrower, B), notifies_on_that(the_lender, the_borrower, C, fails_to_satisfy_the_obligation_that(the_borrower, B)), is_days_after(A, 2, C), not cures_on_or_before_the_failure_to_satisfy_the_obligation_that(the_borrower, A, B).
Figure 1 illustrates a scenario, called "payment", in which the borrower fails to satisfy the obligations, on lines 22 and 23, to pay the lender 550 on 2015-06-01 and 525 on 2016-06-01. The lender does not notice the first failure, but notices the second failure, and gives notice to the borrower of the second failure on 2016-06-04. The borrower attempts to cure the failure, by paying the correct amount 525 and by notifying the lender of the payment within the two day period of grace. But unfortunately, the borrower notifies the lender incorrectly that the payment was made on the date of notification rather than on the date of payment.
Figure 2 illustrates the result of answering the combination of the stored query, called "defaults" with the scenario. An LE document can contain several stored scenarios and several stored queries, which can be combined in the SWISH query pane.
The SWISH implementation also generates explanations in response to commands of the form answer(defaults, with(payment), le(E), R) as shown in figure 3. For VSC users there exist extensions for syntax highlighting and remote execution on a SWISH server. It is also possible to call the LE parser without the SWISH environment, as a standalone Prolog application. All the sources and further information are available at https://github.com/LogicalContracts/LogicalEnglish/.