Productive use of failure in inductive proof
From MaRDI portal
Publication:1915134
DOI10.1007/BF00244460zbMATH Open0847.68103OpenAlexW2067540169MaRDI QIDQ1915134FDOQ1915134
Authors: Andrew Ireland, Alan Bundy 
Publication date: 11 June 1996
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/bf00244460
Recommendations
- Predicting failures of and repairing inductive proof attempts
- Making a productive use of failure to generate witnesses for coinduction from divergent proof attempts
- Logic Based Program Synthesis and Transformation
- A proof theoretic approach to failure in functional logic programming
- scientific article
- Failure reasoning in multiple-strategy proof planning
- scientific article; zbMATH DE number 4072439
- Strictness analysis aids inductive proofs
- Induction on Failure: Learning Connected Horn Theories
Cites Work
- Edinburgh LCF. A mechanized logic of computation
- Title not available (Why is that?)
- Implicit induction in conditional theories
- Title not available (Why is that?)
- Title not available (Why is that?)
- Rippling: A heuristic for guiding inductive proofs
- Title not available (Why is that?)
- Extensions to the rippling-out tactic for guiding inductive proofs
- Guiding induction proofs
- The OYSTER-CLAM system
- Title not available (Why is that?)
- A colored version of the λ-calculus
- A divergence critic
Cited In (38)
- On terminating lemma speculations.
- Algorithmic introduction of quantified cuts
- PLANS AND PLANNING IN MATHEMATICAL PROOFS
- A divergence critic
- The use of embeddings to provide a clean separation of term and annotation for higher order rippling
- On the generation of quantified lemmas
- A computational framework for conceptual blending
- An integrated approach to high integrity software verification
- A proof-centric approach to mathematical assistants
- Supporting the formal verification of mathematical texts
- Extensions to a generalization critic for inductive proof
- \textit{Theorema}: Towards computer-aided mathematical theory exploration
- Solving constrained Horn clauses over algebraic data types
- Predicting failures of and repairing inductive proof attempts
- Lemma discovery in automating induction
- A calculus for and termination of rippling
- Termination of theorem proving by reuse
- Hipster: Integrating Theory Exploration in a Proof Assistant
- TIP: Tons of Inductive Problems
- A colored version of the λ-calculus
- Title not available (Why is that?)
- Proof planning with multiple strategies
- Conjectures, tests and proofs: an overview of theory exploration
- The problem of \(\Pi_{2}\)-cut-introduction
- Using Theorema in the Formalization of Theoretical Economics
- Concept Formation via Proof Planning Failure
- Dynamic rippling, middle-out reasoning and lemma discovery
- Deduction as an Engineering Science
- Termination orderings for rippling
- Appropriate lemmae discovery
- ASP, Amalgamation, and the Conceptual Blending Workflow
- Proof-search in type-theoretic languages: An introduction
- Automating Event-B invariant proofs by rippling and proof patching
- Proving theorems by reuse
- Using a generalisation critic to find bisimulations for coinductive proofs
- Removing algebraic data types from constrained Horn clauses using difference predicates
- Middle-out reasoning for synthesis and induction
- Internal analogy in theorem proving
Uses Software
This page was built for publication: Productive use of failure in inductive proof
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1915134)
