Dolmen_intf.TermSourceInterfaces for Terms. This module defines Interfaces that implementation of terms must respect in order to be used to instantiated the corresponding language classes.
Signature used by the Logic class, which parses languages such as tptp, smtlib, etc... Mainly used to parse first-order terms, it is also used to parse tptp's THF language, which uses higher order terms, so some first-order constructs such as conjunction, equality, etc... also need to be represented by standalone terms.