Logic Programming - A definite program for the theory of groups

Question

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?

Thanks in advance.

Answer 1

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.