Some experiments with a completion theorem prover

DOI10.1016/0747-7171(92)90007-QzbMATH Open0748.68071OpenAlexW2063664916WikidataQ55393318 ScholiaQ55393318MaRDI QIDQ1186705FDOQ1186705

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

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

zbMATH Keywords

canonical formcompletion algorithmrewrite rulesautomatic theorem prover

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Cites Work

• The diamond lemma for ring theory
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Termination of rewriting
• Title not available (Why is that?)
• An essay on free products of groups with amalgamations
• Proving a group infinite
• Another single law for groups
• Title not available (Why is that?)
• Title not available (Why is that?)
• The word problem for one-relator semigroups
• Verifying nilpotence
• Title not available (Why is that?)
• The use of Knuth-Bendix methods to solve the word problem in automatic groups
• An overview of LP, the Larch Prover
• Unnecessary inferences in associative-commutative completion procedures
• Title not available (Why is that?)
• Title not available (Why is that?)
• Some one-relator semigroup presentations with solvable word problems
• 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

Cited In (16)

• A New and Formalized Proof of Abstract Completion
• A case study of completion modulo distributivity and Abelian groups
• Title not available (Why is that?)
• Proving group isomorphism theorems
• Problem corner: Proving equivalence of different axiomatizations of free groups
• Title not available (Why is that?)
• Algebra and automated deduction
• Title not available (Why is that?)
• Title not available (Why is that?)
• The Discovery of My Completeness Proofs
• Unnecessary inferences in associative-commutative completion procedures
• Title not available (Why is that?)
• 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
• Theorem proving with group presentations: examples and questions

Uses Software

• LARCH
• SbReve2
• RRL

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)