A Modal Semantics of Negation in Logic Programming

Article type: Research Article

Authors: Balbiani, Philippe

Affiliations: Institut de Recherche en Informatique de Toulouse, 118 route de Narbonne, 31062 Toulouse Cedex, France

Abstract: The beauty of modal logics and their interest lie in their ability to represent such different intensional concepts as knowledge, time, obligation, provability in arithmetic, … according to the properties satisfied by the accessibility relations of their Kripke models (transitivity, reflexivity, symmetry, well-foundedness, …). The purpose of this paper is to study the ability of modal logics to represent the concepts of provability and unprovability in logic programming. The use of modal logic to study the semantics of logic programming with negation is defended with the help of a modal completion formula. This formula is a modal translation of Clack’s formula. It gives soundness and completeness proofs for the negation as failure rule. It offers a formal characterization of unprovability in logic programs. It characterizes as well its stratified semantics.

DOI: 10.3233/FI-1992-163-403

Journal: Fundamenta Informaticae, vol. 16, no. 3-4, pp. 231-262, 1992