Pages that link to "Item:Q2751365"

The following pages link to The automation of proof by mathematical induction (Q2751365):

Displaying 43 items.

• Algorithmic introduction of quantified cuts (Q402115) (← links)
• Proving termination by dependency pairs and inductive theorem proving (Q438537) (← links)
• Mathematical induction in Otter-lambda (Q861715) (← links)
• Deaccumulation techniques for improving provability (Q882487) (← links)
• Rule-based induction (Q1334895) (← links)
• Induction proofs with partial functions (Q1595923) (← links)
• The problem of \(\Pi_{2}\)-cut-introduction (Q1680562) (← links)
• Appropriate lemmae discovery (Q1827320) (← links)
• Sound generalizations in mathematical induction (Q1882908) (← links)
• Implicit induction in conditional theories (Q1891255) (← links)
• New uses of linear arithmetic in automated theorem proving by induction (Q1915133) (← links)
• A calculus for and termination of rippling (Q1915137) (← links)
• Automated mathematical induction (Q1915187) (← links)
• Removing algebraic data types from constrained Horn clauses using difference predicates (Q2096439) (← links)
• Combining induction and saturation-based theorem proving (Q2303240) (← links)
• Inductive theorem proving based on tree grammars (Q2344621) (← links)
• Verification as a parameterized testing (experiments with the SCP4 supercompiler) (Q2371554) (← links)
• Automated mutual induction proof in separation logic (Q2414251) (← links)
• On the generation of quantified lemmas (Q2417949) (← links)
• An approach to automatic deductive synthesis of functional programs (Q2457802) (← links)
• Herbrand's theorem and term induction (Q2491080) (← links)
• Shallow confluence of conditional term rewriting systems (Q2518609) (← links)
• Inductionless induction (Q2751366) (← links)
• Schematic Cut Elimination and the Ordered Pigeonhole Principle (Q2817924) (← links)
• Strategic issues, problems and challenges in inductive theorem proving (Q2848043) (← links)
• Dynamic Rippling, Middle-Out Reasoning and Lemma Discovery (Q3058453) (← links)
• Automated Certification of Implicit Induction Proofs (Q3100200) (← links)
• Combining Rewriting with Noetherian Induction to Reason on Non-orientable Equalities (Q3522029) (← links)
• Automated Mathematical Induction (Q4849648) (← links)
• (Q4886736) (← links)
• Computer-assisted human-oriented inductive theorem proving by descente infinie--a manifesto (Q4913999) (← links)
• (Q5016384) (← links)
• (Q5020652) (← links)
• Termination Analysis by Dependency Pairs and Inductive Theorem Proving (Q5191111) (← links)
• Automated Cyclic Entailment Proofs in Separation Logic (Q5200020) (← links)
• Verifying Procedural Programs via Constrained Rewriting Induction (Q5278212) (← links)
• What is a proof? (Q5301851) (← links)
• Mechanizing Mathematical Reasoning (Q5717440) (← links)
• A Decidable Class of Nested Iterated Schemata (Q5747768) (← links)
• Perfect Discrimination Graphs: Indexing Terms with Integer Exponents (Q5747777) (← links)
• Analysis and Transformation of Constrained Horn Clauses for Program Verification (Q6063893) (← links)
• Definitional Quantifiers Realise Semantic Reasoning for Proof by Induction (Q6487292) (← links)
• Guiding induction proofs (Q6488528) (← links)