Middle-out reasoning for synthesis and induction
From MaRDI portal
Publication:1915136
DOI10.1007/BF00244461zbMath0847.68104MaRDI QIDQ1915136
Ina Kraan, Alan Bundy, David A. Basin
Publication date: 11 June 1996
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Related Items
An integrated approach to high integrity software verification, \textit{Theorema}: Towards computer-aided mathematical theory exploration, Middle-out reasoning for synthesis and induction, An approach to automatic deductive synthesis of functional programs, Synthesis of list algorithms by mechanical proving, Dynamic Rippling, Middle-Out Reasoning and Lemma Discovery
Uses Software
Cites Work
- Rippling: A heuristic for guiding inductive proofs
- Mechanizing structural induction. II: Strategies
- A unification algorithm for typed \(\bar\lambda\)-calculus
- Edinburgh LCF. A mechanized logic of computation
- Productive use of failure in inductive proof
- Middle-out reasoning for synthesis and induction
- Logic program synthesis
- A logic programming language with lambda-abstraction, function variables, and simple unification
- Synthesis of induction orderings for existence proofs
- Lazy generation of induction hypotheses
- Mollusc a general proof-development shell for sequent-based logics
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item