1:- use_module(library(chr)).    2
    3:- chr_type prop --->
    4    atomic(atom) ; top ; bot ; conj(prop, prop) ; impl(prop, prop) ; disj(prop, prop).    5:- chr_type deriv --->
    6    start(natural)       ; top_i                ; bot_e(deriv) ;
    7    conj_i(deriv, deriv) ; conj_e1(deriv)       ; conj_e2(deriv) ;
    8    impl_i(deriv)        ; impl_e(deriv, deriv) ;
    9    disj_i1(deriv)       ; disj_i2(deriv)       ; disj_e(deriv, deriv, deriv).   10
   11%:- table(derives/3).
   12:- chr_constraint derives(?deriv,?,?prop).   13
   14derives(start(N), Gamma, Phi) :- nth0(N, Gamma, Phi).
   15derives(top_i, Gamma, top).
   16derives(bot_e(D), Gamma, Phi) :- derives(D, Gamma, bot).
   17
   18derives(conj_i(A, B), Gamma, conj(Phi, Psi)) :- derives(A, Gamma, Phi), derives(B, Gamma, Psi).
   19derives(conj_e1(D), Gamma, Phi) :- derives(D, Gamma, conj(Phi, Psi)).
   20derives(conj_e2(D), Gamma, Psi) :- derives(D, Gamma, conj(Phi, Psi)).
   21
   22derives(impl_i(D), Gamma, impl(Phi, Psi)) :- derives(D, [Phi | Gamma], Psi).
   23derives(impl_e(A, B), Gamma, Psi) :- derives(A, Gamma, impl(Phi, Psi)), derives(B, Gamma, Phi).
   24
   25derives(disj_i1(D), Gamma, disj(Phi, Psi)) :- derives(D, Gamma, Phi).
   26derives(disj_i2(D), Gamma, disj(Phi, Psi)) :- derives(D, Gamma, Psi).
   27derives(disj_e(A, B, C), Gamma, Xi) :- derives(A, Gamma, disj(Phi, Psi)), derives(B, [Phi | Gamma], Xi), derives(C, [Psi | Gamma], Xi)