Negation as Failure Using Tight Derivations for General Logic Programs

1988 ◽  
pp. 149-176 ◽  
Author(s):  
Allen Van Gelder
Keyword(s):  
Logic Programs ◽  
Negation As Failure ◽  
General Logic

scholarly journals Practical Methods for Proving Termination of General Logic Programs

1996 ◽  
Vol 4 ◽  
pp. 179-208 ◽  
Author(s):  
E. Marchiori
Keyword(s):  
Selection Rule ◽  
Logic Programs ◽  
Negation As Failure ◽  
General Logic ◽  
Constructive Negation

Termination of logic programs with negated body atoms (here called general logic programs) is an important topic. One reason is that many computational mechanisms used to process negated atoms, like Clark's negation as failure and Chan's constructive negation, are based on termination conditions. This paper introduces a methodology for proving termination of general logic programs w.r.t. the Prolog selection rule. The idea is to distinguish parts of the program depending on whether or not their termination depends on the selection rule. To this end, the notions of low-, weakly up-, and up-acceptable program are introduced. We use these notions to develop a methodology for proving termination of general logic programs, and show how interesting problems in non-monotonic reasoning can be formalized and implemented by means of terminating general logic programs.

Y-Logic: A Framework for Reasoning About Chameleonic Programs with Inconsistent Completions

1990 ◽  
Vol 13 (4) ◽  
pp. 465-483
Author(s):  
V.S. Subrahmanian
Keyword(s):  
Classical Logic ◽  
Logic Program ◽  
Logic Programs ◽  
Large Subset ◽  
General Logic ◽  
Traditional Sense

Large logic programs are normally designed by teams of individuals, each of whom designs a subprogram. While each of these subprograms may have consistent completions, the logic program obtained by taking the union of these subprograms may not. However, the resulting program still serves a useful purpose, for a (possibly) very large subset of it still has a consistent completion. We argue that “small” inconsistencies may cause a logic program to have no models (in the traditional sense), even though it still serves some useful purpose. A semantics is developed in this paper for general logic programs which ascribes a very reasonable meaning to general logic programs irrespective of whether they have consistent (in the classical logic sense) completions.

Tabled evaluation with delaying for general logic programs

1996 ◽  
Vol 43 (1) ◽  
pp. 20-74 ◽  
Author(s):  
Weidong Chen ◽  
David S. Warren
Keyword(s):  
Logic Programs ◽  
General Logic

scholarly journals Termination prediction for general logic programs

2009 ◽  
Vol 9 (6) ◽  
pp. 751-780 ◽  
Author(s):  
YI-DONG SHEN ◽  
DANNY DE SCHREYE ◽  
DEAN VOETS
Keyword(s):  
State Of The Art ◽  
Logic Program ◽  
Time Limit ◽  
Experimental Results ◽  
Prediction Tool ◽  
Logic Programs ◽  
General Logic ◽  
Necessary And Sufficient ◽  
Termination Problem

AbstractWe present a heuristic framework for attacking the undecidable termination problem of logic programs, as an alternative to current termination/nontermination proof approaches. We introduce an idea of termination prediction, which predicts termination of a logic program in case that neither a termination nor a non-termination proof is applicable. We establish a necessary and sufficient characterization of infinite (generalized) SLDNF-derivations with arbitrary (concrete or moded) queries, and develop an algorithm that predicts termination of general logic programs with arbitrary nonfloundering queries. We have implemented a termination prediction tool and obtained quite satisfactory experimental results. Except for five programs which break the experiment time limit, our prediction is 100% correct for all 296 benchmark programs of the Termination Competition 2007, of which 18 programs cannot be proved by any of the existing state-of-the-art analyzers like AProVE07, NTI, Polytool, and TALP.

ON THE PROPOSITIONAL SLDNF-RESOLUTION

1996 ◽  
Vol 07 (04) ◽  
pp. 359-406 ◽  
Author(s):  
JAN A. PLAZA
Keyword(s):  
Propositional Logic ◽  
Modal Logics ◽  
Logic Programs ◽  
Negation As Failure ◽  
Intermediate Logics ◽  
Original Program ◽  
Declarative Semantics ◽  
Constructive Version ◽  
Fix Point ◽  
Multivalued Semantics

We consider propositional logic programs with negations. We define notions of constructive transformation and constructive completion of a program. We use these notions to characterize SLDNF-resolution in classical, intuitionistic and intermediate logics, and also to derive a characterization in modal logics of knowledge. We show that the three-valued and four-valued fix-point or declarative semantics for program P are equivalent to the two-valued semantics for the constructive version of P. We argue that it would be beneficial to replace Negation as Failure by constructive transformation, and it would be beneficial to use the semantics for the constructive version of the program instead of multivalued semantics for the original program.

Sign in / Sign up

Export Citation Format

Share Document