×

zbMATH — the first resource for mathematics

Intuitionistic three-valued logic and logic programming. (English) Zbl 0771.68084
Summary: We study the semantics of logic programs with the help of trivalued logic, introduced by J. Y. Girard [Three-Valued Logic and Cut- Elimination: The Actual Meaning of Takeuti’s Conjecture, Diss. Math., Warszawa, 45 p. (1976; Zbl 0357.02027)].
Trivalued sequent calculus enables to extend easily the results of classical SLD-resolution to trivalued logic. Moreover, if one allows negation in the head and in the body of Horn clauses, one obtains a natural semantics for such programs regarding these clauses as axioms of a theory written in the intuitionistic fragment of that logic.
Finally, we define in the same calculus an intuitionistic trivalued version of Clark’s completion, which gives us a declarative semantics for programs with negation in the body of the clauses, the evaluation method being SLDNF-resolution.
MSC:
68Q55 Semantics in the theory of computing
68N17 Logic programming
PDF BibTeX XML Cite
Full Text: DOI EuDML
References:
[1] 1. S. CERRITO, Negation as Failure: a Linear Axiomatization, Rapport de recherche, L.R.I., Orsay, 1988. · Zbl 0754.68025
[2] 2. K. L. CLARK, Négation as Failure, in Logic and Database, H. GALLAIRE and J. MINER Eds., Plenum Press, New York, 1978, pp.293-322.
[3] 3. J. P. DELAHAYE, Chaînage avant et calcul de modèles booléens et trivalués, Expert Systems and their applications, Avignon, 1987.
[4] 4. M. FITTING, A Kripke-Kleene Semantics for General Logic programs, J. Logic Programming, 1985, 2, pp. 295-321. Zbl0589.68011 MR818647 · Zbl 0589.68011 · doi:10.1016/S0743-1066(85)80005-4
[5] 5. J. GALLIER, Logic for Computer Science: Foundations of Automatic Theorem proving, Harper and Row, New York, 1986. Zbl0605.03004 · Zbl 0605.03004
[6] 6. G. GENTZEN, Collected works, SZABO Ed., North Holland, Amsterdam, 1969. MR262050
[7] 7. J. Y. GIRARD, Three-Valued Logic and Cut-Elimination: The Actual Meaning of Takeuti’s Conjecture, Dissertationes Math., Warszawa, 1976. Zbl0357.02027 · Zbl 0357.02027
[8] 8. J. Y. GIRARD, Théorie de la démonstration, Cours de 3^\circ cycle, Université Paris-VII, 1986.
[9] 9. J. Y. GIRARD, Proof Theory and Logical Complexity, 1987, 1, Napoli, Bibliopolis. Zbl0635.03052 MR903244 · Zbl 0635.03052
[10] 10. K. KUNEN, Negation in logic programming, J. Logic programming, 1987, 4, pp. 289-308. Zbl0655.68018 MR916936 · Zbl 0655.68018 · doi:10.1016/0743-1066(87)90007-0
[11] 11. J. W. LLOYD, Foundations of Logic programming, Second Edition, Springer Verlag, Berlin, 1987. Zbl0668.68004 MR911272 · Zbl 0668.68004
[12] 12. P. H. SCHMITT, Computational Aspects of Three Valued Logic, Proc. 8th Conf. Automated Déduction, Lecture Notes in Comput. Sci., 1986, 230, Springer-Verlag, pp. 190-198. Zbl0644.03015 MR876502 · Zbl 0644.03015
[13] 13. J. C. SHEPHERDSON, Negation as Failure: A Comparison of Clark’s Completed Data Base and Reiter’s Closes World Assumption, J. Logic Programming, 1984, 1, pp. 51-81. Zbl0575.68094 MR754304 · Zbl 0575.68094 · doi:10.1016/0743-1066(84)90023-2
[14] 14. J. C. SHEPHERDSON, Negation as Failure II, J. Logic programming, 1985, 3, pp. 185-202. Zbl0603.68094 MR817854 · Zbl 0603.68094 · doi:10.1016/0743-1066(85)90018-4
[15] 15. J. C. SHEPHERDSON, Negation in Logic Programming, in J. MINKER Éd., Foundations of Deductive Databases and Logic Programming, Morgan Kaufman, Los Altos, 1988, pp. 19-88. Zbl0718.68020 MR938982 · Zbl 0718.68020
[16] 16. M. H. VAN EMDEN and R. KOWALSKI, The Semantics of Predicate Logic as a Programming Language, J. Assoc. Comput. Mach., 1976, 23, pp. 733-742. Zbl0339.68004 MR455509 · Zbl 0339.68004 · doi:10.1145/321978.321991
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.