Deductive Search for Errors in Free Data Type Specifications Using Model Generation

  • Wolfgang Ahrendt
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2392)


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.


Model Candidate Function Symbol Variable Assignment Object Logic Abstract Data Type 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [Ahr01]
    Wolfgang Ahrendt. Deduktive Fehlersuche in Abstrakten Datentypen. 2001. Dissertation (preversion, in German), University of Karlsruhe, available under
  2. [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
  3. [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
  4. [CP00]
    Ricardo Caferra and Nicolas Peltier. Combining enumeration and deductive techniques in order to increase the class of constructible infinite models. Journal of Symbolic Computation, 29:177–211, 2000.zbMATHCrossRefMathSciNetGoogle Scholar
  5. [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
  6. [FL96]
    Christian Fermüller and Alexander Leitsch. Hyperresolution and automated model building. Journal of Logic and Computation, 6(2), 1996.Google Scholar
  7. [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
  8. [MB88]
    Rainer Manthey and François Bry. SATCHMO: A theorem prover implemented in Prolog. In Proceedings 9th Conference on Automated Deduction, volume 310 of LNCS, pages 415–434. Springer-Verlag, 1988.CrossRefGoogle Scholar
  9. [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
  10. [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
  11. [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
  12. [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
  13. [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
  14. [Thu98]
    Andreas Thums. Fehlersuche in Formalen Spezifikationen. diploma thesis, Fakultät für Informatik, Universität Ulm, 1998.Google Scholar
  15. [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

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Wolfgang Ahrendt
    • 1
  1. 1.Department of Computing ScienceChalmers University of TechnologyGöteborgSweden

Personalised recommendations