Pages that link to "Item:Q1915134"

The following pages link to Productive use of failure in inductive proof (Q1915134):

Displaying 35 items.

• Algorithmic introduction of quantified cuts (Q402115) (← links)
• The use of embeddings to provide a clean separation of term and annotation for higher order rippling (Q540694) (← links)
• Automating Event-B invariant proofs by rippling and proof patching (Q667526) (← links)
• An integrated approach to high integrity software verification (Q861714) (← links)
• \textit{Theorema}: Towards computer-aided mathematical theory exploration (Q865646) (← links)
• A proof-centric approach to mathematical assistants (Q865648) (← links)
• Supporting the formal verification of mathematical texts (Q865656) (← links)
• Proof-search in type-theoretic languages: An introduction (Q1575935) (← links)
• The problem of \(\Pi_{2}\)-cut-introduction (Q1680562) (← links)
• A computational framework for conceptual blending (Q1748468) (← links)
• Appropriate lemmae discovery (Q1827320) (← links)
• On terminating lemma speculations. (Q1854370) (← links)
• Middle-out reasoning for synthesis and induction (Q1915136) (← links)
• A calculus for and termination of rippling (Q1915137) (← links)
• Proving theorems by reuse (Q1978233) (← links)
• Removing algebraic data types from constrained Horn clauses using difference predicates (Q2096439) (← links)
• Proof planning with multiple strategies (Q2389631) (← links)
• On the generation of quantified lemmas (Q2417949) (← links)
• Dynamic Rippling, Middle-Out Reasoning and Lemma Discovery (Q3058453) (← links)
• ASP, Amalgamation, and the Conceptual Blending Workflow (Q3449215) (← links)
• TIP: Tons of Inductive Problems (Q3453129) (← links)
• (Q4325785) (← links)
• Extensions to a generalization critic for inductive proof (Q4647499) (← links)
• Internal analogy in theorem proving (Q4647502) (← links)
• Termination of theorem proving by reuse (Q4647503) (← links)
• Lemma discovery in automating induction (Q4647546) (← links)
• Deduction as an Engineering Science (Q4916217) (← links)
• PLANS AND PLANNING IN MATHEMATICAL PROOFS (Q5027672) (← links)
• Using Theorema in the Formalization of Theoretical Economics (Q5200108) (← links)
• A divergence critic (Q5210759) (← links)
• Termination orderings for rippling (Q5210791) (← links)
• Using a generalisation critic to find bisimulations for coinductive proofs (Q5234712) (← links)
• A colored version of the λ-calculus (Q5234713) (← links)
• Hipster: Integrating Theory Exploration in a Proof Assistant (Q5495917) (← links)
• Conjectures, tests and proofs: an overview of theory exploration (Q6646290) (← links)