and A. Momigliano 1 M. Ornaghi 2 and 1Department of Philosophy, Carnegie Mellon University, 15213 PittsburghPA, USA. E-mail: email@example.com 2Dipartimento di Scienze dell'Informazione, Universita' degli studi di Milano, Via Comelico 39/41, Milano, Italy. E-mail: firstname.lastname@example.org
The aim of this paper is to show the fruitfulness and fecundity of the authors' proof-theoretic analysis of logic programming (both for definite and normal programs). It is based on a simple logical framework that goes under the name of regular search spaces. The challenge faced here is to give a treatment in proof-theoretic terms of the issue of negation, which has been one of the toughest problems that has plagued logic programming from its very beginning. While negation-as-failure (NF) has been overwhelmingly the more widespread answer, its intrinsic limitations have made it a rather unsatisfactory solution. In the present paper it is first contended that the notion of regularity offers a better understanding of the traditional theory of NF, and second a firm yet very simple and natural basis for a form of constructive negation, in the sense of Chan, Stuckey and Harland. A version of constructive negation is presented, based on the notion of regular splitting, a transformation technique where the failure axiom(s) of a predicate occurring negatively in a program are split into new clauses according to a covering of the underlying signature.
Keywords: Logic programming, proof-theory, negation-as-failure, constructive negation, search spaces
Part of the OUP Journal of Logic and Computation WWW service
Click here to register with OUP.
This page is maintained by OUP admin
Part of the OUP Journals World Wide Web service.
Last modification: 22 Jul 1997
Copyright© Oxford University Press, 1997.