Pages that link to "Item:Q1891255"
From MaRDI portal
The following pages link to Implicit induction in conditional theories (Q1891255):
Displaying 28 items.
- Sufficient completeness verification for conditional and constrained TRS (Q420848) (← links)
- Inverse subsumption for complete explanatory induction (Q439023) (← links)
- Using induction and rewriting to verify and complete parameterized specifications (Q672051) (← links)
- Conditional excluded middle in systems of consequential implication (Q815021) (← links)
- Deaccumulation techniques for improving provability (Q882487) (← links)
- Inductive proof search modulo (Q1037404) (← links)
- Incorporating decision procedures in implicit induction. (Q1404422) (← links)
- Observational proofs by rewriting. (Q1607227) (← links)
- Induction = I-axiomatization + first-order consistency. (Q1854350) (← links)
- Automata-driven automated induction (Q1854445) (← links)
- Productive use of failure in inductive proof (Q1915134) (← links)
- Specification and proof in membership equational logic (Q1978640) (← links)
- Generalized rewrite theories, coherence completion, and symbolic methods (Q2291817) (← links)
- Combining induction and saturation-based theorem proving (Q2303240) (← links)
- A note on conditional implication (Q2748738) (← links)
- Narrowing and rewriting logic: from foundations to applications (Q2873786) (← links)
- AN EXTENSION OF AN AUTOMATED TERMINATION METHOD OF RECURSIVE FUNCTIONS (Q3021959) (← links)
- The Implications of Induction (Q3383401) (← links)
- Combining Rewriting with Noetherian Induction to Reason on Non-orientable Equalities (Q3522029) (← links)
- Automated Induction with Constrained Tree Automata (Q3541728) (← links)
- Unraveling a Card Trick (Q3587256) (← links)
- On Proving Termination of Constrained Term Rewrite Systems by Eliminating Edges from Dependency Graphs (Q5200103) (← links)
- A divergence critic (Q5210759) (← links)
- Using a generalisation critic to find bisimulations for coinductive proofs (Q5234712) (← links)
- Perfect Discrimination Graphs: Indexing Terms with Integer Exponents (Q5747777) (← links)
- A calculus for conditional inductive theorem proving (Q5881199) (← links)
- A general framework to build contextual cover set induction provers (Q5950934) (← links)
- On Ground Convergence and Completeness of Conditional Equational Program Hierarchies (Q6487297) (← links)