Model building by resolution | SpringerLink
Skip to main content
Springer Nature Link
Log in

Model building by resolution

  • Conference paper
  • First Online:
Computer Science Logic (CSL 1992)

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

Included in the following conference series:

  • 140 Accesses

Abstract

Resolution calculi are best known as basis for algorithms testing the unsatisfiability of sets of clauses. Only recently more attention is paid to the fact that various resolution refinements may also benefitly be employed as decision procedures for a wide range of decidable classes of clause sets. In this proof theoretic approach to the decision problem one usually tries to test for satisfiability by termination of complete resolution procedures. Building on such types of decidability results we show that, for certain classes of clause sets, we can extract (representations of) models from the set of resolvents generated by hyperresolution. The process of model construction proceeds in two steps: First hyperresolution is employed to arrive at a finite set of atoms that represents a description of an Herbrand-model. In a second step we extract from this set of atoms a full representation of a model with finite domain. We emphasize that no backtracking is needed in our model constructing algorithm.

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. C.-L. Chang and R.C.-T. Lee, Symbolic Logic and Mechanical Theorem Proving. Academic Press, New York and London, 1973.

    Google Scholar 

  2. R. Caferra and N. Zabel, Extending Resolution for Model Construction. In: Logics in AI (JELIA '90). Springer Verlag, LNCS 478 (1991), pp. 153–169.

    Google Scholar 

  3. B. Dreben and W.D. Goldfarb, The Decision Problem. Addison-Wesley, Massachusetts 1979.

    Google Scholar 

  4. C.G. Fermüller, Deciding some Horn Clause Sets by Resolution. In: Year-book of the Kurt-Gödel-Society 1989, Vienna 1990, pp. 60–73.

    Google Scholar 

  5. C.G. Fermüller, Deciding Classes of Clause Sets by Resolution. Ph.D. The-sis, Technical University Vienna, 1991.

    Google Scholar 

  6. C.G. Fermüller and A. Leitsch, Model Building by Resolution. Technical Report TUW-E185.2-FL1, TU Wien, 1992.

    Google Scholar 

  7. C.G. Fermüller, A. Leitsch, T. Tammet, and N. Zamov, Resolution Methods for the Decision Problem. To appear in LNCS, Springer Verlag.

    Google Scholar 

  8. J.-M. Hullot, Canonical Forms and Unification. In: 5th Conference on Automated Deduction. Springer Verlag, LNCS 87 (1980), pp. 250–263.

    Google Scholar 

  9. W.H. Joyner, Resolution Strategies as Decision Procedures. J. ACM 23,1 (July 1976), pp. 398–417.

    Article  Google Scholar 

  10. A. Leitsch, Deciding Horn Classes by Hyperresolution. In: CSL'89. Springer Verlag, LNCS 440 (1990), pp. 225–241.

    Google Scholar 

  11. A. Leitsch, Deciding Clause Classes by Semantic Clash Resolution. To appear in: Fundamenta Informaticae.

    Google Scholar 

  12. D. Loveland, Automated Theorem Proving — A Logical Basis. North Holland Publ. Comp. 1978.

    Google Scholar 

  13. R. Manthey and F. Bry, SATCHMO: A theorem prover implemented in Prolog. In: 9th Conference on Automated Deduction. Springer Verlag, LNCS 310 (1988), pp. 415–434.

    Google Scholar 

  14. H. Noll, A Note on Resolution: How to Get Rid of Factoring Without Loos-ing Completeness. In: 5th Conference on Automated Deduction. Springer Verlag, LNCS 87 (1980), pp. 250–263.

    Google Scholar 

  15. T. Tammet, Using Resolution for Deciding Solvable Classes and Building Finite Models. In: Baltic Computer Science. Springer Verlag, LNCS 502 (1991), pp. 33–64.

    Google Scholar 

  16. T. Tammet, Resolution Methods for Decision Problems and Finite Model Building. Dissertation, Department of Computer Science, Chalmers University of Technology. Chalmers/Göteburg, 1992.

    Google Scholar 

  17. S. Winker, Generation and Verification of Finite Models and Counterexamples Using an Automated Theorem Prover Answering Two Open Questions. J. of the ACM, Vol. 29/2, April 1982, pp. 273–284.

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institut für Computersprachen, Technische Universität Wien, Resselgasse 3/1, A-1040, Vienna, Austria

    Christian G. Fermüller & Alexander Leitsch

Authors
  1. Christian G. Fermüller
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Alexander Leitsch
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

E. Börger G. Jäger H. Kleine Büning S. Martini M. M. Richter

Rights and permissions

Reprints and permissions

Copyright information

© 1993 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Fermüller, C.G., Leitsch, A. (1993). Model building by resolution. In: Börger, E., Jäger, G., Kleine Büning, H., Martini, S., Richter, M.M. (eds) Computer Science Logic. CSL 1992. Lecture Notes in Computer Science, vol 702. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-56992-8_10

Download citation

  • DOI: https://doi.org/10.1007/3-540-56992-8_10

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-56992-3

  • Online ISBN: 978-3-540-47890-4

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics