RRL
From MaRDI portal
Cited in
(76)- Using an induction prover for verifying arithmetic circuits
- Sound lemma generation for proving inductive validity of equations
- On the recursive decomposition ordering with lexicographical status and other related orderings
- New uses of linear arithmetic in automated theorem proving by induction
- 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
- Narrowing based inductive proof search
- Rewriting systems of Coxeter groups
- On recursive path ordering
- Rewrite orderings for higher-order terms in \(\eta\)-long \(\beta\)-normal form and the recursive path ordering
- A path ordering for proving termination of AC rewrite systems
- Mathematical induction in Otter-lambda
- Lemma discovery in automating induction
- The correctness of the fast Fourier transform: A structured proof in ACL2
- scientific article; zbMATH DE number 1614706 (Why is no real title available?)
- Termination of rewriting
- On the modelling of search in theorem proving -- towards a theory of strategy analysis
- Transformational methodology for proving termination of logic programs
- Termination orderings for associative-commutative rewriting systems
- A formalization of the Knuth-Bendix(-Huet) critical pair theorem
- LARCH
- AURA
- NQTHM
- SPIKE
- MathXpert
- MGTP
- PARTHEO
- SbReve2
- ORME
- CLAM
- InKa
- Oyster
- Angelic Verification
- A3PAT
- ModGen
- Saturate
- EXPANDER
- PARTHENON
- METEOR
- Aquarius
- QuodLibet
- FELIX
- AFFIRM
- SAEPTUM
- REVE
- UNICOM
- Tecton
- Induction = I-axiomatization + first-order consistency.
- Automated proofs of equality problems in Overbeek's competition
- Automating inductionless induction using test sets
- Gordon's computer: A hardware verification case study in OBJ3
- Unnecessary inferences in associative-commutative completion procedures
- Inductive proof search modulo
- On subsumption in distributed derivations
- Some experiments with a completion theorem prover
- NARROWER
- scientific article; zbMATH DE number 1639660 (Why is no real title available?)
- Artin groups, rewriting systems and three-manifolds
- History and basic features of the critical-pair/completion procedure
- MACE4 and SEM: a comparison of finite model generators
- 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
- A PVS theory for term rewriting systems
- scientific article; zbMATH DE number 4047063 (Why is no real title available?)
- 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
- scientific article; zbMATH DE number 4053061 (Why is no real title available?)
- Semi-unification
- Proving theorems by reuse
- A general framework to build contextual cover set induction provers
This page was built for software: RRL
