We present the CIFF proof procedure for abductive logicprogramming with constraints, and we prove its correctness. CIFF is an extension of the IFF proof procedure for abductive logicprogramming, relaxing the origina...
详细信息
We present the CIFF proof procedure for abductive logicprogramming with constraints, and we prove its correctness. CIFF is an extension of the IFF proof procedure for abductive logicprogramming, relaxing the original restrictions over variable quantification (allowedness conditions) and incorporating a constraint solver to deal with numerical constraints as in constraint logicprogramming. Finally, we describe the CIFF system, comparing it with state-of-the-art abductive systems and answer set solvers and showing how to use it to program some applications.
logic Production System (LPS) is a logic-based framework for modelling reactive behaviour. Based on abductive logicprogramming, it combines reactive rules with logic programs, a database and a causal theory that spec...
详细信息
logic Production System (LPS) is a logic-based framework for modelling reactive behaviour. Based on abductive logicprogramming, it combines reactive rules with logic programs, a database and a causal theory that specifies transitions between the states of the database. This paper proposes a systematic mapping of the Kernel of this framework (called KELPS) into an answer set program (ASP). For this purpose a new variant of KELPS with finite models, called n-distance KELPS, is introduced. A formal definition of the mapping from this n-distance KELPS to ASP is given and proven sound and complete. The Answer Set programming paradigm allows to capture additional behaviours to the basic reactivity of KELPS, in particular proactive, pre-emptive and prospective behaviours. These are all discussed and illustrated with examples. Then a hybrid framework is proposed that integrates KELPS and ASP, allowing to combine the strengths of both paradigms.
Partial functions are common abstractions in formal specification notations such as Z, B and Alloy. Conversely, executable programming languages usually provide little or no support for them. In this paper we propose ...
详细信息
Partial functions are common abstractions in formal specification notations such as Z, B and Alloy. Conversely, executable programming languages usually provide little or no support for them. In this paper we propose to add partial functions as a primitive feature to a Constraint logicprogramming (CLP) language, namely {log}. Although partial functions could be programmed on top of {log}, providing them as first-class citizens adds valuable flexibility and generality to the form of set-theoretic formulas that the language can safely deal with. In particular, the paper shows how the {log} constraint solver is naturally extended in order to accommodate for the new primitive constraints dealing with partial functions. Efficiency of the new version is empirically assessed by running a number of non-trivial set-theoretical goals involving partial functions, obtained from specifications written in Z.
Program completion is a translation from the language of logic programs into the language of first-order theories. Its original definition has been extended to programs that include integer arithmetic, accept input, a...
详细信息
Program completion is a translation from the language of logic programs into the language of first-order theories. Its original definition has been extended to programs that include integer arithmetic, accept input, and distinguish between output predicates and auxiliary predicates. For tight programs, that generalization of completion is known to match the stable model semantics, which is the basis of answer set programming. We show that the tightness condition in this theorem can be replaced by a less restrictive "local tightness" requirement. From this fact we conclude that the proof assistant anthem-p2p can be used to verify equivalence between locally tight programs.
A fundamental task for propositional logic is to compute models of propositional formulas. Programs developed for this task are called satisfiability solvers. We show that transition systems introduced by Nieuwenhuis,...
详细信息
A fundamental task for propositional logic is to compute models of propositional formulas. Programs developed for this task are called satisfiability solvers. We show that transition systems introduced by Nieuwenhuis, Oliveras, and Tinelli to model and analyze satisfiability solvers can be adapted for solvers developed for two other propositional formalisms: logicprogramming under the answer-set semantics, and the logic PC(ID). We show that in each case the task of computing models can be seen as "satisfiability modulo answer-set programming," where the goal is to find a model of a theory that also is an answer set of a certain program. The unifying perspective we develop shows, in particular, that solvers clasp and MINISAT(ID) are closely related despite being developed for different formalisms, one for answer-set programming and the latter for the logic PC(ID).
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.
This paper studies the relation between two recent extensions of propositional Equilibrium logic, a well-known logical characterisation of Answer Set programming. In particular, we show how Temporal Equilibrium logic,...
详细信息
This paper studies the relation between two recent extensions of propositional Equilibrium logic, a well-known logical characterisation of Answer Set programming. In particular, we show how Temporal Equilibrium logic, which introduces modal operators as those typically handled in Linear-Time Temporal logic (LTL), can be encoded into Infinitary Equilibrium logic, a recent formalisation that allows the use of infinite conjunctions and disjunctions. We prove the correctness of this encoding and, as an application, we further use it to show that the semantics of the temporal logicprogramming formalism called TEMPLOG is subsumed by Temporal Equilibrium logic.
This special issue of theory and practice of logic programming (TPLP) contains the regular papers accepted for presentation at the 33rd International Conference on logicprogramming (ICLP 2017), held in Melbourne, Aus...
详细信息
This special issue of theory and practice of logic programming (TPLP) contains the regular papers accepted for presentation at the 33rd International Conference on logicprogramming (ICLP 2017), held in Melbourne, Australia from the 28th of August to the 1st of September, 2017. ICLP 2017 was colocated with the 23rd International Conference on Principles and practice of Constraint programming (CP 2017) and the 20th International Conference on theory and Applications of Satisfiability Testing (SAT 2017). Since the first conference held in Marseille in 1982, ICLP has been the premier international event for presenting research in logicprogramming.
The ICLP series of conferences provides a technical forum for presenting and disseminating innovative research in the field of logicprogramming. The 24th International Conference on logicprogramming took place from ...
The ICLP series of conferences provides a technical forum for presenting and disseminating innovative research in the field of logicprogramming. The 24th International Conference on logicprogramming took place from December 9–13, 2008 in the city of Udine, Italy. The conference attracted 177 submissions and featured a high-quality program focused on the foundations, developments, and applications of logicprogramming. Of particular significance was the special session celebrating the 20th anniversary of the seminal paper on the stable model semantics.
The logicprogramming (LP) community, through the Association for logicprogramming (ALP) and its Executive Committee, decided to introduce for 2010 important changes in the way the main yearly results in LP and relat...
The logicprogramming (LP) community, through the Association for logicprogramming (ALP) and its Executive Committee, decided to introduce for 2010 important changes in the way the main yearly results in LP and related areas are published. Whereas such results have appeared to date in standalone volumes of proceedings of the yearly International Conferences on logicprogramming (ICLP), and this method—fully in the tradition of Computer Science (CS)—has served the community well, it was felt that an effort needed to be made to achieve a higher level of compatibility with the publishing mechanisms of other fields outside CS.
暂无评论