Logic Lab

[Mark Tarver]

Work is underway on the Logic Lab which begins with a facility for generating logic rules in sequent calculus directly instead of coding in Shen.

A sequent is defined as an object of type (list prop) * prop where prop is defined by the user.  Here is a rule where prop is defined for propositional calculus.

(39+) (sequent vl ()

   Q >> P;

   R >> P;

   ____________

   [Q v R] >> P;)

(fn f2082) : ((list prop) --> ((list prop) --> ((list prop) --> ((list ((list prop) * prop)) --> (list ((list prop) * prop))))))

(fn f2080) : ((list prop) --> ((list prop) --> ((list prop) --> ((list ((list prop) * prop)) --> (list ((list prop) * prop))))))

(fn vl) : ((list ((list prop) * prop)) --> (list ((list prop) * prop)))

(40+) (vl [(@p [[p v q]] r)])

[(@p [p] r) (@p [q] r)] : (list ((list prop) * prop))

The Logic Lab will be coming in SP 31 in July.

Mark

[Mark Tarver]

Here we have a parameterised rule:

(sequent lemma (Q : prop)

     Q;

     Q >> P;

     _______

     P;)

(fn f4320) : ((list prop) --> ((list prop) --> (prop --> ((list prop) --> ((list ((list prop) * prop)) --> (list ((list prop) * prop)))))))

(fn lemma) : ((list ((list prop) * prop)) --> (prop --> (list ((list prop) * prop))))

Mark