The following pages link to RRL (Q40618):
Displaying 48 items.
- Mechanically certifying formula-based Noetherian induction reasoning (Q507366) (← links)
- A formalization of the Knuth-Bendix(-Huet) critical pair theorem (Q616850) (← links)
- Automating inductionless induction using test sets (Q758216) (← links)
- Semi-unification (Q808713) (← links)
- Mathematical induction in Otter-lambda (Q861715) (← links)
- Deaccumulation techniques for improving provability (Q882487) (← links)
- A quantifier-elimination based heuristic for automatically generating inductive assertions for programs (Q882517) (← links)
- On the recursive decomposition ordering with lexicographical status and other related orderings (Q912609) (← links)
- Inductive proof search modulo (Q1037404) (← links)
- Termination orderings for associative-commutative rewriting systems (Q1072371) (← links)
- On recursive path ordering (Q1082075) (← links)
- Termination of rewriting (Q1098624) (← links)
- Complexity of matching problems (Q1099615) (← links)
- History and basic features of the critical-pair/completion procedure (Q1103414) (← links)
- Only prime superpositions need be considered in the Knuth-Bendix completion procedure (Q1106657) (← links)
- Problem corner: Proving equivalence of different axiomatizations of free groups (Q1108815) (← links)
- A multi-level geometric reasoning system for vision (Q1116357) (← links)
- Some experiments with a completion theorem prover (Q1186705) (← links)
- Adventures in associative-commutative unification (Q1262757) (← links)
- Rewrite orderings for higher-order terms in \(\eta\)-long \(\beta\)-normal form and the recursive path ordering (Q1275015) (← links)
- On the modelling of search in theorem proving -- towards a theory of strategy analysis (Q1281504) (← links)
- Artin groups, rewriting systems and three-manifolds (Q1295710) (← links)
- Automated proofs of equality problems in Overbeek's competition (Q1319385) (← links)
- Rewriting systems of Coxeter groups (Q1321036) (← links)
- Gordon's computer: A hardware verification case study in OBJ3 (Q1329091) (← links)
- On subsumption in distributed derivations (Q1337562) (← links)
- An overview of the Tecton proof system (Q1341710) (← links)
- Proving Ramsey's theory by the cover set induction: A case and comparision study. (Q1353938) (← links)
- The application of automated reasoning to questions in mathematics and logic (Q1354049) (← links)
- Conditional congruence closure over uninterpreted and interpreted symbols (Q1730315) (← links)
- Induction = I-axiomatization + first-order consistency. (Q1854350) (← links)
- Using an induction prover for verifying arithmetic circuits (Q1856145) (← links)
- A path ordering for proving termination of AC rewrite systems (Q1891259) (← links)
- New uses of linear arithmetic in automated theorem proving by induction (Q1915133) (← links)
- Proving theorems by reuse (Q1978233) (← links)
- (Q2723430) (← links)
- (Q2738486) (← links)
- Sound lemma generation for proving inductive validity of equations (Q3165943) (← links)
- Unnecessary inferences in associative-commutative completion procedures (Q3489486) (← links)
- (Q3783519) (← links)
- (Q3789100) (← links)
- Transformational methodology for proving termination of logic programs (Q3841095) (← links)
- Lemma discovery in automating induction (Q4647546) (← links)
- MACE4 and SEM: A Comparison of Finite Model Generators (Q4913862) (← links)
- Narrowing Based Inductive Proof Search (Q4916079) (← links)
- A PVS Theory for Term Rewriting Systems (Q5178962) (← links)
- A general framework to build contextual cover set induction provers (Q5950934) (← links)
- The correctness of the fast Fourier transform: A structured proof in ACL2 (Q5959860) (← links)
