% problem-set/algebra/groups/Group.ax.eq.clauses % created : 07/21/86 % revised : 08/11/88 % description: % % The following axioms define a group; the equality substitution axioms for % f and g as well as the symmetry and transitivity axioms for equality are % not included, since the problem is being represented in extended first order % predicate calculus, where equality is built in. % representation: % % declare_predicate(1,[O]). % declare_predicate(2,[EQUAL]). % declare_function(1,[g]). % declare_functions(2,[f,l]). % declare_constants([e,a,b,c,d,h,j,k]). % declare_variables([x,y,z]). % % O(x) : membership in a subgroup of index 2 (see index) % g(x) : inverse of x % f(x,y) : names the product of x and y % l(x,y) : names an element in O (see index) % e : identity element % For any x and y in the group x*y is also in the group. No clause is needed % here since this is an instance of reflexivity given as EQUAL(x,x). % There exists an identity element 'e' defined below. % left identity EQUAL(f(e,x),x). % right identity EQUAL(f(x,e),x). % For any x in the group, there exists an element y such that x*y = y*x = e. % left inverse EQUAL(f(g(x),x),e). % right inverse EQUAL(f(x,g(x)),e). % The operation '*' is associative EQUAL(f(f(x,y),z),f(x,f(y,z))). % The operation '*' is well-defined. No clause is needed here since this % is an instance of reflexivity given as EQUAL(x,x). % reflexivity EQUAL(x,x).