I am trying to get used to Prolog, a logic programming language in which I have to enter statements as positive universal Horn sentences and state queries as existential sentences. Let's consider an example.
I want to model groups. I'd chose the symbols $S=\{e, \circ, ^{-1}\}$, where $e$ is a constant, $\circ$ a binary and $^{-1}$ an unary function, and the following axiom set $\Phi_\text{Grp}$ over $S$:
- $\forall u\forall v\forall w. (u\circ v)\circ w=u\circ(v\circ w)$.
- $\forall u. e\circ v=v\circ e=v$.
- $\forall u. u\circ u^{-1} = e$.
These are clearly universal positive Horn sentences.
Difficulties. In Prolog, there is yet another restriction: there are no function symbols, but only relations. I could introduce a ternary relation $C$ for composition and a binary relation $I$ for inverse with
- $\forall u\forall v\exists c. C(u,v,c)$, read: every two elements have a composite,
- $\forall u,v,w,c,\dotsc,c'''. C(u,v,c)\wedge C(c, w,c') \wedge C(v,w,c'') \wedge C(u, c''') \to c' = c'''$, which models associativity,
and so on. However, the first one is no universal Horn sentence.
Question. I guess FOL with and without function symbols are equivalent (otherwise, I'd bet that one would have included these in Prolog); so how can I define groups in that particular setup?
Edit. I just noticed that I can jump from the latter to the former by passing to Skolem normal form (which introduces function, alas). So to rephrase: Is it possible to bring the (any) problem in an equivalent function-free Skolem normal form?