Computer Science Logic and 8th Kurt Gödel Colloquium C.F.M. Vermeulen: More computation power for a denotational semantics for first order logic

Welcome and News Host Institutions Calls and Deadlines Program Social Program Registration Location and Venue Accommodation Committees Contact Colocated Events Authors' instructions

Print this page The paper starts from a denotational semantics for first order logic proposed by Apt (at the computational logic conference CL2000). He interprets first order logic as a programming language in the declarative paradigm, but different from the usual approach of logic programming. For his proposal Apt obtains soundness with respect to the standard interpretation of first order logic. Here we consider the expressivity (or: computation power) of the system proposed, i.e., the programs for which the semantics does not give error messages. To gain computational realism a decrease in expressivity compared to first order logic is inevitable. In Apt's proposal the expressivity was compared with logic programming with both positive and negative results. Here we consider three ways of improving the situation: replacing the conjunction-as-sequential-composition in the original proposal by a symmetric interpretation of conjunction; extending the framework with the option of recursive definitions by Clark completions; replacing the interpretation of disjunction-as-choice by an interpretation which is in the style of `backtracking': only produce an error message if all options lead to error. For each improvement we obtain a soundness result. The three improvements are developed independently in a way that makes sure that also their combination preserves soundness. The combination gives a considerable improvement of the expressivity of the denotational semantics that Apt proposed, both in the comparison with first order logic and in the comparison with logic programming. © 2002-2003 Kurt Gödel Society, Norbert Preining. 2003-06-04