# Logic Programming - A definite program for the theory of groups

I am studying theoretical computer science using Ayala's book "Fundamentos da Programação Lógica e Funcional" (the book is written in Portuguese), but the part I am studying right now is based on Lloyd's book "Foundations of Logic Programming".

I am currently in the part about definite programs, trying to solve the following textbook exercise:

Give a definite program for the theory of groups, specified with the axioms $$x \cdot (y \cdot z) = (x \cdot y) \cdot z$$, $$x \cdot e = x$$ and $$x x^{-1} = e$$. Prove that $$e x = x$$ and $$x^{-1} x = e$$.

My doubt is in the beginning. I think that the terms should be formed using the constant $$e$$ (to represent the identity of the group), the unary function $$i$$ (to represent the inverse), the binary function $$\cdot$$ (to represent the group operation) and variables $$x, y, z, \ldots$$ But what should I use as a predicate symbol in my definite program?

I am not sure it's the most elegant approach, but you can use a predicate symbol for equality. Let's denote this predicate symbol by $$eq$$. A definite program for the task would contain the following 3 definite program clauses for the 3 axioms:

$$eq(x \cdot (y \cdot z), (x \cdot y) \cdot z) \leftarrow$$

$$eq(x \cdot e, x) \leftarrow$$

$$eq(x \cdot i(x), e) \leftarrow$$

I would also add the following clauses to operate easily with the idea of equality:

$$eq(x, x) \leftarrow$$

$$eq(x, y) \leftarrow eq(y, x)$$

$$eq(x, y) \leftarrow eq(x, z), eq(z, y)$$

$$eq(x \cdot y, x' \cdot y') \leftarrow eq(x, x'), eq(y, y')$$

$$eq(i(x), i(x')) \leftarrow eq(x, x')$$

Then, proving $$x^{-1} x = e$$ means proving the goal $$G_0: \ \leftarrow eq(i(x) \cdot x, e)$$, which can be done as sketched (I switched to traditional group notation):

1. Obtain $$eq(e, (x^{-1}x) (x^{-1}x)^{-1})$$
2. Obtain $$eq(x^{-1}x, x^{-1}(x x^{-1}) x)$$ and hence obtain $$eq((x^{-1}x) (x^{-1}x)^{-1}, (x^{-1}x) (x^{-1}x) (x^{-1}x)^{-1})$$
3. Obtain $$eq((x^{-1}x) (x^{-1}x) (x^{-1}x)^{-1}, x^{-1} x)$$
4. Combine the results from steps 1, 2 and 3.

Finall, proving $$e \cdot x = x$$ means proving the goal $$G_1: \ \leftarrow eq(e \cdot x, x)$$, which can be done as sketched (I switched to traditional group notation) below:

1. Obtain $$eq(ex, xx^{-1}x)$$
2. Use what we just proved: $$x^{-1} x = e$$ to obtain $$eq(xx^{-1}x, xe)$$.
3. Obtain $$eq(xe, x)$$ and, combining that with the two previous step, the result will follow.