The following pages link to (Q2751365):
Displaying 28 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)
- Combining Rewriting with Noetherian Induction to Reason on Non-orientable Equalities (Q3522029) (← 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)
- 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)
