Re: Self-evidently I am not my grandpa

Jeff/Barb you might be highly confused! This is Prolog:
grand_father(X,Y) :- father(X,Z), father(Z,Y).
But this is FOL:
∀X∀Y(∃Z(father(X,Z) & father(Z,Y)) <=> grand_father(X,Y)).
The manual method to go from Prolog to FOL is
the so called Clark Completion. It was recently
made popular again by SWI-Prolog's s(CASP),
but the method exists already quite long:
Logic Programming Theory Lecture 8: Clark Completion
https://www.inf.ed.ac.uk/teaching/courses/lp/2012/slides/lpTheory8.pdf
But I am using it manually as well here. You see
the FOL formula I used as input to the model finder
in the problem/2 fact:
% problem(+Integer, -Formula)
problem(1, (
   ![X]:![Y]:(?[Z]:(father(X,Z) & father(Z,Y)) <=> grand_father(X,Y)) =>
   ~ ?[X]:grand_father(X,X))).
Jeff Barnett schrieb:

You also forgot that you posed this as a Prolog, not an FOL, problem.