[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to main content
Springer Nature Link
Log in

A significant extension of logic programming by adapting model building rules

  • Conference paper
  • First Online:
Extensions of Logic Programming (ELP 1996)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 1050))

Included in the following conference series:

Abstract

A method by the authors for automated model building is extended and specialized in a natural way in order to increase the possibilities of logic programming. A rather complete, though reasonably short, description of the ideas and technicalities of the former method is given in order to make the paper self-contained. Specialization of several key rules permits to obtain three main theoretical results concerning extensions of logic programming: non-ground negative facts as well as inductive consequences can be deduced from programs. Goals containing negations, quantifications and logical connectives are allowed. It is proven that the proposed extension is strictly more powerful than SLDNF. Several non-trivial running examples show evidence of the interest of our approach. Last but not least, a nice side effect exploits the model building capabilities of the approach: it is shown on one representative example how the method can be used to detect (and to correct) errors in logic programs. Main lines of future research are given.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Christophe BOURELY, Ricardo CAFERRA, and Nicolas PELTIER. A method for building models automatically. Experiments with an extension of OTTER. In Proc. of CADE-12, pages 72–86. Springer Verlag, 1994. LNAI 814.

    Google Scholar 

  2. Hubert COMON and Pierre LESCANNE. Equational problems and disunification. Journal of Symbolic Computation, 7:371–475, 1989.

    Google Scholar 

  3. Keith L. CLARK. Negation as failure. In H. Gallaire and J. Minker, editors, Logic and Databases, pages 293–322. Plenum Press, 1978.

    Google Scholar 

  4. Ricardo CAFERRA and Nicolas PELTIER. Verifying and correcting a large class of logic programs. Submitted, 199?

    Google Scholar 

  5. Ricardo CAFERRA and Nicolas PELTIER. Model building and interactive theory discovery. In Proceeding of Tableaux'95, LNAI 918, pages 154–168. Springer-Verlag, 1995.

    Google Scholar 

  6. Ricardo CAFERRA and Nicolas ZABEL. Extending resolution for model construction. In Logics in AI, JELIA'90, pages 153–169. Springer-Verlag, LNAI 478, 1990.

    Google Scholar 

  7. Ricardo CAFERRA and Nicolas ZABEL. A method for simultaneous search for refutations and models by equational constraint solving. Journal of Symbolic Computation, 13:613–641, 1992.

    Google Scholar 

  8. H. GELERNTER, J.R. HANSEN, and D.W. LOVELAND. Empirical explorations of the geometry theorem-proving machine. In Jörg Siekmann and Graham Wrightson, editors, Automation of Reasoning, vol. 1, pages 140–150. Springer-Verlag 1983, 1983. Originally published in 1960.

    Google Scholar 

  9. John W. LLOYD. Foundations of Logic Programming. Springer Verlag, second edition, 1987.

    Google Scholar 

  10. Denis LUGIEZ. A deduction procedure for first order programs. In F. Levi and M. Martelli, editors, Proceedings of the sixth International Conference on Logic Programming, pages 585–599. The MIT Press, July 1989.

    Google Scholar 

  11. A.I. MAL'CEV. The Metamathematics of Algebraic Systems: Collected Papers 1936–1967, chapter Axiomatizable classes of locally free algebra of various type. Benjamin Franklin Wells III editor, North Holland, 1971. chapter 23.

    Google Scholar 

  12. Nicolas PELTIER. Increasing the capabilities of model building by constraint solving with terms with integer exponents. To appear, 199?

    Google Scholar 

  13. J.A. ROBINSON. Logic Programming-past, present and future-. New Generation Computing, 1:107–124, 1983.

    Google Scholar 

  14. J.A. ROBINSON. Logic and Logic Programming. Communications of the ACM, 35(3):40–65, March 1992.

    Google Scholar 

  15. Larry WOS and William McCUNE. Automated theorem proving and logic programming: a natural symbiosis. Journal of Logic Programming, 11(1):1–53, july 1991.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LIFIA-IMAG, 46, Avenue Félix Viallet, 38031, Grenoble Cedex, France

    Ricardo Caferra & Nicolas Peltier

Authors
  1. Ricardo Caferra
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Nicolas Peltier
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Roy Dyckhoff Heinrich Herre Peter Schroeder-Heister

Rights and permissions

Reprints and permissions

Copyright information

© 1996 Springer-Verlag

About this paper

Cite this paper

Caferra, R., Peltier, N. (1996). A significant extension of logic programming by adapting model building rules. In: Dyckhoff, R., Herre, H., Schroeder-Heister, P. (eds) Extensions of Logic Programming. ELP 1996. Lecture Notes in Computer Science, vol 1050. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60983-0_4

Download citation

  • DOI: https://doi.org/10.1007/3-540-60983-0_4

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-60983-4

  • Online ISBN: 978-3-540-49751-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation