Advent of Code: Combinatorial Logic

Now I was reading a paper where somebody used
modus ponens and these two axioms:


He then claimed that this here is derivable, whereby
later in the paper he presented a derivation:


He also said its not easy to find such a proof
and that he was helped! Can Prolog help?

Maybe using something from here can help:

Meta-interpreter collection for Prolog

Ok, a solution would be SKK = I where S = #7 and K = #8:


It does not take much CPU to find it. First the logic definition, we
need to linearize the axiom schemas with unify_with_occurs_check/2:

:- dynamic typeof/2.

/* modus ponens */
typeof((S*T), B) :-
   typeof(S, (A -> B)),
   typeof(T, A).
/* K axiom */
typeof(k, (A -> _ -> C)) :-
/* S axiom */
typeof(s, ((A -> B -> C) -> (D -> F) -> (E -> G))) :-

Now from THE BOOK, the Craft of Prolog piece here, something
similar like iterative depening, iterative counting:

/* vanilla interpreter with typeof/2 counting */
search(true, N, N).
search((A,B), N, M) :- 
   search(A, N, H), 
   search(B, H, M).
search(typeof(P, T), N, M) :- N>0, H is N-1, 
   clause(typeof(P, T), B),
   search(B, H, M).
search(unify_with_occurs_check(A,B), N, N) :- 

Eh voila the helping hand is finished. And we can use
it as a brain extension, looking for proofs on our behalf:

?- between(1,6,N), search(typeof(X, a->a), N, 0).
N = 5,
X = s*k*k ;

Source code:

craft.p.log (2,1 KB)

1 Like

Here a little foto album of BOOKS for the next beach holiday:

1 Like

(post deleted by author)

1 Like