Automating Inductive Proofs Using Theory Exploration
- 1 January 2013
- book chapter
- conference paper
- Published by Springer Science and Business Media LLC in Lecture Notes in Computer Science
Abstract
No abstract availableKeywords
This publication has 16 references indexed in Scilit:
- The ACL2 Sedan Theorem Proving SystemLecture Notes in Computer Science, 2011
- Conjecture Synthesis for Inductive TheoriesJournal of Automated Reasoning, 2010
- Dynamic Rippling, Middle-Out Reasoning and Lemma DiscoveryLecture Notes in Computer Science, 2010
- Case-Analysis for Rippling and Inductive ProofLecture Notes in Computer Science, 2010
- QuickSpec: Guessing Formal Specifications Using TestingLecture Notes in Computer Science, 2010
- Z3: An Efficient SMT SolverLecture Notes in Computer Science, 2008
- Rippling: Meta-Level Guidance for Mathematical ReasoningPublished by Cambridge University Press (CUP) ,2005
- Higher Order Rippling in IsaPlannerLecture Notes in Computer Science, 2004
- QuickCheckACM SIGPLAN Notices, 2000
- Productive use of failure in inductive proofJournal of Automated Reasoning, 1996