problem-set/algebra/groups/README created : 06/30/86 revised : 08/12/88 Contents of 'groups' : ---------------------- NOTE : These problems have come from 'Problems & Experiments from & With Automated Theorem-Proving programs' by McCharen, Overbeek, & Wos [Aug. 1976]. Main File Headings ---------------------------------------------------------------------- README : You are currently here; a description of all the files in the directory problem-set/algebra/groups. Group.ax.p.clauses : standard group axioms, in a p-formulation. Group.ax.eq.clauses : standard group axioms, in an equality formulation. Group.ax.g.clauses : standard group axioms, in a revised p-formulation whereby the group is specified in each predicate, so that one may work problems involving more than one group. Lemmas.p.clauses : lemmas proven in the p-formulation. Lemmas.eq.clauses : lemmas proven in the equality formulation. xsquared : Theorem: if, for all x in G, x*x=e then G is abelian (commutative); i.e., for all x,y in G, x*y=y*x. invers1 : Theorem: the inverse is unique; i.e., if ab=ba=e and ac=ca=e, then b=c [e is the identity]. ident1 : Theorem: the right identity axiom is dependant on the rest of the axiom set; i.e., if e is the left identity, then e is also a right identity. invers2 : Theorem: the right inverse axiom is dependant on the rest of the axiom set; i.e., each element has a right inverse. ident2 : Theorem: the right identity axiom is dependant on the rest of the axiom set; i.e., each element has a right identity. Note that this is a corollary to ident1, but also that the proof is different due to the introduction of a skolem function for the right identity of each element of the group. commutator : Theorem: (commutator thm.) if, for all x in G, x*x*x=e then {{x,y},y}=e, where {x,y}=x*y*inverse(x)*inverse(y) is the commutator of x and y. index : Theorem: all subgroups of index 2 are normal; i.e., if O is a subgroup of G and there are exactly 2 cosets in G/O, then O is normal [that is, for all x in G and y in O, x*y*inverse(x) is back in O]. order2 : Theorem: all groups of order 2 are isomorphic; i.e., if G1 has exactly 2 elements and G2 has exactly 2 elements then there exists an isomorphism [a one-to-one and onto homomorphism] between them. order3 : Theorem: all groups of order 3 are isomorphic; i.e., if G1 and G2 each have exactly 3 elements, then there exists an isomorphism [a one-to-one and onto homomorphism] between them. cyclic : Theorem: all groups of order 5 are cyclic; i.e., there exists an element in G which generates all other elements by taking powers of that element. ---------------------------------------------------------------------- For each problem, there are several standard files, which include one probname.desc file and at least one of each of probname.ver#.in, probname.ver#.clauses, and probname.ver#.out. These contain the following: probname.desc : contains the Natural Language Description of the problem, where available, as well as complete details on each formulation and each version. probname.ver#.in : contains the problem specification, input clauses, and strategy for OTTER; this file is ready to run. In this particular directory, each .ver1 file uses the regular p-formulation; each .ver2 file uses an equality formulation; and each .ver3 and .ver4 file uses an extended p-formulation which specifies in which group each statement is true. probname.ver#.clauses : contains the description, commentary, and the actual clauses (including the denial of the conclusion) used for probname.ver#.in, without any strategy; note that comments always are on lines beginning with a %, preceding the clauses to which they refer, and that clauses terminate with periods. probname.ver#.out : contains the output from running probname.ver#.in with OTTER, with proof if one is found, and with statistics on the clauses generated and CPU time used. HOW TO RUN : ---------------------------------------------------------------------- Invoke OTTER by using the following command : otter < probname.ver#.in [ > outfile ] [ & ] NOTE : '> outfile' may be used to send all output to a file named outfile; '&' may be used to run the program in the background.