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