We define, for any logic program P, the Well-Founded Completion compwf(P) of P which, like Clark's Predicate Completion comp(P) of P, is a first order extension of P providing the intended meaning or semantics for...
详细信息
We define, for any logic program P, the Well-Founded Completion compwf(P) of P which, like Clark's Predicate Completion comp(P) of P, is a first order extension of P providing the intended meaning or semantics for the program. We show that well-founded completions compwf(P) are defined for all logic programs P and that they can be computed using a simple and constructive iterative procedure, which, in the case of propositional programs, is quadratic. Moreover, we prove that the set of sentences logically implied by compwf(P) precisely coincides withthe set of sentences satisfied in the well-founded model MP of P, thus showing that the new completion compwf(P) of P in fact describes the well-founded semantics of P. Our results demonstrate that the well-founded semantics can be equivalently defined in terms of classical, 2-valued logic, without any reference to 3-valued models or 3-valued logic. they also clarify the exact nature of the close relationship existing between the stable and well-founded semantics.
the Clark completion of a program is a way of making explicit the inferences which may be made from the program using the Negation as Failure (NAF) rule. this may be thought of as adding negative information to the pr...
详细信息
the Clark completion of a program is a way of making explicit the inferences which may be made from the program using the Negation as Failure (NAF) rule. this may be thought of as adding negative information to the program in such a way that an atom fails iff its negation is derivable from the completion of the program. We show how the completion process may be extended to hereditary Harrop formulae, a class of formulae that properly includes Horn clauses, and, more importantly, that the completion of a hereditary Harrop formulae program may be expressed as a hereditary Harrop formulae program. In this way the richer framework of hereditary Harrop formulae allows the completion to be given in a more explicit form than that of Clark. this also allows the completion to be seen as a set of clauses, i.e. a program, rather than just as a formula of first-order logic. Withthe restriction that programs are locally consistent, we show that the completion behaves as expected, in that the computational properties of the program and its completion correspond precisely.
Negation as failure is sound both for the closed world assumption, CWA, and the Clark's completion, Comp(W) of a program W. Anyway, there is no semantics for which it is also complete for all programs and queries,...
详细信息
Negation as failure is sound both for the closed world assumption, CWA, and the Clark's completion, Comp(W) of a program W. Anyway, there is no semantics for which it is also complete for all programs and queries, as non-ground negative literals cannot be dealt with, and cause floundering. We define a new negation rule, for which floundering is excluded and we give a semantics Comp(W)* for which the new rule is both sound and complete. this semantics is a weak version of Comp(W) obtained by enlarging as much as possible the free interpretation of variables and functions given by Herbrand-interpretations. We have called the proposed negation rule the Negation As Instantiation rule (NAI rule) because an atom is considered negated, though some of its derivations do not finitely fail, provided that some of its variables get instantiated. the NAI rule subsume negation as failure and can be efficiently implemented. A set FFI (Failure by Finite Instantiation) is defined which is proved equivalent to the complement of Tc&darrω with respect to the set of all atoms, where Tc is the immediate consequence operator extended to deal with interpretations that contain atoms with variables (the C-semantics in [6]).
We present a technique for the proof of a wide class of logical properties of the relations defined in a locally stratified logic program. the technique is based on SLS-Resolution. To prove that a program satisfies so...
详细信息
We present a technique for the proof of a wide class of logical properties of the relations defined in a locally stratified logic program. the technique is based on SLS-Resolution. To prove that a program satisfies some property we show that a goal equivalent to the property has a failed SLS-tree. Since these failed trees will often contain infinite branches we develop a technique which enables the existence of an infinite and failed tree to be deduced from consideration of a finite sub-tree. We demonstrate a strong correspondence between this technique and the method of Computational Induction which has previously been proposed for the proof of program properties. Our approach allows the power of induction theorem-proving to be incorporated naturally in a resolution-based framework and establishes a unity between query evaluation and proof of program properties. the approach has important applications in Program Development including proof of program equivalence and can also be applied to perform program synthesis, where the incorporation of induction allows the synthesis of recursive definitions.
this report discusses the definition and implementation of constraint operations for CLP(FT), Prolog with universally quantified disequality constraints on finite trees. As a follow-up to [SH90], where we defined seve...
详细信息
this report discusses the definition and implementation of constraint operations for CLP(FT), Prolog with universally quantified disequality constraints on finite trees. As a follow-up to [SH90], where we defined several operations needed for the partial evaluation of CLP(FT), this report presents: a concise syntax for U-constraints, universally quantified disequality constraints;algorithms for the projection, equivalence, and semantic difference operations needed in the partial evaluation algorithm;a solved form for U-constraints, based on a solved form for existentially quantified equations, that allows the projection of a set of constraints onto a set of variables to be easily computed. the projection of a solved form set C of constraints onto a set V of variables is equal to those constraints c in C whose free variables are all contained in V;and a canonical form for sets of U-constraints that allows the equivalence operation to be easily computed. We also discuss applications of U-constraints and relation to previous work.
For representing high level knowledge, such as the mathematical knowledge used in interactive theorem provers and verification systems, it is desirable to extend Prolog's concept of data object. A basic reason is ...
详细信息
For representing high level knowledge, such as the mathematical knowledge used in interactive theorem provers and verification systems, it is desirable to extend Prolog's concept of data object. A basic reason is that Prolog data objects - Herbrand objects - are terms of a minimal object language, which does not include its own object variables, or quantification over those variables. Qu-Prolog (Quantifier Prolog) is an extended logicprogramming concept which takes as its data objects, object terms which may include object level variables, free or bound, and arbitrary quantifiers to bind those variables. Qu-Prolog is unique in allowing its data objects to include free occurrences of object variables. this paper describes Qu-Prolog's data objects and its facilities for computing on those objects. the Qu-Prolog unification algorithm unifies Qu-Prolog terms up to changes of bound variables. the power of Qu-Prolog unification is greatly increased by the inclusion in the language of an evaluable substitution operator which correctly substitutes at unification time for free occurrences of object variables. Some related Qu-Prolog facilities for implementing theorem proving algorithms are described, including a new method for persisting data across queries. Qu-Prolog 3.0 is a compiled implementation which is in experimental use, supporting the development of interactive reasoning systems.
A flexible scheduler for distributing and- and or- parallel work in the Andorra-I system is presented. the scheduler allows workers to move freely between teams. Its strategy is based on estimates of and-and or-parall...
详细信息
暂无评论