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. © 2010 Springer-Verlag.
Cite
CITATION STYLE
Blanchette, J. C., & Claessen, K. (2010). Generating counterexamples for structural inductions by exploiting nonstandard models. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6397 LNCS, pp. 127–141). Springer Verlag. https://doi.org/10.1007/978-3-642-16242-8_10
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
