Problem corner: Proving equivalence of different axiomatizations of free groups

DOI10.1007/BF00244946MaRDI QIDQ1108815zbMATH OpenOpenAlexFDO

Authors Deepak Kapur, Hantao Zhang

Publication date 1988

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/bf00244946

zbMATH Keywords

automatic theorem provercomplete sets of rewrite rulesfree grouplexicographic recursive path ordering

Mathematics Subject Classification ID

Axiomatics and elementary properties of groups (20A05) Free nonabelian groups (20E05)

Review text

The authors have developed an automatic theorem prover based on lexicographic recursive path ordering [the authors, RRL: A rewrite rule laboratory - user's manual, GE R \& D Center (1987)] that transforms given formulas into normal forms and then uses substitution rules to derive new formulas. The authors use the program to show the equivalence of four axiomatizations of the notion of free group and to derive complete sets of rewrite rules for these constructs.

Recommendations

• Some experiments with a completion theorem prover
• Proving group isomorphism theorems
• Some group theoretic examples with completion theorem provers
• Computer proofs in group theory
• scientific article; zbMATH DE number 934902

Cited in

(5)

• Some experiments with a completion theorem prover
• Single axioms for groups and abelian groups with various operations
• Automated proofs of equality problems in Overbeek's competition
• Lattice-ordered groups in deduction
• The Existence of Level Sets in a Free Group Implies the Axiom of Choice

Describes a project that uses

Uses Software

• RRL

This page was built for publication: Problem corner: Proving equivalence of different axiomatizations of free groups

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