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
