Preuves infinies en Programmation logique

ABSTRACT. This paper focuses on the assignment of meaning to some nonterminating SLD derivations in logic programming. Several approaches have been developped by considering infinite elements in the universe of the discourse but none are complete. We investigate here infinite derivations over the domain of finite terms (i.e., derivations which do not compute infinite terms) and show they correspond to co-induction proofs. A sound and complete semantics for this class of derivations, based on the "logic programs as co-inductive definitions" paradigm, is defined. MOTS-CL

• Type: Conference
• Year: 2000
• Where: JFPLC
• Authors: Mathieu Jaume
• Keywords: Infinite Derivations, Infinite Elements, JFPLC 2000, JFPLC 2001, Nonterminating Sld Derivations