Generating Counterexamples for Structural Inductions by Exploiting Nonstandard Models

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