Theorem proving requires an axiom scheme yielding an enumerable set of axioms of a formal logic system whose formulas and theorems are symbol strings over some finite alphabet that may include traditional symbols of logic (such as , ), probability theory (such as , the expectation operator), arithmetics ( ), string manipulation (in particular, symbols for representing any part of state at any time, such as ). A proof is a sequence of theorems, each either an axiom or inferred from previous theorems by applying one of the inference rules such as modus ponens combined with unification, e.g., [10].
The remainder of this paper will omit standard knowledge to be found in any proof theory textbook. Instead of listing all axioms of a particular in a tedious fashion, we will focus on the novel and critical details: how to overcome potential problems with self-reference and how to deal with the potentially delicate online generation of proofs that talk about and affect the currently running proof generator itself.