1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
|
#-------------------------------------------------------------
# Equational specification of a group. This specification does have
# models, i.e. it cannot be refuted (and the prover will note this).
#
# It uses only unit clauses in infix-equational notation.
#
# There exists a right-neutral element (null).
f(X,null)=X.
# For each X, there is a right inverse element i(X).
f(X,i(X))=null.
# f is associative.
f(f(X,Y),Z)=f(X,f(Y,Z)).
# Possible Hypothesis: Right inverse is also left inverse
# <- f(i(a),a) = null.
# A nother possible hypothesis: Multiplication with inverse element is
# commutative.
# ~f(a,i(a)) = f(i(a),a).
|
