I recently discovered that class and instance declarations in Haskell are Horn clauses. So I encoded the arithmetic operations from the first chapter of <i>Art of Prolog</i> into Haskell, in the standar<br><br style="font-family: courier new,monospace;">
<div style="margin-left: 40px;"><span style="font-family: courier new,monospace;">fac(0,s(0)).</span><br style="font-family: courier new,monospace;"><span style="font-family: courier new,monospace;">fac(s(N),F) :- fac(N,X), mult(s(N),X,F).</span><br style="font-family: courier new,monospace;">
<br style="font-family: courier new,monospace;"><span style="font-family: courier new,monospace;">class Fac x y | x -&gt; y</span><br style="font-family: courier new,monospace;"><span style="font-family: courier new,monospace;">instance Fac Z (S Z)</span><br style="font-family: courier new,monospace;">
<span style="font-family: courier new,monospace;">instance (Fac n x, Mult (S n) x f) =&gt; Fac (S n) f</span><br><br></div>I don&#39;t understand, however, to make Haskell instantiate values for variables in a proof. I.e., I don&#39;t understand what the Haskell equivalent of<br>
<br><div style="margin-left: 40px;"><span style="font-family: courier new,monospace;">?- fac(X,Y)</span><br><br></div>would be for some value of X.<br>