Problem corner: Proving equivalence of different axiomatizations of free groups
type: Item
instance of: scholarly article
title: Problem corner: Proving equivalence of different axiomatizations of free groups
zbMATH Open document ID: 0654.68102
DOI: 10.1007/BF00244946
author: Deepak Kapur
author: Hantao Zhang
published in: Journal of Automated Reasoning
publication date: 1988-01-01T00:00:00Z
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.
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 20E05
Mathematics Subject Classification ID: 20A05
zbMATH DE Number: 4068332
zbMATH Keywords: automatic theorem prover
zbMATH Keywords: lexicographic recursive path ordering
zbMATH Keywords: free group
zbMATH Keywords: complete sets of rewrite rules
reviewed by: Heinrich Guggenheimer
describes a project that uses: RRL
MaRDI profile type: Publication
full work available at URL: https://doi.org/10.1007/bf00244946
OpenAlex ID: W2011658799
description: scientific article; zbMATH DE number 4068332