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.


1 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.

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.