Skip to main content
SpringerLink
Log in
Book cover

Kurt Gödel Colloquium on Computational Logic and Proof Theory

KGC 1993: Computational Logic and Proof Theory pp 132–143Cite as

The inverse of fitting's functional

  • Contributed Papers
  • Conference paper
  • First Online:

  • 162 Accesses

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 713))

Abstract

The evaluation of a goal for a logic program can be viewed as the search for an answer, written in the constraints language, that correctly implies the goal. We propose a small set of inference rules, correct w.r.t. the completion of a program and the Clark equational theory, which is strong enough to compute a complete set of answers for extended programs over the Herbrand constraint system. The basic step, the unfolding, is shown to realize, in a syntactic way, the inverse of what Fitting's functional computes in the semantic one. Then, using the fundamental result of Kunen, we can prove the completeness of our schema for the three valued consequences of the completion.

This is a preview of subscription content, log in via an institution.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. A. Bottoni. La riscrittura completa è l'inverso del funzionale di Fitting. Master's thesis, Dipartimento di Informatica, Università di Pisa, 1992. In italian.

    Google Scholar 

  2. A. Bottoni. CET Standard Forms. Technical report, Dipartimento di Informatica, Università di Pisa, 1993.

    Google Scholar 

  3. A. Bottoni. Complete Constraints Extraction for First Order CLP. Technical report, Dipartimento di Matematica Pura ed Applicata, Università di Padova, 1993.

    Google Scholar 

  4. P. Bruscoli, F. Levi, G. Levi, and M. C. Meo. Compilative constructive negation in CLP. Technical report, Dipartimento di Informatica, Università di Pisa, 1992.

    Google Scholar 

  5. D. Chan. Constructive Negation Based on the Completed Database. In R. A. Kowalski and K. A. Bowen, editors, Proc. Fifth Int'l Conf. on Logic Programming, pages 111–125. The MIT Press, Cambridge, Mass., 1988.

    Google Scholar 

  6. D. Chan. An Extension of Constructive Negation and its Application in Coroutining. In E. Lusk and R. Overbeek, editors, Proc. North American Conf. on Logic Programming'89, pages 477–493. The MIT Press, Cambridge, Mass., 1989.

    Google Scholar 

  7. K. L. Clark. Negation as Failure. In H. Gallaire and J. Minker, editors, Logic and Data Bases, pages 293–322. Plenum Press, New York, 1978.

    Google Scholar 

  8. M. Fitting. A Kripke-Kleene semantics for logic programs. Journal of Logic Programming, 2:295–312, 1985.

    Google Scholar 

  9. K. Kunen. Negation in logic programming. Journal of Logic Programming, 4:289–308, 1987.

    Google Scholar 

  10. K. Kunen. Signed Data Dependencies in Logic Programs. Journal of Logic Programming, 7(3):231–245, 1989.

    Google Scholar 

  11. J.-L. Lassez, M. J. Maher, and K. Marriott. Unification Revisited. In J. Minker, editor, Foundations of Deductive Databases and Logic Programming, pages 587–625. Morgan Kaufmann, Los Altos, Ca., 1988.

    Google Scholar 

  12. J. W. Lloyd. Foundations of Logic Programming. Springer-Verlag, Berlin, 1987.

    Google Scholar 

  13. J. W. Lloyd and R. W. Topor. Making PROLOG More Expressive. Journal of Logic Programming, 1(3):225–240, 1984.

    Google Scholar 

  14. D. Lugiez. A deduction procedure for first order programs. In G. Levi and M. Martelli, editors, Proc. Sixth Int'l Conf. on Logic Programming, pages 585–600. The MIT Press, Cambridge, Mass., 1989.

    Google Scholar 

  15. J. A. Robinson. Beyond LOGLISP: combining functional and relational programming in a reduction setting. In D. Michie and Hayes-Michie, editors, Machine Intelligence 11. Oxford University Press, 1985.

    Google Scholar 

  16. T. Sato, F. Motoyoshi. A Complete Top-down Interpreter for First Order Programs. In V. Saraswat and K. Ueda, editors, Proc. International Symposium on Logic Programming'91, pages 35–53. The MIT Press, Cambridge, Mass., 1991.

    Google Scholar 

  17. R. F. Stärk. A Complete Axiomatization of the Three valued Completion of Logic Programs. Journal of Logic and Computation, 1(6):811–834, 1991.

    Google Scholar 

  18. P. J. Stuckey. Constructive Negation for Constraint Logic Programming. In Proc. Sixth IEEE Symp. on Logic In Computer Science. IEEE Comp. Soc. Press, 1991.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dipartimento di Matematica Pura ed Applicata, Università di Padova, Via Belzoni 7, 35131, Padova, Italia

    Alberto Bottoni

  2. Dipartimento di Informatica, Univeristà di Pisa, Corso Italia 40, 56125, Pisa, Italia

    Giorgio Levi

Authors
  1. Alberto Bottoni
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Giorgio Levi
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Georg Gottlob Alexander Leitsch Daniele Mundici

Rights and permissions

Reprints and permissions

Copyright information

© 1993 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Bottoni, A., Levi, G. (1993). The inverse of fitting's functional. In: Gottlob, G., Leitsch, A., Mundici, D. (eds) Computational Logic and Proof Theory. KGC 1993. Lecture Notes in Computer Science, vol 713. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0022561

Download citation

  • DOI: https://doi.org/10.1007/BFb0022561

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-57184-1

  • Online ISBN: 978-3-540-47943-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation