Re: Proofs as programs (Was: Advent of Logic 2024: Weekend 3)

On 17/12/2024 16:41, Julio Di Egidio wrote:

On 14/12/2024 22:13, Mild Shock wrote:
 

Create a proof search in Simple Types,
that finds Lambda Expressions as proof,
for a given formula in propositional logic.

 Thinking about it:
 Either by hand or with a 'solve', we/I [*] go from a Goal to a Proof (proof tree).  And, by Curry-Howard, that is (already!) our Type and witnessing Term, i.e. our Proof is a program whose type is the Goal. Indeed, we also already find type-checking: of a Proof against the Goal it alleges to be a proof of.

<snip>
My interpretation might be unorthodox, anyway here is concretely what I am doing (a far better approximation that is): <https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system#Syntax-directed_rule_system>
So yeah, my system definitely qualifies, assuming I meet a deadline that remains a mystery to this point - I guess that's the main challenge.

<https://gist.github.com/jp-diegidio/b6a7a071f9f81a469c493c4afcc5cb11#file-gentzen-pl>

Meanwhile, kindly, for your records:
```
?- case(codile, LT, G), prove(LT, G, Ps), print_ps(Ps).  % v30-alpha
[
   orE(0)
   [
     orIL
     impE(2)
     [
       init(0)
     ]
     [
       init(0)
     ]
   ]
   [
     orIR
     impE(1)
     [
       init(0)
     ]
     [
       init(0)
     ]
   ]
]
LT = pos,
G = ([(p->q),(r->s),p\/r]=>q\/s),
Ps = [orE(0),[orIL,impE(2),[init(0)],[init(0)]],
       [orIR,impE(1),[init(0)],[init(0)]]] .
% 3 more solutions...
```
Have fun,
-Julio