Some experiments with a completion theorem prover

DOI10.1016/0747-7171(92)90007-QMaRDI QIDQ1186705zbMATH OpenOpenAlexWikidataFDO

Authors Ursula Martin Webb, Michael Lai

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 formcompletion algorithmrewrite rulesautomatic theorem prover

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Recommendations

• Some group theoretic examples with completion theorem provers
• scientific article; zbMATH DE number 3870642
• scientific article; zbMATH DE number 44069
• scientific article; zbMATH DE number 3856444
• A case study of completion modulo distributivity and Abelian groups

Cites work

• scientific article; zbMATH DE number 3137403 (Why is no real title available?)
• scientific article; zbMATH DE number 3870642 (Why is no real title available?)
• scientific article; zbMATH DE number 3871338 (Why is no real title available?)
• scientific article; zbMATH DE number 3904002 (Why is no real title available?)
• scientific article; zbMATH DE number 3682004 (Why is no real title available?)
• scientific article; zbMATH DE number 3761016 (Why is no real title available?)
• scientific article; zbMATH DE number 41806 (Why is no real title available?)
• scientific article; zbMATH DE number 42096 (Why is no real title available?)
• scientific article; zbMATH DE number 3299786 (Why is no real title available?)
• An essay on free products of groups with amalgamations
• An overview of LP, the Larch Prover
• Another single law for groups
• History and basic features of the critical-pair/completion procedure
• Problem corner: Proving equivalence of different axiomatizations of free groups
• Proving a group infinite
• Some experiments in nonassociative ring theory with an automated theorem prover
• Some one-relator semigroup presentations with solvable word problems
• Termination of rewriting
• The diamond lemma for ring theory
• The use of Knuth-Bendix methods to solve the word problem in automatic groups
• The word problem for one-relator semigroups
• Unnecessary inferences in associative-commutative completion procedures
• Verifying nilpotence

Cited in

(16)

• Theorem proving with group presentations: examples and questions
• A New and Formalized Proof of Abstract Completion
• A case study of completion modulo distributivity and Abelian groups
• scientific article; zbMATH DE number 4033137 (Why is no real title available?)
• Proving group isomorphism theorems
• Problem corner: Proving equivalence of different axiomatizations of free groups
• scientific article; zbMATH DE number 65529 (Why is no real title available?)
• Algebra and automated deduction
• scientific article; zbMATH DE number 1615240 (Why is no real title available?)
• scientific article; zbMATH DE number 3856444 (Why is no real title available?)
• The Discovery of My Completeness Proofs
• Unnecessary inferences in associative-commutative completion procedures
• scientific article; zbMATH DE number 3870642 (Why is no real title available?)
• REVEUR-3: The implementation of a general completion procedure parameterized by built-in theories and strategies
• Artificial Intelligence and Symbolic Computation
• Citius altius fortius: lessons learned from the theorem prover Waldmeister

Describes a project that uses

Uses Software

• RRL
• SbReve2
• LARCH

This page was built for publication: Some experiments with a completion theorem prover

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1186705)