Declarative modeling of the operational behavior of logic languages (Q913530)

A new declarative semantics for logic programs is introduced and investigated. This new semantics differs essentially from the standard van Emden-Kowalsky semantics for logic programs, allowing the presence of atoms with variables in interpretations. The latter gives possibility to model the truth of universal formulae directly and to prove a more elegant completeness theorem than the standard one. Two types of new semantics based on upwards closure and subset properties imposed on sets of atoms in interpretations are studied and compared. It is proved that both types of interpretations form complete lattices. These new semantics are shown to capture the difference between effectively computable answers and answers obtainable by instantiations of universally quantified variables. As the authors argue, this fills the gap between operational and declarative semantics existing in the standard semantics for logic programs. Counterparts of results on classical Herbrand model semantics, including existence of minimal models, fixpoint characterization, etc., are shown to hold for the new semantics. Also, a stronger versions of soundness and completeness theorems for SLD-resolution are proved. Guidelines for future research, including characterization of finite failure sets, the description of semantics for logical programs with negation and universally quantified atoms are sketched.