Productive use of failure in inductive proof
From MaRDI portal
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; zbMATH DE number 1696795
- 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
- A colored version of the -calculus
- A divergence critic
- Edinburgh LCF. A mechanized logic of computation
- Extensions to the rippling-out tactic for guiding inductive proofs
- Guiding induction proofs
- scientific article; zbMATH DE number 3913652 (Why is no real title available?)
- scientific article; zbMATH DE number 4072439 (Why is no real title available?)
- scientific article; zbMATH DE number 3702108 (Why is no real title available?)
- scientific article; zbMATH DE number 1348478 (Why is no real title available?)
- scientific article; zbMATH DE number 3333259 (Why is no real title available?)
- Implicit induction in conditional theories
- Rippling: A heuristic for guiding inductive proofs
- The OYSTER-CLAM system
Cited in
(41)- Proof-search in type-theoretic languages: An introduction
- The problem of \(\Pi_{2}\)-cut-introduction
- A computational framework for conceptual blending
- Appropriate lemmae discovery
- On terminating lemma speculations.
- Middle-out reasoning for synthesis and induction
- A calculus for and termination of rippling
- Proving theorems by reuse
- Removing algebraic data types from constrained Horn clauses using difference predicates
- Proof planning with multiple strategies
- On the generation of quantified lemmas
- Concept Formation via Proof Planning Failure
- Dynamic rippling, middle-out reasoning and lemma discovery
- ASP, amalgamation, and the conceptual blending workflow
- TIP: tons of inductive problems
- Predicting failures of and repairing inductive proof attempts
- scientific article; zbMATH DE number 19767 (Why is no real title available?)
- Algorithmic introduction of quantified cuts
- scientific article; zbMATH DE number 733397 (Why is no real title available?)
- Extensions to a generalization critic for inductive proof
- Internal analogy in theorem proving
- Termination of theorem proving by reuse
- Lemma discovery in automating induction
- Deduction as an engineering science
- Plans and planning in mathematical proofs
- Using Theorema in the Formalization of Theoretical Economics
- A divergence critic
- Termination orderings for rippling
- Using a generalisation critic to find bisimulations for coinductive proofs
- A colored version of the -calculus
- The use of embeddings to provide a clean separation of term and annotation for higher order rippling
- Hipster: integrating theory exploration in a proof assistant
- Solving constrained Horn clauses over algebraic data types
- Conjectures, tests and proofs: an overview of theory exploration
- Automating Event-B invariant proofs by rippling and proof patching
- Lemma discovery and strategies for automated induction
- Automatically generalizing proofs and statements
- An integrated approach to high integrity software verification
- \textit{Theorema}: Towards computer-aided mathematical theory exploration
- A proof-centric approach to mathematical assistants
- Supporting the formal verification of mathematical texts
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)
