Electronic Resource
Springer
Journal of automated reasoning
9 (1992), S. 291-308
ISSN:
1573-0670
Keywords:
Group
;
model
;
paramodulation
Source:
Springer Online Journal Archives 1860-2000
Topics:
Computer Science
Notes:
Abstract We study equations of the form (α=x) which are single axioms for group theory. Earlier examples of such were found by Neumann and McCune. We prove some lower bounds on the complexity of these α, showing that McCune's examples are the shortest possible. We also show that no such α can have only two distinct variables. We do produce an α with only three distinct variables, refuting a conjecture of Neumann. Automated reasoning techniques are used both positively (searching for and verifying single axioms) and negatively (proving that various candidate (α=x) hold in some nongroup and are, hence, not single axioms).
Type of Medium:
Electronic Resource
URL:
http://dx.doi.org/10.1007/BF00245293
Permalink
|
Location |
Call Number |
Expected |
Availability |