Productive use of failure in inductive proof
From MaRDI portal
Publication:1915134
DOI10.1007/BF00244460zbMath0847.68103OpenAlexW2067540169MaRDI QIDQ1915134
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
Related Items
ASP, Amalgamation, and the Conceptual Blending Workflow ⋮ TIP: Tons of Inductive Problems ⋮ Proof planning with multiple strategies ⋮ 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 ⋮ Middle-out reasoning for synthesis and induction ⋮ A calculus for and termination of rippling ⋮ The problem of \(\Pi_{2}\)-cut-introduction ⋮ On the generation of quantified lemmas ⋮ Algorithmic introduction of quantified cuts ⋮ Solving constrained Horn clauses over algebraic data types ⋮ Automating Event-B invariant proofs by rippling and proof patching ⋮ Proving theorems by reuse ⋮ Extensions to a generalization critic for inductive proof ⋮ Internal analogy in theorem proving ⋮ Termination of theorem proving by reuse ⋮ Lemma discovery in automating induction ⋮ A computational framework for conceptual blending ⋮ Deduction as an Engineering Science ⋮ The use of embeddings to provide a clean separation of term and annotation for higher order rippling ⋮ Dynamic Rippling, Middle-Out Reasoning and Lemma Discovery ⋮ 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 ⋮ Appropriate lemmae discovery ⋮ Hipster: Integrating Theory Exploration in a Proof Assistant ⋮ Proof-search in type-theoretic languages: An introduction ⋮ Removing algebraic data types from constrained Horn clauses using difference predicates ⋮ On terminating lemma speculations. ⋮ PLANS AND PLANNING IN MATHEMATICAL PROOFS
Uses Software
Cites Work
