The following pages link to (Q2751365):
Displaying 20 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)
- The problem of \(\Pi_{2}\)-cut-introduction (Q1680562) (← links)
- Appropriate lemmae discovery (Q1827320) (← links)
- Sound generalizations in mathematical induction (Q1882908) (← 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)
- Schematic Cut Elimination and the Ordered Pigeonhole Principle (Q2817924) (← links)
- Dynamic Rippling, Middle-Out Reasoning and Lemma Discovery (Q3058453) (← links)
- What is a proof? (Q5301851) (← links)
- Analysis and Transformation of Constrained Horn Clauses for Program Verification (Q6063893) (← links)
