Deductive Search for Errors in Free Data Type Specifications Using Model Generation
- 285 Downloads
The presented approach aims at identifying false conjectures about free data types. Given a specification and a conjecture, the method performs a search for a model of an according counter specification. The model search is tailor-made for the semantical setting of free data types, where the fixed domain allows to describe models just in terms of interpretations. For sake of interpretation construction, a theory specific calculus is provided. The concrete rules are ‘executed’ by a procedure known as model generation. As most free data types have infinite domains, the ability of automatically solving the non-consequence problem is necessarily limited. That problem is addressed by limiting the instantiation of the axioms. This approximation leads to a restricted notion of model correctness, which is discussed. At the same time, it enables model completeness for free data types, unlike approaches based on limiting the domain size.
KeywordsModel Candidate Function Symbol Variable Assignment Object Logic Abstract Data Type
Unable to display preview. Download preview PDF.
- [Ahr01]Wolfgang Ahrendt. Deduktive Fehlersuche in Abstrakten Datentypen. 2001. Dissertation (preversion, in German), University of Karlsruhe, available under http://www.cs.chalmers.se/~ahrendt/cade02/diss.ps.gz.
- [Bac88]Leo Bachmair. Proof by consistency in equational theories. In Proc. Third Annual Symposium on Logic in Computer Science, Edinburgh, Scotland, pages 228–233. IEEE Press, 1988.Google Scholar
- [BT98]François Bry and Sunna Torge. A deduction method complete for refutation and finite satisfiability. In Proc. 6th European Workshop on Logics in AI (JELIA), volume 1489 of LNAI, pages 122–136. Springer-Verlag, 1998.Google Scholar
- [FH91]Hiroshi Fujita and Ryuzo Hasegawa. A model generation theorem prover in KL1 using a ramified-stack algorithm. In Koichi Furukawa, editor, Proceedings 8th International Conference on Logic Programming, Paris/France, pages 535–548. MIT Press, 1991.Google Scholar
- [FL96]Christian Fermüller and Alexander Leitsch. Hyperresolution and automated model building. Journal of Logic and Computation, 6(2), 1996.Google Scholar
- [GA99]Martin Giese and Wolfgang Ahrendt. Hilbert’s ∈-terms in Automated Theorem Proving. In Neil V. Murray, editor, Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, Saratoga Springs, USA, volume 1617 of LNAI, pages 171–185. Springer-Verlag, 1999.Google Scholar
- [MBI94]Raul Monroy, Alan Bundy, and Andrew Ireland. Proof plans for the correction of false conjectures. In Frank Pfenning, editor, Proc. 5th International Conference on Logic Programming and Automated Reasoning, Kiev, Ukraine, volume 822 of LNAI, pages 54–68. Springer-Verlag, 1994.Google Scholar
- [Pro92]Martin Protzen. Disproving conjectures. In D. Kapur, editor, Proc. 11th CADE, Albany/NY, USA, volume 607 of LNAI, pages 340–354. Springer-Verlag, 1992.Google Scholar
- [Pro96]Martin Protzen. Patching faulty conjectures. In Michael McRobbie and John Slaney, editors, Proc. 13th CADE, New Brunswick/NJ, USA, volume 1104 of LNCS, pages 77–91. Springer-Verlag, 1996.Google Scholar
- [RST01]Wolfgang Reif, Gerhard Schellhorn, and Andreas Thums. Flaw detection in formal specifications. In Rajeev Goré, Alexander Leitsch, and Tobias Nipkow, editors, Automated Reasoning, IJCAR 2001 Siena, Italy, June 18–23, 2001 Proceedings, volume 2083 of LNAI. Springer-Verlag, 2001.Google Scholar
- [Sla94]John Slaney. FINDER: finite domain enumerator. In Alan Bundy, editor, Proc. 12th CADE, Nancy/France, volume 814 of LNCS, pages 798–801. Springer-Verlag, 1994.Google Scholar
- [Thu98]Andreas Thums. Fehlersuche in Formalen Spezifikationen. diploma thesis, Fakultät für Informatik, Universität Ulm, 1998.Google Scholar
- [ZZ96]Jian Zhang and Hantao Zhang. Generating models by SEM. In Michael McRobbie and John Slaney, editors, Proc. 13th CADE, New Brunswick/NJ, USA, volume 1104 of LNCS, pages 309–327. Springer-Verlag, 1996.Google Scholar