The following pages link to Proof by consistency (Q1094888):
Displaying 30 items.
- Proving termination by dependency pairs and inductive theorem proving (Q438537) (← links)
- Mechanically certifying formula-based Noetherian induction reasoning (Q507366) (← links)
- Tools for proving inductive equalities, relative completeness, and \(\omega\)-completeness (Q582891) (← links)
- Towards a foundation of completion procedures as semidecision procedures (Q673134) (← links)
- Automating inductionless induction using test sets (Q758216) (← links)
- Only prime superpositions need be considered in the Knuth-Bendix completion procedure (Q1106657) (← links)
- Which data types have \(\omega\)-complete initial algebra specifications? (Q1318728) (← links)
- Deductive and inductive synthesis of equational programs (Q1322836) (← links)
- Proving Ramsey's theory by the cover set induction: A case and comparision study. (Q1353938) (← links)
- Model building with ordered resolution: Extracting models from saturated clause sets (Q1404975) (← links)
- Induction = I-axiomatization + first-order consistency. (Q1854350) (← links)
- Implicit induction in conditional theories (Q1891255) (← links)
- An algebraic characterization of inductive soundness in proof by consistency (Q1894333) (← links)
- Induction using term orders (Q1915132) (← links)
- Proving semantic properties as first-order satisfiability (Q2289018) (← links)
- Unification modulo lists with reverse relation with certain word equations (Q2305403) (← links)
- Finite reasons for safety (Q2351397) (← links)
- Abstract canonical presentations (Q2500482) (← links)
- Sufficient-completeness, ground-reducibility and their complexity (Q2641108) (← links)
- Termination of algorithms over non-freely generated data types (Q4647505) (← links)
- Proving ground confluence and inductive validity in constructor based equational specifications (Q5044723) (← links)
- Computing ground reducibility and inductively complete positions (Q5055712) (← links)
- Inductive proofs by specification transformations (Q5055713) (← links)
- An overview of LP, the Larch Prover (Q5055717) (← links)
- Proving equational and inductive theorems by completion and embedding techniques (Q5055774) (← links)
- Termination Analysis by Dependency Pairs and Inductive Theorem Proving (Q5191111) (← links)
- Induction using term orderings (Q5210765) (← links)
- On notions of inductive validity for first-order equational clauses (Q5210769) (← links)
- A constructor-based approach for positive/negative-conditional equational specifications (Q5881186) (← links)
- Completion procedures as semidecision procedures (Q5881279) (← links)
