Model Elimination with Simplification and its Application to Software Verification
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].
KeywordsInference Rule Simplification Rule Static Simplification Proof Obligation Model Elimination
Unable to display preview. Download preview PDF.
- [Astrachan, 1992]Owen L. Astrachan. Investigations in Model Elimination based Theorem Proving PhD thesis, Duke University, 1992. Technical Report CS-1992–21.Google Scholar
- [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
- [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/.
- [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
- [Boyer and Moore, 1988]R.S. Boyer and J.S. Moore. A Computational Logic. Academic Press, 1988.Google Scholar
- [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
- [Bruning, 1995]
- [Chang and Lee, 1973]C. Chang and R. Lee. Symbolic Logic and Mechanical Theorem Proving. Academic Press, 1973.Google Scholar
- [Fitting, 1990]
- [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
- [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
- [Lee and Plaisted, 1989]Shie-Jue Lee and David A. Plaisted. Reasoning with Predicate Replacement, 1989.Google Scholar
- [Loveland, 1969]D. Loveland. A Simplified Version for the Model Elimination Theorem Proving Procedure. JACM, 16 (3), 1969.Google Scholar
- [McCune, 1994]
- [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
- [Schäfer, 1998]Dorothea Schäfer. Simplification in model elimination. Master’s thesis, Universität Koblenz, 1998. To appear.Google Scholar
- [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:http://www.informatik.uniulm.de/pm/kiv/setheo/enum.ps.
- [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