zbMATH — the first resource for mathematics

Declarative modeling of the operational behavior of logic languages. (English) Zbl 0699.68113
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.
Reviewer: S.Vorobyov

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03B35 Mechanization of proofs and logical operations
68Q55 Semantics in the theory of computing
Full Text: DOI
[1] Apt, K.R.; Van Emden, M., Contributions to the theory of logic programming, J. ACM, 29, 841-862, (1982) · Zbl 0483.68004
[2] Bruynooghe, M.; Janssens, G.; Callebaut, A.; Demoen, B., Abstract interpretation: towards the global optimisation of prolog programs, (), 192-204
[3] Clark, K.L., Predicate logic as a computational formalism, ()
[4] Deransart, P.; Ferrand, G., Programmation en logique avec negation: presentation formelle, ()
[5] Drabent, W.; Maluszynski, J., Inductive assertion method for logic programs, (), 167-181
[6] Van Emden, M.; Kowalski, R.A., The semantics of predicate logic as a programming language, J. ACM, 23, 733-742, (1976) · Zbl 0339.68004
[7] Falaschi, M.; Levi, G., Operational and fixpoint semantics of committed-choice logic languages, ()
[8] Ferrand, G., A reconstruction of logic programming with negation, ()
[9] Ferrand, G., Error diagnosis in logic programming, an adaptation of E.Y. Shapiro’s method, J. logic programming, 4, 177-198, (1987) · Zbl 0623.68005
[10] Golson, W.G., Toward a declarative semantics for infinite objects in logic programming, () · Zbl 0644.68025
[11] Henschen, L.; Wos, L., Unit refutations and Horn sets, J. ACM, 21, 590-605, (1974) · Zbl 0296.68093
[12] Jaffar, J.; Lassez, J.-L.; Maher, M.J., A logic programming language scheme, (), 441-468
[13] Jaffar, J.; Lassez, J.-L., Constraint logic programming, Proc. SIGACT-SIGPLAN symp. on principles of programming languages, 111-119, (1987)
[14] Levi, G.; Palamidessi, C., The declarative semantics of Read-only variables, (), 128-137
[15] Levi, G.; Palamidessi, C., An approach to the declarative semantics of synchronization of logic languages, ()
[16] Levi, G., A new declarative semantics for GHC, (January 1988), Technical Report, ICOT
[17] Lloyd, J.W., Foundations of logic programming, (1984), Springer Berlin · Zbl 0547.68005
[18] Tamaki, H.; Sato, T., Unfold/fold transformation of logic programs, Proc. 2nd internat. logic programming conf., 127-138, (1984), Uppsala, Sweden
[19] Yamasaki, S.; Yoshida, M.; Doshita, S., A fixpoint semantics of Horn sentences based on substitution sets, Theoret. comput. sci., 51, 309-324, (1987) · Zbl 0641.68147
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.