MathBus

[ Term Structure | Algebra | Geometry | Logic | Drawing ]
[ Language Bindings | C++ | Java | Lisp | ML ]

Logic

Would like to be able to support the Nuprl term structure and binding models, as well as those of HOL and other theorem provers.

Recognize that although the MathBus term structure includes concepts like variables and binding, these term labels are not related to the variables and binding mechanisms that arise in Logic. Thus, just as special node labels were introduced to represent algebraic variables and algebraic functions special node labels will be produced to represent logic variables and binding mechanisms.