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: Tue, 19 Nov 2024 13:05:34 +0100
Organization: A noiseless patient Spider
Lines: 57
Message-ID: <vhhuuf$1qic1$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>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Tue, 19 Nov 2024 13:05:35 +0100 (CET)
Injection-Info: dont-email.me; posting-host="d0ce389b00a444e2f93f0bf2f9d6d685";
	logging-data="1919361"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX18oR3sDaXCyyvOmnu7Em+eJbLgmmvDQMY8="
User-Agent: Mozilla Thunderbird
Cancel-Lock: sha1:iq+n+ZGYJySPfhb469InVz5Izgs=
Content-Language: en-GB
In-Reply-To: <vhhsit$d108$1@solani.org>
Bytes: 2745

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?"

Now, thanks also to your help, I have fixed my rule for `->E` and now my 
little solver in plain Prolog does it:

```plain
?- solve_test.

solve_test::pos:
- absorp: [(p->q)]=>p->p/\q --> true
- andcom: [p/\q]=>q/\p --> true
- export: [(p/\q->r)]=>p->q->r --> true
- import: [(p->q->r)]=>p/\q->r --> true
- frege_: [(p->q->r)]=>(p->q)->p->r --> true
- hsyll_: [(p->q),(q->r)]=>p->r --> true
solve_test::pos: tot.=6, FAIL=0 --> true.

solve_test::neg:
- pierce: []=>((p->q)->p)->p --> true
solve_test::neg: tot.=1, FAIL=0 --> true.

true.
```

```plain
?- solve(([]=>(p->q->r)->p/\q->r), Qs).
Qs = [
     impi((p->q->r)),
     impi(p/\q),
     impe(1:(q->r)),
     impe(1:p),
     impe(2:r),
     impe(2:q),
     equi(2:r),
     ande(1:(p,q)),
     equi(2:q),
     ande(1:(p,q)),
     equi(1:p)
].
```

In fact, it's still in its infancy and the output is still a flat mess 
with wrong hypothesis numbering, but I will keep working on it with the 
idea of going well past just propositional: will start sharing as soon 
as I manage to implement negation, and a proper proof tree...

-Julio