Chiron: A Multi-Paradigm Logic
William M. Farmer · 2007
Abstract. Chiron is a derivative of von-Neumann-Bernays-Gödel (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. 1