Re: Self-evidently I am not my grandpa

Hi,
A full version that has operator definitions
that also work for Scryer Prolog and that uses a
Quine algorithm that even supports function
symbols like in Mace4 by McCune, is found
here on SWI-Prolog SWISH:
McCunes Mace4 Model Finder
https://swish.swi-prolog.org/p/mace4.swinb
Have Fun!
Mild Shock schrieb:

Its only work if you don't like it, otherwise
its pure logic programming joy. I didn't have
time to try an ancestor formalization yet.
 Yes the requirememt is FOL, from the SWI-Prolog
thread one can extract that I am using the
Vidal-Rosset Variant of the Otten Prover Syntax:
 :- op( 500, fy, ~).     % negation
:- op(1000, xfy, &).    % conjunction
:- op(1100, xfy, '|').  % disjunction
:- op(1110, xfy, =>).   % conditional
:- op(1120, xfy, <=>).  % biconditional
:- op( 500, fy, !).     % universal quantifier:  ![X]:
:- op( 500, fy, ?).     % existential quantifier:  ?[X]:
:- op( 500,xfy, :).
 Thats the Operator definitions in Prolog
to feed the Otten Prover with FOL formulas.
I use the same Operators to feed my model
 finder with FOL formulas. Now I have rewritten
the model finder to give a better output:
 ?- counter(1).
father(0,0)-1
grand_father(0,0)-1
true ;
[...]
father(0,0)-0
father(0,1)-1
father(1,0)-1
father(1,1)-0
grand_father(0,0)-1
grand_father(0,1)-0
grand_father(1,0)-0
grand_father(1,1)-1
true
 This is the cosmetic makeover of the model finder:
 % problem(+Integer, -Formula)
problem(1, (
   ![X]:![Y]:(?[Z]:(father(X,Z) & father(Z,Y)) <=> grand_father(X,Y)) =>
   ~ ?[X]:grand_father(X,X))).
 % counter(+Integer)
counter(K) :-
    problem(K, F),
    between(1, 3, N),
    expand(F, N, G),
    quine(G, M, V),
    V = 0,
    keysort(M, L),
    (member(X, L), write(X), nl, fail; true).
 Plus expand/3 and quine/3 are found here:
https://swi-prolog.discourse.group/t/7398
 Barb Knox schrieb:
 > This is beginning to smell a lot like homework.