Skip to main content
SpringerLink
Log in
Book cover

International Conference on Logic for Programming Artificial Intelligence and Reasoning

LPAR 2010: Logic for Programming, Artificial Intelligence, and Reasoning pp 127–141Cite as

Generating Counterexamples for Structural Inductions by Exploiting Nonstandard Models

  • Conference paper

  • 786 Accesses

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 6397))

Abstract

Induction proofs often fail because the stated theorem is noninductive, in which case the user must strengthen the theorem or prove auxiliary properties before performing the induction step. (Counter)model finders are useful for detecting non-theorems, but they will not find any counterexamples for noninductive theorems. We explain how to apply a well-known concept from first-order logic, nonstandard models, to the detection of noninductive invariants. Our work was done in the context of the proof assistant Isabelle/HOL and the counterexample generator Nitpick.

Research supported by the DFG grant Ni 491/11-1.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Ahrendt, W.: Deductive search for errors in free data type specifications using model generation. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 211–225. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  2. Berghofer, S., Nipkow, T.: Random testing in Isabelle/HOL. In: Cuellar, J., Liu, Z. (eds.) SEFM 2004, pp. 230–239. IEEE C.S., Los Alamitos (2004)

    Google Scholar 

  3. Berghofer, S., Wenzel, M.: Inductive datatypes in HOL—lessons learned in formal-logic engineering. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Théry, L. (eds.) TPHOLs 1999. LNCS, vol. 1690, pp. 19–36. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  4. Blanchette, J.C.: Relational analysis of (co)inductive predicates (co)inductive datatypes, and (co)recursive functions. In: Fraser, G., Gargantini, A. (eds.) TAP 2010. LNCS, vol. 6143, pp. 117–134. Springer, Heidelberg (2010)

    Google Scholar 

  5. Blanchette, J.C., Nipkow, T.: Nitpick: A counterexample generator for higher-order logic based on a relational model finder. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 131–146. Springer, Heidelberg (2010)

    Google Scholar 

  6. Caferra, R., Leitsch, A., Peltier, N.: Automated Model Building. Applied Logic, vol. 31. Springer, Heidelberg (2004)

    MATH  Google Scholar 

  7. Church, A.: A formulation of the simple theory of types. J. Symb. Log. 5, 56–68 (1940)

    Article  MathSciNet  MATH  Google Scholar 

  8. Claessen, K., Svensson, H.: Finding counter examples in induction proofs. In: Beckert, B., Hähnle, R. (eds.) TAP 2008. LNCS, vol. 4966, pp. 48–65. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  9. Gordon, M.J.C., Melham, T.F. (eds.): Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, Cambridge (1993)

    MATH  Google Scholar 

  10. Klein, G., Nipkow, T., Paulson, L.: The archive of formal proofs, http://afp.sf.net/

  11. Meng, J., Paulson, L.C.: Translating higher-order clauses to first-order clauses. J. Auto. Reas. 40(1), 35–60 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  12. Meng, J., Paulson, L.C.: Lightweight relevance filtering for machine-generated resolution problems. J. Applied Logic 7(1), 41–57 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  13. Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002)

    MATH  Google Scholar 

  14. Owre, S., Shankar, N.: Abstract datatypes in PVS. Technical report, SRI (1993)

    Google Scholar 

  15. Skolem, T.: Über die Nicht-charakterisierbarkeit der Zahlenreihe mittels endlich oder abzählbar unendlich vieler Aussagen mit ausschließlich Zahlenvariablen. Fundam. Math. 23, 150–161 (1934)

    MATH  Google Scholar 

  16. Stark, J., Ireland, A.: Invariant discovery via failed proof attempts. In: Flener, P. (ed.) LOPSTR 1998. LNCS, vol. 1559, pp. 271–288. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  17. Torlak, E., Jackson, D.: Kodkod: A relational model finder. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 632–647. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  18. Wenzel, M., Wiedijk, F.: A comparison of the mathematical proof languages Mizar and Isar. J. Auto. Reas. 29(3–4), 389–411 (2002)

    Article  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institut für Informatik, Technische Universität München, Germany

    Jasmin Christian Blanchette

  2. Dept. of CSE, Chalmers University of Technology, Gothenburg, Sweden

    Koen Claessen

Authors
  1. Jasmin Christian Blanchette
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Koen Claessen
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Institut für Computersprachen 185.2, Theory and Logic Group, TU Wien, Favoritenstraße 9-11, A-1040, Vienna, Austria

    Christian G. Fermüller

  2. School of Computer Science, University of Manchester, Oxford Road, Kilburn Building, M13 9PL, Manchester, United Kingdom

    Andrei Voronkov

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Blanchette, J.C., Claessen, K. (2010). Generating Counterexamples for Structural Inductions by Exploiting Nonstandard Models. In: Fermüller, C.G., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2010. Lecture Notes in Computer Science, vol 6397. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-16242-8_10

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-16242-8_10

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-16241-1

  • Online ISBN: 978-3-642-16242-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation