Middle-out reasoning for synthesis and induction
From MaRDI portal
(Redirected from Publication:1915136)
Recommendations
Cites work
- scientific article; zbMATH DE number 3859117 (Why is no real title available?)
- scientific article; zbMATH DE number 4164172 (Why is no real title available?)
- scientific article; zbMATH DE number 3976991 (Why is no real title available?)
- scientific article; zbMATH DE number 4072439 (Why is no real title available?)
- scientific article; zbMATH DE number 43398 (Why is no real title available?)
- scientific article; zbMATH DE number 108494 (Why is no real title available?)
- scientific article; zbMATH DE number 193479 (Why is no real title available?)
- scientific article; zbMATH DE number 3566137 (Why is no real title available?)
- A logic programming language with lambda-abstraction, function variables, and simple unification
- A unification algorithm for typed \(\bar\lambda\)-calculus
- Edinburgh LCF. A mechanized logic of computation
- Lazy generation of induction hypotheses
- Logic program synthesis
- Mechanizing structural induction. II: Strategies
- Middle-out reasoning for synthesis and induction
- Productive use of failure in inductive proof
- Rippling: A heuristic for guiding inductive proofs
- Synthesis of induction orderings for existence proofs
- The OYSTER-CLAM system
- \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
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)
