Coloring Subjudgments.

We define a map "turn", computing to which player a given judgment belongs to. The player is Abelard for conjuctive formulas, and Eloise for disjunctive formulas. If the sign is negative it is the opposite. Afterwards, we will color each subjudgment with the color of the player it belongs to.

In[172]:=

(* For t . A, f . A with A conjunctive we set : *)

In[173]:=

turn[Un[_, _], s_]          := SignToPlayer[Dual[s]] ; ... tring, s_] := If[AbbreviationQ[A], turn[Unfold[A], s], SignToPlayer[s]] ;

We define a map taking a judgment, and coloring it with the color of the player it belongs to.

In[182]:=

ColLin[A_, s_] := BoldFace[Size[Col[Lin[A, s], PlayerCol[turn[A, s]]]]] ;

In[183]:=

ColLin[A_, s_, n_] := Col[Lin[A, s, n], PlayerCol[turn[A, s]]] ;

We define a map returning a coloured list of subjudgments for a given judgment.

In[184]:=

CF[A_, s_] := {ColLin[A, s], PCF[A, s]} ;

In[185]:=

PCF[Conj[A_, B_], s_] := {CF[A, s], CF[B, s]} ; PCF[Disj[A_, B_], s_] := {CF[A, s], CF ... rmulas *)PCF[A_String, s_]           := {} ;

The previous map returns a nested list. We define a map returning a flat list.

In[193]:=

ColouredList[F_, s_] := Flatten[CF[F, s]] ;

An example of subjudgement list with colors.

In[194]:=

ColouredList[Impl["MP", Ex["x", "f(x)<=f(x+27)"]], PosSign]

Out[194]=

{.(MP∃x.f(x)<=f(x+27)), .MP, .∃x.f(x)<=f(x+27), .f(x0)<=f(x0+27)}

In[195]:=

ColouredList[Unfold["MP"], PosSign]

Out[195]=

{.∃x.∀y.f(x)≤f(y), .∀y.f(x0)≤f(y), .f(x0)≤f(y0)}

Created by Mathematica  (October 17, 2006)