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:23:27 +0100
Organization: A noiseless patient Spider
Lines: 53
Message-ID: <vhqemf$16mc2$1@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>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Fri, 22 Nov 2024 18:23:28 +0100 (CET)
Injection-Info: dont-email.me; posting-host="71eefe3a736813c653b6f052d99f6b2c";
	logging-data="1268098"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX194lKYaoEFaxU1uJ3NhBcU1O/m49HGafHc="
User-Agent: Mozilla Thunderbird
Cancel-Lock: sha1:ZUW2Vg/bcrUz8uYokkbNJiuZthA=
In-Reply-To: <vhi5ch$d5rb$1@solani.org>
Content-Language: en-GB
Bytes: 2961

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).
```

-Julio