Middle-out reasoning for synthesis and induction
From MaRDI portal
Publication:1915136
DOI10.1007/BF00244461zbMATH Open0847.68104MaRDI QIDQ1915136FDOQ1915136
Authors: Ina Kraan, Alan Bundy, David Basin 
Publication date: 11 June 1996
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Recommendations
Cites Work
- Edinburgh LCF. A mechanized logic of computation
- A unification algorithm for typed \(\bar\lambda\)-calculus
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Productive use of failure in inductive proof
- A logic programming language with lambda-abstraction, function variables, and simple unification
- Title not available (Why is that?)
- Middle-out reasoning for synthesis and induction
- Logic program synthesis
- Lazy generation of induction hypotheses
- Rippling: A heuristic for guiding inductive proofs
- Mechanizing structural induction. II: Strategies
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- The OYSTER-CLAM system
- Synthesis of induction orderings for existence proofs
- \textit{Mollusc}: a general proof-development shell for sequent-based logics
Cited In (7)
- Conjecture synthesis for inductive theories
- An approach to automatic deductive synthesis of functional programs
- An integrated approach to high integrity software verification
- \textit{Theorema}: Towards computer-aided mathematical theory exploration
- Synthesis of list algorithms by mechanical proving
- Dynamic rippling, middle-out reasoning and lemma discovery
- Middle-out reasoning for synthesis and induction
Uses Software
This page was built for publication: Middle-out reasoning for synthesis and induction
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1915136)
