Horn clause to Prolog

Problem Detail: 

At the needs of my HW at uni I need to transform some Horn clauses to Prolog but I cannot figure out how to do it. I found out some guides but they describe how to do it with only one fact. So can you give me a brief example on how to do it?

Eg John is beautiful and rich

we can transform it at: not (Beautiful(John)) ^ not(Rich(John)) which is a Horn clause right? So how this can be translated it Prolog?

another example Everyone loves somebody. Horn clause: $\forall X \exists Y Loves(X,Y)$ how can this be implemented in Prolog?

Thx in advance

Asked By : Mario

Answered By : Gaste

A horn clause is a disjunction with at most one positive literal, e.g.

\begin{align} \lnot X_1 \lor \lnot X_2 \lor \ldots \lor \lnot X_n \lor Y \end{align}

The implication $X \rightarrow Y$ can be written as disjunction $\lnot X \lor Y$ (proof by truth table). If $X = \lnot X_1 \lor \lnot X_2 \lor \ldots \lor \lnot X_n $, then $\lnot X$ is equivalent to $X_1 \land X_2 \land \ldots \land X_n$ (De Morgan's law). Therefore, the above clause is logically equivalent to

\begin{align} (X_1 \land X_2 \land \ldots X_n) \rightarrow Y \end{align}

A Prolog program basically is a (large) list of horn clauses. A Prolog clause (called rule) is of the form head :- tail., which in logic notation is $head \leftarrow tail$. Therfore, any horn clause

\begin{align} \lnot X_1 \lor \lnot X_2 \lor \ldots \lor \lnot X_n \lor Y \end{align}

is written in Prolog notation as Y :- X1, X2, X3, ..., Xn.

A horn clause containing no positive literal , e.g. $\lnot X_1 \lor \lnot X_2 \lor \ldots \lor \lnot X_n$ can be rewritten as $(X_1 \land X_2 \land \ldots X_n) \rightarrow \bot$, which is :- X1, X2, X3, ..., Xn. in Prolog notation.

Regarding your examples:

1. "John is beautiful and rich", is a CNF, and each clause contains at most one positive literal, hence it can be written in Prolog as beautiful(john). and rich(john).

2. $\forall X \ \exists Y \ \operatorname{Loves}(X,Y)$

   That nested extential quantifier can be eleminated by Skolemization, which is introducing a new function for the extential quantifier inside the universal quantifier: $\forall X \ \operatorname{Loves}(X,p(x))$, which in Prolog notation is loves(X,p(X)).

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/22682