The practical employment of automated deduction systems requires the user to input problem statements in a well-formed string representation. While this presentation is usually fixed by the respective system, the various language dialects of the TPTP library are meanwhile accepted as a de-facto standard for all current automated theorem provers based on classical logics. In the context of reasoning in non-classical logics, however, only a few limited standardization approaches exist, with QMLTP being the most notable exception. To move standardization forward, we outline conservative extensions to the TPTP language that allow systematic syntax definitions for various expressive, non-classical logics. These logics include higher-order versions of modal logics, conditional logics, hybrid logics, free logics, and many-valued logics. We are convinced that a standard syntax for prominent non-classical logics will not only facilitate their deployment but also support the development and comparability of corresponding theorem proving systems.
Computer-assisted reasoning in non-classical logics is of increasing interest to enable and
support applications in e.g. computer science, mathematics and philosophy. Several
powerful automated and interactive theorem proving systems have been developed over the
past decades. However, when it comes to quantified logics, most of the available systems
focus on classical logic only. Amongst the notable exceptions is MleanCoP [
Orthogonal to the development of specialized provers, the semantical embedding
approach [
In order to amplify the practical development, deployment and comparison of automated reasoning in quantified non-classical logics, we therefore outline problem representation formats for various (quantified) non-classical logics, primarily for use in automated
TPTP and QMLTP. The Thousands of Problems for Theorem Provers problem
library (TPTP) [
A closely related project is QMLTP [
We primarily address quantified versions of non-classical logics in this paper. Since we do
not intend to (artificially) restrict these logics to be first-order only, their representation
formats will quite naturally be given as extensions of (classical) higher-order logic (HOL) [
HOL is a typed logic. The set of simple types T contains all types that are freely generated using the binary function type constructor → and a set of base types, usually chosen to be {o, ι} for Booleans and individuals, respectively. Terms of HOL are given by the following grammar:
s, t ::= cτ | Xτ | (λXτ . sν )τ→ν | (sτ→ν tτ )ν where cτ ∈ Στ is a constant symbol from the (typed) signature Σ := Sτ Στ and Xτ is a variable. The type of a term is explicitly stated as subscript but may be dropped for legibility reasons if obvious from the context. Terms so of type o are formulas.
In general, we require Σ to contain a complete logical signature. To that end, we choose Σ to consist at least of the primitive logical connectives for disjunction, negation, and, for τ each type, equality and universal quantification. Hence, we have {∨o→o→o, ¬o→o, =τ→τ→o Π(ττ→o)→o} ⊆ Σ for all τ ∈ T .1 Optionally, we add choice operators and definite description operators ι for all types. Depending on the logics we are addressing in the following, the concrete set of constants (hence also connectives, quantifiers, etc.) Σ will actually vary. Often, we will only add further constants to the above ones. In all other cases, we will specify Σ explicitly.
1 The remaining logical connectives can be defined as usual, e.g. conjunction by ∧ := λso.λto.¬(¬s ∨ ¬t). thf(1, type, (p: ($i > $i) > $o)). thf(2, conjecture, (? [F: $i > $i]:
(p @ F = p @ (^ [X: $i]: X)))).
The semantics of HOL is now briefly addressed. A frame {Dτ }τ∈T is a collection of non-empty sets Dτ such that Do = {T, F } (for truth and falsehood, respectively) and Dτ→ν ⊆ Dν Dτ is a collection of functions from Dτ to Dν . An interpretation is a pair M = ({Dτ }τ∈T , I) where {Dτ }τ∈T is a frame and I is a function mapping each constant cτ to some denotation in Dτ . We assume that the primitive logical connectives are assigned their usual denotation. Given a variable assignment g we can define a valuation k.kM,g by kcτ kM,g kXτ kM,g ksτ→ν tτ kM,g kλXτ . sν kM,g = = = =
I(cτ ) g(Xτ ) ksτ→ν kM,g ktτ kM,g
s M,g[z/Xτ ] f : z 7−→ k k ∈ Dτ→ν where g[z/Xτ ] denotes the variable assignment that maps Xτ to z and every other variable Yν to σ(Yν ), where Yν 6= Xτ .
A formula so is called valid, iff ksokM,g = T for every variable assignment g and every
interpretation M. We call M a standard model iff Dτ→ν is the complete set of total
functions, i.e. Dτ→ν = DνDτ . As a consequence of Go¨del’s Incompleteness Theorem [
A de-facto standard representation of HOL problems for automated theorem provers
is given by the THF dialect [
We will use the THF dialect as a starting point for the development of specific representations of quantified non-classical logics in the following section. 3
In this section, we outline possible conservative extensions to the TPTP THF dialect in order to capture various quantified non-classical logics, to be used as input language of suitable ATP systems. The here discussed logics are modal logics, hybrid logics, conditional logics and free logics, each of them in a higher-order quantified version. Also, we briefly discuss means of representation for many-valued logics. 3.1
”Modal logic” refers to a family of non-classical logics that are used to express and reason
about modal qualities of truth. To that end, the operators and are added to the usual
classical logic language and characterized by appropriate rules and axiomatizations.
Notions of necessity and possibility are probably the most prominent of such modal concepts
represented by the new operators, but many further related systems and interpretations
(e.g. focusing on temporal or deontic aspects) exist. Modal logics are not only of strong
interest for the interpretation of philosophical arguments, but have also become increasingly
important to mathematics and computer science [
Syntax and semantics. We now briefly sketch the syntax and semantics of
higherorder modal logics (HOML) [
The syntax definition is nearly identical to that of HOL. We merely add the box operators io→o (for all i ∈ I) to the set of constants Σ. Their duals, the diamond operators i, can be defined by io→o := λΦo. ¬( i(¬Φ)).
For the semantics of HOML, we augment the concept of a HOL model with Kripke (possible world) semantics, yielding a HOML model structure M:
M = where W is a set of worlds, the Ri ⊆ W × W are accessibility relations between the worlds of W , and each Iw is an interpretation function (similar to I of §2) for world w. We assume that connectives are always given the standard interpretation by Iw in each world w ∈ W .
In a final step, we augment the valuation function k.kM,g for HOL models to a valuation . M,g,w for HOML models M, a variable assignment g and a world w ∈ W by function k k k
isokM,g,w = T iff for all v ∈ W such that wRiv it holds that ksokM,g,v = T
The semantics definition stated here are only adequate for constant domain semantics
in which we assume the domains Dτ to be the same for all worlds w ∈ W . However, if we
assume varying domain semantics (or their restricted forms of cumulative or decreasing
domains), we need to further augment the above model. Instead of a single frame D :=
{Dτ }τ∈T we employ a family of frames {Dw}w∈W , one for each world. Additionally, the
valuation of universal quantification is appropriately adjusted. We refer to the literature
for details (cf. e.g. [
We are in a higher-order setting. Hence, bridge rules (e.g. iφ =⇒ j φ) can simply be postulated as axioms (e.g. ∀φ( iφ =⇒ j φ)). Consequently, we can avoid a specific representation for bridge rules below. However, such axioms should possibly be marked specifically so that provers can easily recognize them (similar to TPTP definitions) and apply special techniques where possible.
The above definitions give us modalities with logic K properties. In order to obtain stronger logics, such as KB, KD, S4 and S5, we e.g. could, analogous to the above bridge rules, postulate respective axioms. However, it seems to us that this approach would be impractical and too verbose. Hence, we include a special syntax for postulating frame conditions to the modalities below.
2 Mixed uses of constant and varying domain quantifiers occur for example in variants of the ontological
argument for the existence of God; cf. Anderson [
The ! quantifier respects some quantification semantics that is chosen by the user. Additionally, we add four new quantifiers !=, !~, !+, !- that always denote constant, varying, cumulative and decreasing domain quantification semantics, respectively, regardless of the default setting for !. Existential variants are added analogously.
Global parameters. There are several parameters that adjust the exact meaning of modal logic problems. One of this parameters was already mentioned above, namely whether we use constant domain or variants of varying domain semantics. Another important point is the rigidity of constant symbols: Does every symbol denote the same object in every world? The global parameters for the problem input considered here are: quantification Sets the quantification semantics for the ! and ? symbols of the language.
Valid values: constant, varying, cumulative, or decreasing.
Default value: constant. constants Sets the default interpretation constraint for constant symbols, i.e. whether constant symbols have the same denotation in every world (called rigid) or not. Valid values: rigid or dependent.
Default value: rigid. consequence Specifies the precise meaning of the logical consequence relation S |= t where S = {s1, . . . , sn} is a set of formulas. In thet giffl=o∀bMaTl,)gci.am(s(e∀pwlwie.eskskh1takkvMMe,:,gg,,wwS |== t iff ∀M, g.∀w.((ks1kM,g,w = T and . . . and ksnkM,g,w T ). In the local case we instead have S |= = T and . . . and ∀w.ksnkM,g,w = T ) implies ∀w.ktkM,g,w = T ).
Valid values: local or global.
Default value: local. modalities Sets which different modalities are defined within the problem. For each indexed modality, the respective index name is given. If not stated, a mono-modal logic is assumed where the default box and diamond operators (i.e. #box and #dia without name qualification) are used in the problem.
Example: (a,s5) defines an indexed modality named a with S5 axiomatization. These parameters need to be included in the problem description using the TPTP process instruction language (TPI)3 which, amongst other aspects, allows adding meta statements about the problem setting. An exemplary multi-modal setting with cumulative domain semantics, rigid constant interpretation, and a global consequence relation is given by tpi(1, set_logic, modal([’quantification’ = ’cumulative’, ’constants’ = ’rigid’, ’consequence’ = ’global’ ’modalities’ = [(a, s5), (b, kb), (c, k)]])).
3A proposal for the TPI language can be found at http://www.cs.miami.edu/~tptp/TPTP/Proposals/ TPILanguage.html. Here, three different indexed modalities a, b and c are introduced with the given axiomatizations S5, KB and K, respectively. Valid axiomatization schemes for modalities include k, kb, k4, k5, d, m, b, s4 and s5. There have been more systems presented in the literature. Hence, this list could/should be appropriately extended.
Per-Symbol Options. As a convenience feature, we allow per-symbol specification of rigidity, allowing some symbols to be rigid and some symbols to be world-dependent. More specifically, all symbols introduced using type statements have the default rigidity as stated by the constants option of the set_logic statement, unless overridden by another set_logic statement specifically for that new constant. In the following example, the constant symbol q is a rigid symbol while p is world-dependent as stated by statement 4: tpi(1, set_logic, modal([’quantification’ = ’cumulative’, ’constants’ = ’rigid’, ’modalities’ = [(a, s5), (b, kb), (c, k)]])). hmf(2, type, (q: $i)). hmf(3, type, (p: $i)). tpi(4, set_logic, hmf(p, ’dependent’)). 3.2
Hybrid logic [
Syntax and semantics. Classically, nominals are introduced in propositional and first-order logic by introducing new cases into the syntax BNF and adjusting the models accordingly. Additional to HOML we need to introduce the nominals, the satisfaction operator @, and the shifter ↓ to the BNF over a set N OM .4
n ∈ N OM The semantics is build on the same model as ordinary modal logic.
M = The variable assignment g = (gi, gn) is adorned with an extra variable assignment gn, that maps nominals to worlds. The assignment gi is the variable assignment from standard higher-order modal logic.
The valuation k.k is then augmented for formulas containing nominals, given by
knkM,g,w
k@nϕkM,g,w
k ↓ ϕo→okM,g,w
=
=
=
gn(n) ≡ w.
kϕkM,g,gn(n)
kϕnkM,g,w
n ∈ N OM
where n is free in ϕ
and gn(n) = w
4Higher-Order Hybrid Logics have not yet been researched. They can be conceived as a straight-forward
adaptation of propositional and first-order hybrid logic to HOL. Another possibility is to introduce a new type
for nominals. This would yield a solution, that resembles the embedding approach [
Since hybrid logic is an extension of ordinary modal logic, we can still obtain the stronger logics stated by the frame conditions K B, K D, S4, S5 as usual. On the other hand, nominals allow the formulation of frame conditions, that were not previously expressible in ordinary modal logic. For example, the condition n ⇒ ¬n for n ∈ N OM , for instance, corresponds to an irreflexivity condition. As in the last section we allow to name the new frame conditions explicitly.
Representation. We extend the hmf syntax for ordinary modal logic described before and add the two new syntax features described above. To distinguish nominals from ordinary Boolean constants, we introduce a new type, called $nominalType. In a formula the nominal is grounded to Boolean type, by introducing a new predicate #nom. A nominal n has then to be written as #nom(n) inside a formula. We propose to adopt the satisfaction and shifter operator with an explicit binding mechanism: #at(n) : p for @n p, and #shift [n] : p for ↓ (λX . p). Thereby, in both cases, the operator takes as first argument only nominals. The remaining syntax containing modal operators and higher-order features are the above described hmf based on the standard THF. A short example (where n1 is a nominal) is given by: hhf(1, type, p : $i > $o). hhf(2, type, n1 : $nominalType). hhf(3, conjecture, (#shift[n] : (#at(n1) :
![X : $i] : (p(X) => #at(n) : p(X))))).
Global parameters. Hybrid logic is an extension to ordinary modal logic, with the same parameters. The same options for quantification, constants, and consequence can be given, as well as giving each symbol a rigid or dependent. In theory a range of additional frame conditions can be given for the modalities, but in practice hybrid logic is used in common frame settings. Hence we suggest to use the exact same (resp. suitably adapted) notation as for ordinary higher-order modal logic. 3.3
Conditional logics [
6The extension of quantified conditional logic to full higher-order conditional logic as presented here is ad hoc and straight-forward. Whether there are any particular complications arising from that extension still needs to be inspected. ID MP
CS CEM AC RT CV CA
Axiom Condition
Axiom Condition
Axiom Condition
Axiom Condition
Axiom Condition
Axiom Condition
Axiom Condition
Axiom Condition
A −→ A f (w, [A]) ⊆ [A] (A −→ B) =⇒ (A =⇒ B) w ∈ [A] =⇒ w ∈ f (w, [A])
(A ∧ B) =⇒ (A −→ B) w ∈ [A] =⇒ f (w, [A]) ⊆ {w} (A −→ B) ∨ (A −→ ¬B)
|f (w, [A])| ≤ 1 (A −→ B) ∧ (A −→ C) =⇒ (A ∧ C −→ B) f (w, [A]) ⊆ [B] =⇒ f (w, [A ∧ B]) ⊆ f (w, [A]) (A ∧ B −→ C) =⇒ ((A −→ B) =⇒ (A −→ C)) f (w, [A]) ⊆ [B] =⇒ f (w, [A]) ⊆ f (w, [A ∧ B]) (A −→ B) ∧ ¬(A −→ ¬C) =⇒ (A ∧ C −→ B) (f (w, [A]) ⊆ [B] and f (w, [A]) ∩ [C] 6= ∅) =⇒ f (w, [A ∧ C]) ⊆ [B] (A −→ B) ∧ (C −→ B) =⇒ (A ∨ C −→ B)
f (w, [A ∨ B]) ⊆ f (w, [A]) ∪ f (w, [B])
kso −→ tokM,g,w = T iff ktkM,g,t for all t ∈ W s.t. t ∈ f (w, [s]) where [so] := {u | ksokM,g,u = T } is the so-called proof set of s.
Like in the case of modal logics, where we distinguish between logics such as K, B, D, S4, S5, there are many different conditional logics, which differ regarding the particular axioms/conditions associated with the conditionality operator −→. These logics are based on the axioms ID, MP, CS, CEM, AC, RT, CV, CA; see Fig. 2.
Representation. Representation of HCL is straight-forward: The syntax is exactly the same as for ordinary HOL problems. We merely add a new implication -> which denotes the conditional implication whereas the included implication of THF, =>, still denotes material implication (for the sake of consistency). Also, we add the different new quantification symbols !=, !~, !+ and !- for the respective quantification semantics and denote by ! the default quantification semantics as chosen by the user. The following example presents a formula that is valid in MP but not in ID: Parameters. The global parameters quantification and constants are the same as for in HOML. We also allow per-symbol rigidity specification as done for HOML. We do not need the specification of modalities here, instead we only need to specify the logic (axiomatization) under consideration. In contrast to modal logic where there exist mostly standardized naming conventions for important logical systems, this is not as evident for conditional logic. However, the axiom names themselves seem standard enough, hence we can describe the logical system by enumerating the included axioms.
This is done by the parameter logic Sets the semantics for the conditional logic under consideration. More precisely, collects a list of axioms that is to be considered. If omitted, a base conditional logic with none additional axioms is assumed.
Valid values: All of the axiom names of Fig. 2.
In the following example the logical axioms ID, MP and CEM (cf. Fig 2) are assumed for the remainder of the conditional logic problem under consideration. tpi(1, set_logic, hcl([’quantification’ = ’cumulative’, ’constants’ = ’rigid’, ’logic’ = [’id’, ’mp’, ’cem’]])).
Analogous to HOML, the above representations could be extended to support multiconditional logics, i.e. indexed operators ->. We do not pursue this further here, since were are not aware yet of applications. 3.4
Classical logic is only mildly suited for handling undefinedness and partiality in an appropriate way. There are two related reasons: (i) terms denote, without exemptions (e.g. for undefined terms), entities in a non-empty domain of “existing” objects D, and (ii) the quantifiers range over this entire set D.
An elegant alternative to remedy these shortcomings is free logic [
Moreover, the domain E may be empty (this special case is called inclusive logic).
Unfortunately, no theorem provers have been available so far for free logic. Nevertheless,
free logic can be embedded in HOL [
T iff for all d ∈ E holds ksokM,g[d/Xτ ] = T (d
if {d ∈ E | ksokM,g[d/Xτ ] = T } is unitary ∗
otherwise Representation. Since the syntax is exactly the same as for HOL, we do not need any special representation for free logic formulas. Nevertheless, we need to specify if the domain E is empty or not.
This is simply stated by the parameter
→
f
u
t
f u t
t t t
u u t
f u t
→
f
u
t
f u t
t u t
u u u
f u t
→∗
f
u
t
f u t
t t t
t t t
f f t
(a) Strong-Kleene
(b) Weak-Kleene
(c) Bocvar
Classical logics are based on the bivalence principle, that is, the set of truth-values V has the
cardinality |V | = 2, usually denoted V = {T, F } for truth and falsity. Many-valued logics
generalize this requirement to more or less arbitrary sets of truth-values, rather referred
to as truth-degrees in that context. Popular examples of many-valued logics are Go¨del
logics, Lukasiewicz and fuzzy logics with (non-)denumerable sets of truth-degrees, and,
from the field of finitely-many valued logics, Kleene, Bocvar and Dunn/Belnap logic [
Many valued logics have applications in linguistics and philosophy (especially nonwestern philosophy) for arguing about vagueness, and in computer science for analyzing database and information systems.
Syntax and semantics. There is no single unique way for defining the semantics of quantification in many-valued logics. Hence, we are focusing, for the time being, on propositional many-valued logic. The grammar we are considering is formed by a, b ::= ti | c | ¬a | aCb.
Where the ti are the truth-values of the logic, c ∈ Σ is a constant symbol and C is a symbol of the set of binary connectives, containing at least {&, ∨, ∧, →}. Depending on the selected logic, additional symbols can be added, and the number of ti is fixed.
The semantics here is highly dependent on the chosen logic. As usual the semantics of the connectives can be given in a truth-table. In Fig. 3 the semantics of → for three different three-valued logics is given as an example.
Representation. Since we are only considering propositional many-valued logic at this point, it does not fit well into the quantified fragment of the TPTP. But since there exist quantified versions of many-valued logics, we base the propositional case on the FOF fragment of the TPTP. This way, the proposal can be extended towards a first-order version.
In addition to FOF, we first introduce a term for truth degrees #t(i) for ti with i = 1, . . . , n, where n is the number of truth constants for the selected logic. To distinguish between weak and strong conjunction, we introduce a new symbol /\ for the standard weak conjunction ∧. The standard AND-symbol & is defined to be the strong conjunction to avoid confusion.
The following is an example for axioms of a many-valued logic, relating ∧ and ∨ to the minimal signature of Lukasiewicz or Go¨del logics. mvf(1, axiom, (a /\ b) = ((a & (a -> b)))). mvf(2, axiom, (a | b) = ((a -> b) -> b) /\ ((b -> a) -> a)).
Global Parameters. There are two parameters we can provide to adjust the semantics. The first fixes the exact logic. As described, there are many possible many-valued logics, that fix an interpretation for the logical symbols. The second parameter sets the cardinality of the set of truth values. This parameter is only important for the logics with an adjustable amount of truth values. The exact parameters are: semantics Sets the exact logic and fixes the interpretation for the logical symbols.
Valid values: kleene-weak, kleene-strong, post, lukasiewicz, goedel, bocvar. card Sets the size of the truth values. Has only an effect on lukasiewicz and goedel.
Valid values: any natural number The parameters can be set as in the previous cases in the instruction language TPI. For example, a Lukasiewicz logic with {0, 14 , 24 , 43 , 1} as truth values can be declared with: tpi(1, set_logic, mvl([‘semantics‘ = ‘lukasiewicz‘,
‘card‘ = 5])).
In theory the cardinality cases ℵ0 and ℵ1 were possible, but this would require a different mechanism to name truth values. 3.5.1
MVL based on SIXTEEN
There are several sixteen-valued logics based on a lattice denoted SIXTEEN. These logical
systems have been developed by Shramko and Wansing as a generalization of the
fourvalued system of Dunn/Belnap [
V = 2{N,T,F,B} = {∅, N, T, F, B, . . . , {N, T, F, B}}
where N, T, F and B are the respective singleton sets containing N, T, F and B. The
remaining truth-degrees are named using a combination of the letters N, T, F and B,
representing the truth-degree that contains the respective elements when regarded as a
set (e.g. NT for the set {N, T}). This generalization is essentially motivated by the
observation that a four-valued system cannot express certain phenomena that arise in
knowledge bases in computer networks. Further applications in linguistics and philosophy
are discussed in the monograph by Shramko and Wansing [
where a, b are ad-hoc introduced individuals symbols as supported by FOF.
In this paper, we discussed means of representing both problems and meta-logical
specification for quantified non-classical logics. To that end we adapt and extend TPTP-THF
and QMLTP syntax for problems and the TPI language proposal for fixing semantic
parameters. We have outlined specialized syntaxes for higher-order modal logic, hybrid logic,
conditional logic, and free logic to be used as input languages of ATP systems.
Additionally, we sketched ideas for representing many-valued logics. Further logics can easily be
added and addressed along the same lines. For example, due to space restrictions we have
omitted the inclusion of (quantified) intuitionistic logic [
The suggestions in this paper are, at this stage, not meant to be conclusive. Instead, we want to stimulate discussions, e.g. at the ARQNL event, about further requirements and extensions. Moreover, we envision a close collaboration with the QMLTP and TPTP projects.
A concluding, motivating example is displayed in Appendix A where an encoding of Go¨del’s Ontological argument is given in hmf syntax.
Acknowledgments: We thank Harold Boley for his comments and for proofreading this document. We also thank the reviewers for the very valuable feedback they provided. A
The following example is an encoding of Go¨del’s ontological argument in hmf syntax as
described in this work (cf. §3.1). More precisely, we present here Dana Scott’s variant as a
one step proof in which intermediate argumentation steps are omitted. HOL provers such
as Leo-II are capable of automating this example in a few seconds (however, not yet for
the syntax representation below). Details about the ontological argument, its formalization
and its automation can be found in the literature (e.g. in [