RRL

swMATH28904MaRDI QIDQ40618FDOQ40618

Author name not available (Why is that?)

Cited In (48)

• Sound lemma generation for proving inductive validity of equations
• Using an induction prover for verifying arithmetic circuits
• New uses of linear arithmetic in automated theorem proving by induction
• On the recursive decomposition ordering with lexicographical status and other related orderings
• Deaccumulation techniques for improving provability
• Conditional congruence closure over uninterpreted and interpreted symbols
• A quantifier-elimination based heuristic for automatically generating inductive assertions for programs
• Problem corner: Proving equivalence of different axiomatizations of free groups
• Adventures in associative-commutative unification
• Complexity of matching problems
• A multi-level geometric reasoning system for vision
• Rewriting systems of Coxeter groups
• A path ordering for proving termination of AC rewrite systems
• Rewrite orderings for higher-order terms in \(\eta\)-long \(\beta\)-normal form and the recursive path ordering
• On recursive path ordering
• MACE4 and SEM: A Comparison of Finite Model Generators
• Mathematical induction in Otter-lambda
• The correctness of the fast Fourier transform: A structured proof in ACL2
• Lemma discovery in automating induction
• A PVS Theory for Term Rewriting Systems
• Title not available (Why is that?)
• Termination of rewriting
• Transformational methodology for proving termination of logic programs
• On the modelling of search in theorem proving -- towards a theory of strategy analysis
• Termination orderings for associative-commutative rewriting systems
• A formalization of the Knuth-Bendix(-Huet) critical pair theorem
• Induction = I-axiomatization + first-order consistency.
• Automated proofs of equality problems in Overbeek's competition
• Automating inductionless induction using test sets
• Unnecessary inferences in associative-commutative completion procedures
• Gordon's computer: A hardware verification case study in OBJ3
• Inductive proof search modulo
• On subsumption in distributed derivations
• Some experiments with a completion theorem prover
• Title not available (Why is that?)
• Artin groups, rewriting systems and three-manifolds
• History and basic features of the critical-pair/completion procedure
• Proving Ramsey's theory by the cover set induction: A case and comparision study.
• The application of automated reasoning to questions in mathematics and logic
• Title not available (Why is that?)
• Narrowing Based Inductive Proof Search
• An overview of the Tecton proof system
• Only prime superpositions need be considered in the Knuth-Bendix completion procedure
• Mechanically certifying formula-based Noetherian induction reasoning
• Title not available (Why is that?)
• Semi-unification
• Proving theorems by reuse
• A general framework to build contextual cover set induction provers

This page was built for software: RRL