Skip to main content
SpringerLink
Log in

Extending resolution for model construction

  • Selected Papers
  • Conference paper
  • First Online:
Logics in AI (JELIA 1990)

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

Included in the following conference series:

Abstract

A method is proposed to systematize the simultaneous search for a refutation and Herbrand models of a given conjecture. It is based on an extension of resolution using equational problems and the inference system included in the method is proved to be sound and refutational complete. For some classes of formulae the method is indeed a decision procedure. Some examples of model construction — including one for which other resolution based decision procedures fail to detect satisfiability — are developed in detail.

Models are built by constructing relations on Herbrand universe. The relationship between these models and finite ones is established. The class of these constructible relations is precisely characterized. Some of the rules introduced, in order to extend resolution, are essentially new. Their necessity in constructing models is proved. A brief comparison with existing methods which bear similarity with ours, either in the use of constraints (a particular case of equational problems) or in the search of a model, shows the originality of our proposal.

This work has been supported by the MEDLAR BRA Esprit project and the PRC - IA - CRNS — MRT.

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.

References

  1. W. Ackermann. Solvable cases for the decision problem. North-Holland, 1954.

    Google Scholar 

  2. W. W. Bledsoe and D. W. Loveland, editors. Automated theorem proving after 25 years, volume 29. Contemporary Mathematics, 1984.

    Google Scholar 

  3. T. Boy de la Tour, R. Caferra, and G. Chaminade. Some tools for an inference laboratory (atinf). In Proc. of CADE 9, pages 744–745. Springer-Verlag LNCS 310, 1988.

    Google Scholar 

  4. H. Bürckert. Solving disequations in equational theories. In Proc. of CADE 9, pages 517–526. Springer-Verlag LNCS 310, 1988.

    Google Scholar 

  5. R. Caferra and N. Zabel. Une extension des tableaux sémantiques utilisant les problèmes équationnels pour guider la recherche de modèles et de réfutations. In Actes 3ème Journées Nationales PRC-GRD Intelligence Artificielle, pages 213–222. Éd. Hèrmes, 1990.

    Google Scholar 

  6. H. Comon. Disunification: a survey. Technical Report 540, L.R.I, Université Paris-Sud, 1990. to appear in “Festschrift for Robinson” (J.L. Lassez and G.Plotkin, eds.) MIT Press 1990.

    Google Scholar 

  7. H. Comon and P. Lescanne. Equational problem and disunification. JSC, 7:371–425, 1989.

    Google Scholar 

  8. V. J. Digricoli and M. C. Harrison. Equality based binary resolution. JACM, 33(2):253–289, 1986.

    Google Scholar 

  9. B. Dreben and W. D. Goldfarb. The decision problem — Solvable Classes of Quantificational Formulas. Addison-Wesley, 1979.

    Google Scholar 

  10. J. H. Gallier. Logic for Computer Science. Harper & Row, 1986.

    Google Scholar 

  11. J. Jaffar and J.-L. Lassez. Constraint logic programming. In Proc. of 14th ACM Symp. on Princ. of Prog. Lang., pages 111–119, Munich, 1987.

    Google Scholar 

  12. W. H. Joyner. Resolution strategies as decision procedures. JACM, 23(3):253–417, 1976.

    Google Scholar 

  13. C. Kirchner and H. Kirchner. Constrained equational reasoning. In Proc of the ACM SIGSAM — Int. Symp. Symbolic and Algebraic Computation, pages 382–389, Portland, U.S.A, 1989.

    Google Scholar 

  14. C. Kirchner and P. Lescanne. Solving disequations. Technical Report 686, INRIA, 1987.

    Google Scholar 

  15. D. W. Loveland. Automatic Theorem Proving: a logical basis. North Holland, 1978.

    Google Scholar 

  16. M. Rusinowitch. Démonstration automatique par des techniques de réécriture. Inter Editions, Paris, 1989.

    Google Scholar 

  17. M. E. Stickel. Automated deduction by theory resolution. JAR, 1(4):333–355, 1985.

    Google Scholar 

  18. S. Winker. Generation and verification of finite models and counter-examples using an automated theorem prover answering two open questions. JACM, 29(2):273–284, 1982.

    Google Scholar 

  19. L. Wos. Automated reasoning: 33 basic research problems. Prentice-Hall, 1988.

    Google Scholar 

  20. L. Wos and S. Winker. Open questions solved with the assistance of AURA, 1984. in [2].

    Google Scholar 

  21. N. Zamov. On a bound for a complexity of terms in the resolution method. In Proc. Steklov of Inst. Math. 121, pages 1–10, 1972.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Laboratoire d'Informatique Fondamentale et d'Intelligence Artificielle, Imag-Cnrs, 46, Av. F. Viallet, 38031, Grenoble, France

    Ricardo Caferra & Nicolas Zabel

Authors
  1. Ricardo Caferra
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Nicolas Zabel
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

J. van Eijck

Rights and permissions

Reprints and permissions

Copyright information

© 1991 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Caferra, R., Zabel, N. (1991). Extending resolution for model construction. In: van Eijck, J. (eds) Logics in AI. JELIA 1990. Lecture Notes in Computer Science, vol 478. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0018439

Download citation

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

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

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

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation