A Proof Procedure for Extended Logic Programs.
Frank Teusink · Centrum Wiskunde & Informatica (CWI), the national research institute for mathematics and computer science in the Netherlands · 1993
In [GL90], M. Gelfond and V. Lifschitz proposed to extend general logic programs to so-called extended logic programs, by adding strong negation. They proposed answer sets as a semantics for these programs. However, this semantics uses the notion of global consistency. The necessity of testing for global consistency makes finding a proof for a specific query w.r.t. a program as hard as finding a complete answer set for that program. In this paper, we abandon the idea of preserving global consistency and propose a modified transformation from extended logic programs to general logic programs, based on a semantics in which only local consistency is preserved. We use the notion of conservative derivability, as defined by G. Wagner in [Wag91], as a proof-theoretic semantics for extended logic programs, and show that the three-valued completion semantics of a transformed program is sound and complete with respect to conservative derivability in the original extended logic program. ...