Chiron: A Multi-Paradigm Logic

William M. Farmer

2010

Abstract

Chiron is a derivative of von-Neumann-Bernays-Goedel (NBG) set theory
that is intended to be a practical, general-purpose logic for
mechanizing mathematics.  It supports several reasoning paradigms by
integrating NBG set theory with elements of type theory, a scheme for
handling undefinedness, and a facility for reasoning about the syntax
of expressions.  This paper gives a quick, informal presentation of
the syntax and semantics of Chiron and then discusses some of the
benefits Chiron provides as a multi-paradigm logic.