Printing the view in sequent form.

These maps take a  list L of integers, an integer i, and return the sublist of all integers < i (all integers > i):

In[294]:=

LessThan[L_, i_] := Select[L, Function[x, x<i]] ;

In[295]:=

MoreThan[L_, i_] := Select[L, Function[x, x>i]] ;

This maps takes a list {n_1, ..., n_k} of integers, and returns the sequent of all formulas of index n_1, ..., n_k, in the usual syntax.

In[296]:=

Sequent[L_] := Map[Lin, Map[FormInd, L]] ;

This maps takes a list {n_1, ..., n_k} of integers, and returns the sequent all formulas of index n_1, ..., n_k  and < i (and > i) in the usual syntax.

In[297]:=

SequentLess[L_, i_] := Sequent[LessThan[L, i]] ;

In[298]:=

SequentMore[L_, i_] := Sequent[MoreThan[L, i]] ;

We explain how to make evident formula of index i in a one-sided sequent. This maps takes a list {n_1, ..., n_k} of integers, an index n_i, and prints the sequent of all formulas of index n_1, ..., n_k in the usual syntax, with the formula n_i in bold.

In[299]:=

PrintSequent[L_, i_] := Print[SequentLess[L, i] , ",",  BoldFace[Lin[FormInd[i]]] ,  ",",  SequentMore[L, i] ] ;

Printing a sequent of Classical Logic. This map takes two lists {n_1, ..., n_k}, {m_1, ..., m_h} of integers, an index n_i in the first list, and returns the two-sided sequent Γ,A,Γ'|-Δ of Classical Logic, having all formulas of index n_1, ..., n_k and m_1, ..., m_h in the left- and right-hand-side. Formulas in the usual syntax, with the formula n_i in the left-hand-side in bold. Another map does the same when the index m_j is in the right-hand-side.

In[300]:=

(* i index of the left - hand - side *)PrintSequentLeft[L_, M_, i_, "Clas ... ;PrintSequent[L, i] ; Print[ BoldFace["⊢"]] ; Print[Sequent[M]]] ;

In[301]:=

(* j index of the right - hand - side *)PrintSequentRight[L_, M_, j_, "Cl ... ;Print[Sequent[L]] ; Print[ BoldFace["⊢"]] ; PrintSequent[M, j]] ;

Printing a sequent of Intuitionistic Logic. These maps takes the same parameters of the previous ones, but they return a two-sided sequent Γ,A,Γ'|-D or Γ|-A of Intuitionistic Logic. The difference is that, in intuitionistic logic, the right-hand-side has at most one formula, which is the last formula of the right-hand-side in the classical sequent if any. In the intuitionistic case, if the formula we print in bold in is the right-hand-side, then it is the unique formula of the right-hand-side.

In[302]:=

(* i index of the left - hand - side *)PrintSequentLeft[L_, M_, i_, "Intuitionistic"] := PrintSequentLeft[L, M, i, "Classical"] ;

In[303]:=

(* j index of the right - hand - side . j is the only formula in the intuitionistic right - ha ... L]] ; Print[ BoldFace["⊢"]] ; Print [BoldFace[Lin[FormInd[j]]]]] ;

This map takes a list and return a list having only the last element of the original list, empty if the original list is empty.

In[304]:=

LastIfAny[L_] := If[L {}, {}, {Last[L]}] ;

Printing a sequent of LCM. This map selects the formulas having the sign of the player in the list of formulas visible  in LCM.

In[305]:=

SignedBranch[p_, pview_, psign_] := Select[Branch[p, pview], Function[i, FormSign[i] psign]] ;

These maps takes the same parameters of the previous ones, but they return a two-sided sequent Γ,A,Γ'|-Δ or Γ|-Δ,A of LCM. The right-hand-side is linearly ordered by the father/child relation on formulas. If the formula printed in bold is in the right-hand-side, then it is the last one.

In[306]:=

(* i index of the left - hand - side *)PrintSequentLeft[L_, M_, i_, "LCM"] := PrintSequentLeft[L, M, i, "Classical"] ;

In[307]:=

(* j index of the right - hand - side . j is the last formula in the LCM right - hand - side . ... ot;⊢"]] ; Print [Sequent[Most[M]], ",", BoldFace[Lin[FormInd[j]]]]] ;

Printing the view in sequent form. This function prints the sequent associated to the view player p from turn pview. The formula of index CurrentPlay and sign s is printed in bold. For each case we compute the right-hand-side. In the intuitionistic case, is the last visible formula (if any). In the LCM case, are the LCM visible formulas having the same sign of the player. In the Classical case, are the visible formulas having the same sign of the player.

In[308]:=

PrintSequent[p_, s_, pview_, CurrentPlay_] := CompoundExpression[psign = PlayerToSign[ ... lay, Logic], PrintSequentRight[LeftSequent, RightSequent, CurrentPlay, Logic]] ] ;

Created by Mathematica  (October 17, 2006)