Qi II
lambda-the-ultimate.org
lambda-the-ultimate.org
Tarver strikes me as a smart guy doing serious work in an intelligent way. For example, building Qi on top of CL (in such a way that you can drop in to CL whenever you want, though this point is redundant) seems like an obvious win. I don't feel a need to use something that right now, but I'm also skeptical of the "I don't feel a need to use that" feeling... perhaps we are all Blub to Qi!
Unlike Qi I, Qi II allows you to embed sequent rules within functions, evaluating them to closures. These rule closures are type checked and are permeable to having their variables lexically bound from outside the scope of the rule itself. These devices enable the student of computational logic to effortlessly code complex logical systems of all descriptions. Thus the rule
let PTerm/X (replace-by X Term P)
PTerm/X, (all X P) >> Q;
____________________
(all X P) >> Q;
allows universally quantified assumptions to be instantiated to new premises. This rule can be embedded into a Qi II function called all-left which does precisely this job. The rule is turned into a closure by the rule function which is then applied to the problem (list of sequents).
(define all-left
{term --> [sequent] --> [sequent]}
Term S -> ((rule let PTerm/X (replace-by X Term P)
PTerm/X, (all X P) >> Q;
____________________
(all X P) >> Q;) S))
This Virtual Directory does not allow contents to be listed.