SMT
type: FormalLanguage
comment: The LISP-like language of the SMT Library as defined at http://combination.cs.uiowa.edu/smtlib/

FormalProof
type: Class
comment: Formal proofs in a logical calculus.
subclass of: Proof

InformalProof
type: Class
subclass of: Proof
comment: Informal proofs, e.g., in mathematical vernecular.

format
type: FunctionalProperty
range: FOProblemFormat
comment: The format of the TSTP proving problem, either FOF (first-order-formula) or CNF (clause normal form).
type: ObjectProperty
domain: http://lodlaundromat.org/.well-known/genid/e24b0299dfe23c4ae7cb179870101668#60

ClassicalNDCalculus
type: Class
subclass of: NDCalculus
comment: ND

OMDoc
type: FormalLanguage
comment: The OMDoc language as described at http://www.mathweb.org/omdoc/

ConstructiveNDCalculus
type: Class
subclass of: NDCalculus
comment: NI

BfFPResolutionCalculus
type: Class
comment: A resolution calculus that uses only the rules Binary resolution, Factoring and Paramodulation.
subclass of: ResolutionCalculus

TSTP
type: FormalLanguage
comment: The TSTP language as defined at http://www.cs.miami.edu/~tptp/TSTP/

timeRes
type: ObjectProperty
comment: CPU and/or wallclock time (in secs) available to solve a given problem, or perform a certain task.
domain: http://lodlaundromat.org/.well-known/genid/e24b0299dfe23c4ae7cb179870101668#44
range: TimeResource
type: FunctionalProperty

time
type: ObjectProperty
type: FunctionalProperty
range: TimeResource
domain: http://lodlaundromat.org/.well-known/genid/e24b0299dfe23c4ae7cb179870101668#49
comment: CPU and wallclock time (in msecs) that was needed to generate a problem, result, etc.

cpuTime
type: DatatypeProperty
comment: The CPU time of the time resource in seconds.
type: FunctionalProperty
domain: TimeResource
range: integer

wallClockTime
type: DatatypeProperty
domain: TimeResource
comment: The wall clock time of the CPU of a time resource in seconds.
range: integer
type: FunctionalProperty

twelfDocument
type: FunctionalProperty
domain: Logic
comment: A URL pointing to a twelf document defining the logic.
type: DatatypeProperty
range: string

TPTP
type: FormalLanguage
comment: The TPTP language as defined at http://www.cs.miami.edu/~tptp/TPTP/SyntaxBNF.html

fo horn
type: FOProblemFeature
comment: Problem is in CNF and only consists of horn clauses.
name: Horn
code: HRN

fo equality
type: FOProblemFeature
name: equality
code: EQU
comment: super feature of all other equality features.

fo noEquality
type: FOProblemFeature
code: NEQ
comment: Problem contains no equality at all.
name: noEquality

fo sat
type: FOProblemFeature
code: SAT
name: sat
comment: Problem is known as satisfiable.

fol plus equ
type: FOLogic
comment: Classical first-order predicate logic with equality as described in..

fo unitPureEquality
type: FOProblemFeature
comment: Problem is in TSTP CNF format, contains only equality atoms and they all occur in unit clauses.
name: unitPureEquality
code: UEQ

fo someEquality
type: FOProblemFeature
comment: Problem contains some equality atoms.
code: SEQ
name: someEquality

fo nonUnitPureEquality
type: FOProblemFeature
comment: Problem is in TSTP CNF format and contains only equality atoms but some of them occur in non-unit clauses.
name: nonUnitPureEquality
code: NUE

OpenMath
type: FormalLanguage
comment: The OpenMath language as described at http://www.openmath.org/cocoon/openmath/standard/index.html

fo fofForm
type: FOProblemFeature
code: FOF
comment: Problem is in TSTP FOF format.
name: fofForm

NBG
type: SetTheory
comment: Neumann, Bernays, Goedel set theory.

fo theorem
type: FOProblemFeature
comment: Problem is known as a theorem.
name: theorem
code: THM

fo pureEquality
type: FOProblemFeature
code: PEQ
name: pureEquality
comment: Problem contains only equality atoms.

test proving problem
type: ProvingProblem
comment: only for testing
formal description: afasfdafd
in logic: fol plus equ
language: OMDoc

fo essentiallyProp
type: FOProblemFeature
comment: Problem is essentially propositional, e.g., it doesn't contain any variables.
code: EPR
name: essentiallyProp

QF UF
type: SmtTheory
comment: Closed quantifier-free formulas built over an arbitrary expansion of the empty signature with free sort, function and predicate symbols. Note that the formulas can contain term (resp., formula) variables as long as they are bound by a let (resp., flet) construct. Also, formulas in ite terms must be themselves quantifier-free.
in logic: fol plus equ
format: FOF

fo notHorn
type: FOProblemFeature
name: notHorn
comment: Problem does not only contain Horn clauses.
code: NHN

test fof problem
type: TstpFOFProblem
time res: test time resource
in logic: fol plus equ
prob name: test_fof_problem
formal description: input_formula(foo,conjecture,(equal(bar,bar))).

ZF
type: SetTheory
comment: Zermelo Fraenkel set theory.

HOL
type: HOLogic
comment: like in Isabelle/HOL