Path: ...!weretis.net!feeder8.news.weretis.net!reader5.news.weretis.net!news.solani.org!.POSTED!not-for-mail
From: Mild Shock <janburse@fastmail.fm>
Newsgroups: sci.logic
Subject: Re: Self-evidently I am not my grandpa
Date: Tue, 30 Apr 2024 20:04:10 +1000
Message-ID: <v0qfmr$6vn6$1@solani.org>
References: <v0hvp5$25uj$1@solani.org>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Tue, 30 Apr 2024 10:04:12 -0000 (UTC)
Injection-Info: solani.org;
	logging-data="229094"; mail-complaints-to="abuse@news.solani.org"
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
 Firefox/91.0 SeaMonkey/2.53.18.2
Cancel-Lock: sha1:6OOMnzJiuVgcKEZtn+EXuiRq5kw=
In-Reply-To: <v0hvp5$25uj$1@solani.org>
X-User-ID: eJwNxcEBwCAIA8CViECUcRBh/xHa+5wrwdpGp/n4IMFb6HV65cYNH6N6XCuejNoPJWjn/edC5/OOw5DRFtEPTn4VJg==
Bytes: 2585
Lines: 60

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.