Middle-out reasoning for synthesis and induction

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)

zbMATH Keywords

logic program synthesisinduction schemesmiddle-out reasoning

Mathematics Subject Classification ID

Related Items (6)

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

• NQTHM
• InKa
• CLAM
• Oyster
• Mollusc

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• 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

This page was built for publication: Middle-out reasoning for synthesis and induction