<div class="notebook">

<div class="nb-cell html" name="htm4">
<p>Some Prolog code for Natural Deduction Minimal Logic with DNE:</p>
</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; 'E'(T):_) :- check(G &gt; T:f).
check(G &gt; 'C'(T):A) :- check(G &gt; T:((A=&gt;f)=&gt;f)).

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

dne :-
  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 minimal rule system for 
natural deduction. The rule system is such that 
it also extracts proof terms according to Curry 
Howard isomorphims.</p>

<p>The original system that has combinators 
'E' for Ex Falso Quodlibet and 'C' for Double 
Negation Elimination.</p>

<p>First question, is it fast? With all the
  choices it can do, I guess not:</p>
</div>

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

<div class="nb-cell html" name="htm3">
<p>Second question, is it pretty? I guess it is 
quite verbose, often 'C' is combined with 
  abstraction:</p>
</div>

<div class="nb-cell query" name="q2">
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>