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:
- “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).
- $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
