%% MIU-system from GEB				-*- mode: prolog -*-
%% Time-stamp: <2023-08-30 18:50:22 philip>

rule(rule1, S, T) :-
    append(_, [i], S),		%ends with I
    append(S, [u], T).		%append U

rule(rule2, [M|X], [M|Y]) :-
    X = [_|_],			%don't duplicate []
    append(X, X, Y).		%duplicate suffixes

rule(rule3, S, T) :-
    append(A, [i,i,i|B], S),	%contains III
    append(A, [u|B], T).	%replace with U

rule(rule4, S, T) :-
    append(A, [u,u|B], S),	%contains UU
    append(A, B, T).		%drop it

%% we will search the theorem-space using IDS.
nat(0). nat(N) :- nat(N0), N is N0 + 1.

deriv0(S, S, [], _).
deriv0(S, T, [(R, S, T)], _) :- rule(R, S, T).
deriv0(S, T, [(R, S, U)|E], N) :-
    N > 0, N0 is N-1,
    rule(R, S, U),
    deriv0(U, T, E, N0).

deriv(S, T, Sol) :-
    nat(N), deriv0(S, T, Sol, N).

%% ?- deriv([m,i], [m,u], R). % solve puzzle from the book 
%% ?- deriv([m,i], X, _).     % enumerate all theorems