swMATH28904MaRDI QIDQ40618FDOQ40618
Author name not available (Why is that?)
Official website: https://www.sciencedirect.com/science/article/pii/089812219400218A
Cited In (75)
- Sound lemma generation for proving inductive validity of equations
- A path ordering for proving termination of AC rewrite systems
- Title not available (Why is that?)
- Title not available (Why is that?)
- MACE4 and SEM: a comparison of finite model generators
- 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
- Narrowing based inductive proof search
- Complexity of matching problems
- A multi-level geometric reasoning system for vision
- Rewriting systems of Coxeter groups
- Rewrite orderings for higher-order terms in \(\eta\)-long \(\beta\)-normal form and the recursive path ordering
- On recursive path ordering
- Mathematical induction in Otter-lambda
- The correctness of the fast Fourier transform: A structured proof in ACL2
- Lemma discovery in automating induction
- 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
- AURA
- NQTHM
- SPIKE
- MathXpert
- MGTP
- PARTHEO
- SbReve2
- ORME
- Automating inductionless induction using test sets
- Unnecessary inferences in associative-commutative completion procedures
- Gordon's computer: A hardware verification case study in OBJ3
- CLAM
- InKa
- Oyster
- Angelic Verification
- A3PAT
- ModGen
- Saturate
- EXPANDER
- PARTHENON
- METEOR
- Aquarius
- QuodLibet
- FELIX
- AFFIRM
- SAEPTUM
- REVE
- UNICOM
- Tecton
- Inductive proof search modulo
- On subsumption in distributed derivations
- NARROWER
- Some experiments with a completion theorem prover
- Artin groups, rewriting systems and three-manifolds
- History and basic features of the critical-pair/completion procedure
- A PVS theory for term rewriting systems
- 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?)
- 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
