Some experiments with a completion theorem prover

DOI10.1016/0747-7171(92)90007-QzbMath0748.68071WikidataQ55393318 ScholiaQ55393318MaRDI QIDQ1186705

Michael Lai, Ursula Martin Webb

Publication date: 28 June 1992

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0747-7171(92)90007-q

zbMATH Keywords

canonical form; completion algorithm; rewrite rules; automatic theorem prover

Mathematics Subject Classification ID

68Q42: Grammars and rewriting systems

Related Items

Theorem proving with group presentations: Examples and questions

Uses Software

• LARCH
• SbReve2
• RRL

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Verifying nilpotence
• Termination of rewriting
• History and basic features of the critical-pair/completion procedure
• Some experiments in nonassociative ring theory with an automated theorem prover
• Problem corner: Proving equivalence of different axiomatizations of free groups
• Proving a group infinite
• The use of Knuth-Bendix methods to solve the word problem in automatic groups
• The diamond lemma for ring theory
• Unnecessary inferences in associative-commutative completion procedures
• Another single law for groups
• The word problem for one-relator semigroups
• Some one-relator semigroup presentations with solvable word problems
• An overview of LP, the Larch Prover
• An essay on free products of groups with amalgamations