Model Elimination with Simplification and its Application to Software Verification

  • Peter Baumgartner
  • Dorothea Schäfer
Conference paper
Part of the Advances in Computing Science book series (ACS)


Software verification is known to be a notoriously difficult application area for automated theorem provers. Consequently, this is the domain of interactive systems, such as KIV [Reif et al., 1997], HOL [Gordon and Melham, 1993], Isabelle [Nipkow and Paulson, 1992] and PVS [Owre et al., 1992]. The work described here aims to demonstrate that automated theorem provers (ATPs) can be successfully incorporated into such systems in order to relieve the user from some interactions. More specifically, we describe our approach of coupling the interactive program verification system KIV [Reif et al , 1997] with our automated theorem prover PROTEIN [Baumgartner and Furbach, 1994].


Inference Rule Simplification Rule Static Simplification Proof Obligation Model Elimination 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [Astrachan, 1992]
    Owen L. Astrachan. Investigations in Model Elimination based Theorem Proving PhD thesis, Duke University, 1992. Technical Report CS-1992–21.Google Scholar
  2. [Bachmair and Ganzinger, 1998]
    Leo Bachmair and Harald Ganzinger. Chapter 11: Equational Reasoning in Saturation-Based Theorem Proving. In Wolfgang Bibel and Peter H. Schmitt, editors, Automated Deduction. A Basis for Applications, volume I: Foundations. Calculi and Refinements, pages 353–398. Kluwer Academic Publishers, 1998.Google Scholar
  3. [Baumgartner and Furbach, 1994]
    Peter Baumgartner and Ulrich Furbach. PRO-TEIN: A PROver with a Theory Extension Interface. In A. Bundy, editor, Au-tomated Deduction - CADE-12,volume 814 of Lecture Notes in Artificial Intelligence,pages 769–773. Springer, 1994. Available in the WWW, URL:http://www.uni-koblenz. de/ag-ki/Systems/PROTEIN/.
  4. [Beckert and Posegga, 1995]
    Bernhard Beckert and Joachim Posegga. leanT’P: Lean tableau-based deduction. Journal of Automated Reasoning, 15 (3): 339–358, 1995.Google Scholar
  5. [Boyer and Moore, 1988]
    R.S. Boyer and J.S. Moore. A Computational Logic. Academic Press, 1988.Google Scholar
  6. [Bronsard and Reddy, 1992]
    Francois Bronsard and Uday S. Reddy. Reduction Techniques for First-Order Reasoning. In M. Rusinowitch and J.L. Rémy, editors, Proceedings of the Third International Workshop on Conditional Term Rewriting Systems, pages 242–256. Springer-Verlag, July 1992. LNCS 656.Google Scholar
  7. [Bruning, 1995]
    S. Brüning. Exploiting Equivalences in Connection Calculi. Journal of the IGPL, 3 (6): 857–886, 1995.MATHCrossRefGoogle Scholar
  8. [Chang and Lee, 1973]
    C. Chang and R. Lee. Symbolic Logic and Mechanical Theorem Proving. Academic Press, 1973.Google Scholar
  9. [Fitting, 1990]
    M. Fitting. First Order Logic and Automated Theorem Proving. Texts and Monographs in Computer Science. Springer, 1990.MATHCrossRefGoogle Scholar
  10. [Gordon and Melham, 1993]
    M. J. C. Gordon and T. F. Melham, editors. Introduction to HOL: A theorem proving environment for higher order logic. Cambridge University Press, 1993.Google Scholar
  11. [Kaufmann and Moore, 1996]
    M. Kaufmann and J.S. Moore. Ac12: An industrial strength version of nqthm. In Proceedings of Eleventh Annual Conference on Computer Assurance (COMPASS-96), pages 23–34 IEEE Computer Society Press, 1996.Google Scholar
  12. [Lee and Plaisted, 1989]
    Shie-Jue Lee and David A. Plaisted. Reasoning with Predicate Replacement, 1989.Google Scholar
  13. [Loveland, 1969]
    D. Loveland. A Simplified Version for the Model Elimination Theorem Proving Procedure. JACM, 16 (3), 1969.Google Scholar
  14. [McCune, 1994]
    William W. McCune. OTTER 3.0 reference manual and guide. Technical Report ANL-94/6, National Laboratory, Argonne, IL, 1994.CrossRefGoogle Scholar
  15. [Nipkow and Paulson, 1992]
    Tobias Nipkow and Lawrence C. Paulson. Isabelle-91. In D. Kapur, editor, Proceedings of the 11th International Conference on Automated Deduction,pages 673676, Saratoga Springs, NY, 1992. Springer-Verlag LNAI 607. System abstract.Google Scholar
  16. [Schäfer, 1998]
    Dorothea Schäfer. Simplification in model elimination. Master’s thesis, Universität Koblenz, 1998. To appear.Google Scholar
  17. [Schellhorn and Reif, 1997]
    Gerhard Schellhorn and Wolfgang Reif. Proving properties of finite enumerations: A problem set for automated theorem provers. Technical report, University of Ulm, Dept. of Computer Science, 1997. URL:
  18. [Schmitt and Wernecke, 1989]
    P.H. Schmitt and W. Wernecke. Tableau calculus for sorted logics. In Sorts and Types in Artificial Intelligence, volume 418 of Lecture Notes in Artificial Intelligence, pages 49–60. Springer, 1989.Google Scholar

Copyright information

© Springer-Verlag Wien 1999

Authors and Affiliations

  • Peter Baumgartner
  • Dorothea Schäfer

There are no affiliations available

Personalised recommendations