Generating Counterexamples for Structural Inductions by Exploiting Nonstandard Models

DOI10.1007/978-3-642-16242-8_10zbMath1306.68139OpenAlexW1673618793MaRDI QIDQ4933301

Jasmin Christian Blanchette, Koen Claessen

Publication date: 12 October 2010

Published in: Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-16242-8_10

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Nonstandard models (03H99)

Uses Software

• Nitpick
• Isabelle/HOL
• Mizar
• Kodkod

This page was built for publication: Generating Counterexamples for Structural Inductions by Exploiting Nonstandard Models