Experiments with proof plans for induction
From MaRDI portal
Recommendations
Cites work
- scientific article; zbMATH DE number 4164172 (Why is no real title available?)
- scientific article; zbMATH DE number 4164177 (Why is no real title available?)
- scientific article; zbMATH DE number 4047053 (Why is no real title available?)
- scientific article; zbMATH DE number 4072439 (Why is no real title available?)
- A Transformation System for Developing Recursive Programs
- Edinburgh LCF. A mechanized logic of computation
- Planning in a hierarchy of abstraction spaces
Cited in
(16)- Internal analogy in theorem proving
- Discussing Hilbert's 24th problem
- Conjecture synthesis for inductive theories
- On process equivalence = equation solving in CCS
- Rippling: A heuristic for guiding inductive proofs
- Extensions to the rippling-out tactic for guiding inductive proofs
- Guiding induction proofs
- scientific article; zbMATH DE number 4072439 (Why is no real title available?)
- An integrated approach to high integrity software verification
- A calculus for and termination of rippling
- Lazy techniques for fully expansive theorem proving
- Knowledge-based proof planning
- Proof planning with multiple strategies
- Dynamic rippling, middle-out reasoning and lemma discovery
- scientific article; zbMATH DE number 1189094 (Why is no real title available?)
- scientific article; zbMATH DE number 4164172 (Why is no real title available?)
This page was built for publication: Experiments with proof plans for induction
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q809617)
