Contributions to the Theory of Logic Programming

Abstract

Horn clauses of first-order predicate logic can be regarded as a high-level programming language when SLD-resoluUon, a special-purpose resolution theorem prover, is used as interpreter. Consequently, the semantics of Horn clauses can be studied both by model-theoreuc and fixpomt methods (in the sense of Scott). This posslbihty is exploited here by identifying the least (greatest) fixpomt with a least (greatest) model Successful termination of SLD-resolution is characterized by least fixpomts A semantic characterization of t'mlte failure of SLD-resoluuon is given, which coincides with the greatest fixpomt only for a special case of clauses. It is shown that nondetermmistlc flowchart schemata of bounded nondeterminaey are modeled by this special case; the connection between finite fadure and greatest fixpomt is then used to give a semantic characterization of termmauon, blocking, and nontermination of such flowchart schemata Categories and Subject Descriptors" F 3 1 ILogics and Meanings of Programs]' Speofymg and Verifying and Reasoning about Programs--logics of programs, F 4.1 [Mathematlcal Logic and Formal Languagesl Mathematical Logic--logic programming, 1 2 3 [Artificial Intelligencel. Deduction and Theorem Proving-logic programming