<div class="notebook">

<div class="nb-cell html" name="htm5">
Some Prolog code for Natural Deduction Minimal Logic with RAA:
</div>

<div class="nb-cell program" name="p1">
:- op(1100, xfy, '|').  % disjunction
:- op(1110, xfy, =&gt;).   % implication

:- op(200, fy, /).      % co-abstraction
:- op(400, yfx, #).     % co-application

% -----------------------------------------------------------------
prove(F,P) :- between(1,11,I), count(check([]&gt;P:F),I,0).

type(P,F) :- check([]&gt;P:F).

:- dynamic check/1.
check(G &gt; U:A) :- member(U:B, G), unify_with_occurs_check(A, B).
check(G &gt; (\U:T):(A=&gt;B)) :- check([U:A|G] &gt; T:B).
check(G &gt; (S*T):B) :- check(G &gt; S:(A=&gt;B)), check(G &gt; T:A).
check(G &gt; (/U:T):A) :- check([U:(A=&gt;f)|G] &gt; T:f).

% -----------------------------------------------------------------

raa :-
  time(once(prove((((a=&gt;b)=&gt;a)=&gt;a),_))).

% -----------------------------------------------------------------
prove(F) :-
   prove(F,P), !,
   show(P, 0'x).
prove(_) :-
   write('n.a.'), nl.

type(P) :-
   type(P,F), !,
   show(F, 0'a).
type(_) :-
   write('n.a.'), nl.

test :-
   write('Ex Falso: '), prove((f=&gt;a)),
   write('Clavius\'s Law: '), prove((((a=&gt;f)=&gt;a)=&gt;a)),
   write('Double Neg: '), prove((((a=&gt;f)=&gt;f)=&gt;a)),
   write('Peirce\'s Law: '), prove((((a=&gt;b)=&gt;a)=&gt;a)).

% -----------------------------------------------------------------
count(true, J, J).
count((A,B), J, K) :- count(A, J, I), count(B, I, K).
count(check(H), J, K) :- J&gt;0, I is J-1, clause(check(H), B), count(B, I, K).
count(member(X,L), J, J) :- member(X,L).
count(unify_with_occurs_check(A,B), J, J) :-  unify_with_occurs_check(A,B).

% -----------------------------------------------------------------
show(T, Z) :-
   term_variables(T, V),
%   term_singletons(T, _A),
   term_names(V, _A, Z, 0),
   write(T), nl.

term_names([], _, _, _).
% term_names([V|L], [W|R], Z, K) :- V == W, !,
%    V = '!',
%    term_names(L, R, Z, K).
term_names([N|L], A, Z, K) :-
   term_name(K, N, Z),
   J is K+1,
   term_names(L, A, Z, J).

term_name(K, N, Z) :- K &lt; 3, !,
   J is K+Z,
   char_code(N, J).
term_name(K, N, Z) :-
   J is (K rem 3)+Z,
   H is K//3+1,
   number_codes(H, L),
   atom_codes(N, [J|L]).
</div>

<div class="nb-cell html" name="htm2">
<p>A little generic rule executor using iterative 
counting. Applied to Kleenes rule system for 
natural deduction. The rule system is such that 
it also extracts proof terms according to Curry 
Howard isomorphims.</p>

<p>Unlike the original system that had combinators 
'E' for Ex Falso Quodlibet and 'C' for Double 
Negation Elimination. We use a new abstraction,
that has 'C' built-in.</p>

<p>First question, is it fast? Its faster than 
  'E' and 'C' combinators. Here Peirce's Law again:</p>
</div>

<div class="nb-cell query" name="q2">
raa.
</div>

<div class="nb-cell html" name="htm3">
<p>Second question, is it pretty? Well see for yourself, it has an interesting features, Ex Falso is recognited when the binder is unused, seen by '!':</p>
</div>

<div class="nb-cell query" name="q1">
test.
</div>

<div class="nb-cell html" name="htm1">
<p>Disclaimer: We don’t make it exactly H-IPC from Kleene, 
  since we do allow (A =&gt; (A =&gt; B)) =&gt; (A =&gt; B), i.e. we 
  allow left contraction. And since we set ~A = A =&gt; f, 
  we also got the law of non-contradiction.</p>

More propositional logic Prolog notebooks here:<br>
<a href="https://swish.swi-prolog.org/p/Logic.swinb">Logic</a>
</div>

<div class="nb-cell html" name="htm4">

</div>

</div>