Path: ...!eternal-september.org!feeder2.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail
From: Julio Di Egidio <julio@diegidio.name>
Newsgroups: sci.logic
Subject: =?UTF-8?Q?Re=3A_can_=CE=BB-prolog_do_it=3F_=28Was=3A_How_to_prove_t?=
 =?UTF-8?Q?his_theorem_with_intuitionistic_natural_deduction=3F=29?=
Date: Fri, 22 Nov 2024 18:30:02 +0100
Organization: A noiseless patient Spider
Lines: 60
Message-ID: <vhqf2q$16mc2$2@dont-email.me>
References: <vhgdq0$19evr$1@dont-email.me> <vhgemi$ca9e$1@solani.org>
 <vhgg23$19evr$2@dont-email.me> <vhhsit$d108$1@solani.org>
 <vhhuuf$1qic1$1@dont-email.me> <vhi5ch$d5rb$1@solani.org>
 <vhqemf$16mc2$1@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Fri, 22 Nov 2024 18:30:03 +0100 (CET)
Injection-Info: dont-email.me; posting-host="71eefe3a736813c653b6f052d99f6b2c";
	logging-data="1268098"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX19pyzwfEcniCrJIq7pU4NQ8VsOTkN01sto="
User-Agent: Mozilla Thunderbird
Cancel-Lock: sha1:ZIHoWUiSw6u56A/I4IKPMlMWhgM=
Content-Language: en-GB
In-Reply-To: <vhqemf$16mc2$1@dont-email.me>
Bytes: 3467

On 22/11/2024 18:23, Julio Di Egidio wrote:
> On 19/11/2024 14:55, Mild Shock wrote:
>> Julio Di Egidio schrieb:
>>> On 19/11/2024 12:25, Mild Shock wrote:
>>>> Can λ-prolog do it? The proof is a little bit
>>>> tricky, since line 1 is used twice in
>>>> line 2 and in line 4. So its not a proof
>>>> tree, rather a proof mesh (*).
>>>
>>> My reduction rules actually take a goal and, if it can be reduced, 
>>> return proof steps and residual goals.  But indeed, my experiment has 
>>> started with "how far can I get without lambda Prolog", aka "why 
>>> lambda Prolog?"
>>
>> I don't know exactly what your full source
>> code in plain Prolog is.
> 
> It's here for your preview, up to disjunction and with a beginning of a 
> proof tree (still with the messed up numbering):
> 
> <https://gist.github.com/jp-diegidio/b6a7a071f9f81a469c493c4afcc5cb11>
> 
> And it fails one test:
> 
> ```
> ?- solve_t.
> pos:begin:
> - absorpt   : [(p->q)]=>p->p/\q             : ok
> - andcomm   : [p/\q]=>q/\p                  : ok
> - codilem   : [(p->q),(r->s),p\/r]=>q\/s    : FAIL!
> - distand   : []=>p/\(q\/r)<->p/\q\/p/\r    : ok
> - distor    : []=>p\/q/\r<->(p\/q)/\(p\/r)  : ok
> - export    : [(p/\q->r)]=>p->q->r          : ok
> - import    : [(p->q->r)]=>p/\q->r          : ok
> - frege     : [(p->q->r)]=>(p->q)->p->r     : ok
> - hsyllo    : [(p->q),(q->r)]=>p->r         : ok
> - idempand  : []=>p/\p<->p                  : ok
> - idempor   : []=>p\/p<->p                  : ok
> pos:end: tot.=11, failed=1 : FAIL!
> neg:begin:
> - pierce    : []=>((p->q)->p)->p            : ok
> neg:end: tot.=1, failed=0 : ok
> false.
> ```
> 
> And I have already spent a day trying to find the bug, the trace is a 
> little bit overwhelming:
> 
> ```
> ?- solve_trace([p->q,r->s,p\/r]=>q\/s, Qs).
> ```

Never mind, I have fixed it: just needed to get rid of those `once`! 
Will update the Gist shortly.

If you have any feedback already, it's very welcome: anyway, will keep 
you guys posted.

-Julio