TPTP And Beyond: Representation of Quantified Non-Classical Logics∗ Max Wisniewski1 , Alexander Steen1 , and Christoph Benzmüller21 1 Freie Universität Berlin, Institute of Computer Science {m.wisniewski,a.steen}@fu-berlin.de 2 Stanford University, CSLI c.benzmueller@gmail.com Abstract The practical employment of automated deduction systems requires the user to input problem statements in a well-formed string representation. While this presentation is usu- ally 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 excep- tion. To move standardization forward, we outline conservative extensions to the TPTP language that allow systematic syntax definitions for various expressive, non-classical log- ics. 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. 1 Introduction 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 pow- erful 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 [26] which automates first-order modal logic. Orthogonal to the development of specialized provers, the semantical embedding ap- proach [7] allows for a quick adaptation of existing higher-order reasoning systems to a broad variety of expressive, non-classical logics. In fact, for each logic discussed in this paper, we already have a new theorem provers in place [7, 5, 9, 8, 32]. These reasoners have been implemented by utilizing the embeddings approach on top of systems such as Leo-II [4] or Isabelle/HOL [22]. Recent experiments show that this approach indeed offers a surprisingly effective automation of the embedded non-classical logics. However, from the users perspective the utilization of the embeddings approach can become rather involved and distracting. Hence, system users may eventually not want to be exposed to the embed- dings at all. Moreover, a comprehensive evaluation of systems based on the embeddings approach against systems based on the direct approach is currently hardly feasible. One reason, in addition to the fact the very few systems in the direct approach are available to date, is the lack of commonly agreed input formats. In order to amplify the practical development, deployment and comparison of auto- mated reasoning in quantified non-classical logics, we therefore outline problem represen- tation formats for various (quantified) non-classical logics, primarily for use in automated ∗ This work has been supported by the DFG under grant BE 2501/11-1 (Leo-III) and grant BE 2501/9-2 (Computational Metaphysics). ARQNL 2016 51 CEUR-WS.org/Vol-1770 Representation of Quantified Non-Classical Logics Wisniewski, Steen and Benzmüller theorem proving (ATP) systems. More specifically, we present conservative extensions to the well-known TPTP [34] syntax representations. We display proposals on how to represent logical problems in quantified versions of multi-modal logics, hybrid logics, con- ditional logics, free logics and some propositional many-valued logics. Additionally, we include means of adding meta-logical information to the problem statement that specifies details regarding the assumed semantics of the respective problem and logic. We briefly introduce each of the mentioned logics and describe the necessary modifications of the already existing languages. TPTP and QMLTP. The Thousands of Problems for Theorem Provers problem li- brary (TPTP) [34] provides a coherent environment for testing automated theorem provers for their correctness and performance. To that end, it postulates a standardized and stable formula representation syntax for most classical logic languages (e.g. FOF for first-order formulas or THF [35] for typed higher-order formulas). We will base our problem repre- sentation format on the THF dialect and moderately extend the existing syntax definitions to match the requirements of the particular non-classical logic in question. A closely related project is QMLTP [27] which provides a syntax and a collection of problems for first-order modal logic. The QMLTP syntax is designed as an extension of the TPTP FOF language, introducing special symbols for the box and the diamond operators of modal logic (cf. §3.1). Regarding modal logics (or logics based on modal logic), we will also re-use existing syntax representations of the QMLTP project. Moreover, we adopt and extend the QMLTP approach for the specification of meta-logical information. 2 Classical Higher-Order Logic 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 for- mats will quite naturally be given as extensions of (classical) higher-order logic (HOL) [13]. The syntax and semantics of HOL is now briefly introduced as it serves as a basis for later, when logic-specific definitions of the syntax and semantics of non-classical higher-order logics are depicted. The brief introduction to HOL is mainly borrowed from [33] which, in turn, adapts the simplified notation of [21] for 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τ )ν S where cτ ∈ Στ is a constant symbol from the (typed) signature Σ := τ Στ 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 ∧ := λs .λt .¬(¬s ∨ ¬t). o o 2 52 Representation of Quantified Non-Classical Logics Wisniewski, Steen and Benzmüller thf(1, type, (p: ($i > $i) > $o)). thf(2, conjecture, (? [F: $i > $i]: (p @ F = p @ (^ [X: $i]: X)))). Figure 1: A small HOL problem in THF representation. 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 = I(cτ ) kXτ kM,g = g(Xτ ) ksτ →ν tτ kM,g = ks  τ →ν k M,g ktτ kM,g  kλXτ . sν kM,g = f : z 7−→ kskM,g[z/Xτ ] ∈ 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 kso kM,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 Gödel’s Incompleteness Theorem [17], HOL with standard semantics is necessarily incomplete. However, if we allow Dτ →ν to be a proper subset of DνDτ with the constraint that k.k remains total, a meaningful notion of completeness can be achieved [19]. We assume this so-called Henkin semantics in the following. A de-facto standard representation of HOL problems for automated theorem provers is given by the THF dialect [35] of the TPTP syntax [34]. This representation syntax is supported by most current HOL ATP, including Satallax [11], LEO-II [4], agsyHOL [20], Isabelle/HOL [22] and many others. A small example problem encoded in THF is displayed in Fig. 1. The circumflex ^ and the @ denote λ-abstraction and function application, respectively. Types can be stated explicitly (cf. first line of Fig. 1), where > denotes the function type constructor →. Most remaining operations are standard TPTP syntax as used in first-order syntax. We will use the THF dialect as a starting point for the development of specific repre- sentations of quantified non-classical logics in the following section. 3 Representation of Non-Classical Logics 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 Logics ”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 53 3 Representation of Quantified Non-Classical Logics Wisniewski, Steen and Benzmüller classical logic language and characterized by appropriate rules and axiomatizations. No- tions 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 in- terest for the interpretation of philosophical arguments, but have also become increasingly important to mathematics and computer science [18]. Syntax and semantics. We now briefly sketch the syntax and semantics of higher- order modal logics (HOML) [21] by augmenting the appropriate definitions of HOL as given in §2. We here assume a multi-modal logic, that is a modal logic consisting of multiple, different box operators i , i ∈ I (and corresponding diamond operators), for some index set I. The syntax definition is nearly identical to that of HOL. We merely add the box oper- ators 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 = W, {Ri }i∈I , {Dτ }τ ∈T , {Iw }w∈W 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 function k.kM,g,w for HOML models M, a variable assignment g and a world w ∈ W by ki so kM,g,w = T iff for all v ∈ W such that wRi v it holds that kso kM,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. [15]). Regarding the quantification constants Πτ , τ ∈ T , we might want to allow mixed-semantics quantification statements, i.e. formulas where multiple quantifications are contained, each possibly with different semantics.2 This can simply be done by adding different quantification constants for the respective different quantification semantics to the signature, yielding Σ = {. . . , Πτ,co , Πτ,va , Πτ,inc , Πτ,dec } for each type τ ∈ T for constant, varying, cumulative and decreasing domain quantification semantics, respectively. 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 [1], footnote 14. 4 54 Representation of Quantified Non-Classical Logics Wisniewski, Steen and Benzmüller Representation. We adopt the representation of QMLTP for representing the box and diamond operators, i.e. by writing #box for  and #dia for . Since we are in a multi-modal setting, we qualify these connectives with an appropriate identifier, called index: #box(i) for i and #dia(i) for i . The modal operators are then used similar to quantifiers in TPTP: #box(a): t represents the formula a to . The remaining syntax is standard THF. A short example (where a and b are identifiers from I) is given by: hmf(1, type, (p: $i > $o)). hmf(2, conjecture, ((#box(a): (! [X: $i]: p @ X)) => (#dia(b): (? [X: $i]: p @ X)))). The ! quantifier respects some quantification semantics that is chosen by the user. Addi- tionally, 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 impor- tant 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 the global case we have: S |= t iff ∀M, g.∀w.((ks1 kM,g,w = T and . . . and ksn kM,g,w = T ) implies ktkM,g,w = T ). In the local case we instead have S |= t iff ∀M, g.((∀w.ks1 kM,g,w = T and . . . and ∀w.ksn kM,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)]])). 3 A proposal for the TPI language can be found at http://www.cs.miami.edu/ tptp/TPTP/Proposals/ ~ TPILanguage.html. 55 5 Representation of Quantified Non-Classical Logics Wisniewski, Steen and Benzmüller Here, three different indexed modalities a, b and c are introduced with the given axioma- tizations 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 Logics Hybrid logic [10] is a general term for extensions of ordinary modal logics that introduce a new sort of atomic formulas – the so-called nominals. Nominals introduce one convenient feature to modal logic, that is referencing and arguing about worlds. In natural language it is a common construct to refer to a specific point in time or the knowledge of one particular person. Although modal logic is used to model these problem domains, it is not possible to reference to the underlying world structure. Hybrid logic allows to evaluate a formula in a specific world – with the satisfaction operator @ – and to bind the current world to a variable – with the shift operator ↓. 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 s, t ::= ...|no |@(no )so | ↓ so→o |... n ∈ N OM The semantics is build on the same model as ordinary modal logic.   M = W, {Ri }i∈I , {Dτ }τ ∈T , {Iw }w∈W The variable assignment g = (g i , g n ) is adorned with an extra variable assignment g n , that maps nominals to worlds. The assignment g i 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 = g n (n) ≡ w. n ∈ N OM n k@nϕkM,g,w = kϕkM,g,g (n) k ↓ ϕo→o kM,g,w = kϕnkM,g,w where n is free in ϕ and g n (n) = w 4 Higher-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 [36]. 6 56 Representation of Quantified Non-Classical Logics Wisniewski, Steen and Benzmüller 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 Conditional logics [24] have many applications including action planning, counter-factual reasoning, default reasoning, deontic reasoning, metaphysical modeling and reasoning about knowledge. A new operator for so-called conditionality, denoted −→, is added to the basic logical language which is not to be confused with material implication ( =⇒ ).5 First-order conditional logics have been studied in [14, 16] and extended (to include propo- sitional quantification) and embedded in HOL in [3]. We here consider a higher-order quantified version of conditional logic (HCL).6 Syntax and semantics. Terms of HCL are defined as ordinary HOL terms, ex- cept that we add a new constant symbol for conditionality to the signature, i.e. Σ = {. . . , −→o→o→o }. As for modal logics above, we may add quantifiers for different domain conditions. Monomodal logics are subsumed by HCL since 2so can be introduced as an abbreviation for ¬so −→ so . Syntactically, HCL can be seen as a generalization of HOML where the index of modality −→ is a formula of the same language. For instance, in (so −→ to ) −→ uo the subformula s −→ t is the index of the second occurrence of −→. 5 The literature on conditional logics often uses =⇒ for conditionality and −→ for material implication. Our choice here is pragmatically motivated, since the TPTP already reserves => for material implication. 6 The 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. 57 7 Representation of Quantified Non-Classical Logics Wisniewski, Steen and Benzmüller ID Axiom A −→ A Condition f (w, [A]) ⊆ [A] MP Axiom (A −→ B) =⇒ (A =⇒ B) Condition w ∈ [A] =⇒ w ∈ f (w, [A]) CS Axiom (A ∧ B) =⇒ (A −→ B) Condition w ∈ [A] =⇒ f (w, [A]) ⊆ {w} CEM Axiom (A −→ B) ∨ (A −→ ¬B) Condition |f (w, [A])| ≤ 1 AC Axiom (A −→ B) ∧ (A −→ C) =⇒ (A ∧ C −→ B) Condition f (w, [A]) ⊆ [B] =⇒ f (w, [A ∧ B]) ⊆ f (w, [A]) RT Axiom (A ∧ B −→ C) =⇒ ((A −→ B) =⇒ (A −→ C)) Condition f (w, [A]) ⊆ [B] =⇒ f (w, [A]) ⊆ f (w, [A ∧ B]) CV Axiom (A −→ B) ∧ ¬(A −→ ¬C) =⇒ (A ∧ C −→ B) Condition (f (w, [A]) ⊆ [B] and f (w, [A]) ∩ [C] 6= ∅) =⇒ f (w, [A ∧ C]) ⊆ [B] CA Axiom (A −→ B) ∧ (C −→ B) =⇒ (A ∨ C −→ B) Condition f (w, [A ∨ B]) ⊆ f (w, [A]) ∪ f (w, [B]) Figure 2: Conditional logic axioms and semantic conditions An adequate semantics is achieved by adapting selection function semantics [31, 12]. We modify the HOL model structure by adding possible worlds (similar to HOML) and a selection function f : W × 2W 7→ 2W , yielding a HCL model structure M = (W, f, {Dτ }τ ∈T , {Iw }w∈W ) where W is a set of worlds, {Dτ }τ ∈T is a frame and {Iw }w∈W a collection of interpretation functions. Together with a variable assignment g and a world w ∈ W we can then refine the valuation function k.kM,g,s (only the valuation of conditionality is shown, the remaining cases are straight-forward adaptions of the HOL case): kso −→ to kM,g,w = T iff ktkM,g,t for all t ∈ W s.t. t ∈ f (w, [s]) where [so ] := {u | kso kM,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: hcf(1, type, (f : $i > $o)). hcf(2, type, (g : $i > $o)). hcf(3, conjecture, (! [X: $i]: ((f @ X) -> (g @ X)) => ((f @ X) => (g @ X)))). 8 58 Representation of Quantified Non-Classical Logics Wisniewski, Steen and Benzmüller 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 multi- conditional logics, i.e. indexed operators ->. We do not pursue this further here, since were are not aware yet of applications. 3.4 Free Logics Classical logic is only mildly suited for handling undefinedness and partiality in an ap- propriate 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 [23, 28], which dis- tinguishes between a raw domain of possibly non-existing objects D and a particular sub- domain E of D, containing only the “existing” entities. Free variables range over D and quantified variables only over E. Each term denotes in D, but not necessarily in E. This is the case, for example, for improper definite descriptions which can now be mapped to a distinguished non-existing object, denoted ∗ ∈ D. 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 [8], allowing indirect automation via HOL ATP systems. Syntax and semantics. The syntax of free higher-order logic is the same as for ordinary HOL. The non-trivial semantics definitions concern universal quantification and definite description (denoted by ι). A model M in this context distinguishes (for all types τ ) between a raw domain Dτ and a set Eτ ⊆ Dτ of existing objects. A valuation function for these cases can be formulated as k∀Xτ .so kM,g = T iff for all d ∈ E holds kso kM,g[d/Xτ ] = T ( d if {d ∈ E | kso kM,g[d/Xτ ] = T } is unitary kιXτ .so kM,g = ∗ 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 59 9 Representation of Quantified Non-Classical Logics Wisniewski, Steen and Benzmüller → f u t → f u t →∗ f u t f t t t f t u t f t t t u u u t u u u u u t t t t f u t t f u t t f f t (a) Strong-Kleene (b) Weak-Kleene (c) Bocvar Figure 3: Three different three valued semantics for implication. E Decides whether domain E is allowed to become empty or not. Valid values: empty or non-empty. Default value: empty A free logic setting in which the domain E may become empty can be configured using tpi(1, set_logic, free(’E’ = ’non-empty’)). 3.5 Many-valued Logics 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 Gö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 [2]. The latter logics (Kleene, Bocvar) introduce a third value often denoted u for unknown and differ in the interpretation in the presence of the unknown value. The Dunn/Belnap logic introduces two additional values n, b – denoting none and both, respectively. Many valued logics have applications in linguistics and philosophy (especially non- western 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 10 60 Representation of Quantified Non-Classical Logics Wisniewski, Steen and Benzmüller 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 Gö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 seman- tics. 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, 41 , 24 , 34 , 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 four- valued system of Dunn/Belnap [2] to knowledge bases in computer networks [29] and was subsequently further investigated in various contexts (e.g. [25, 30]). In SIXTEEN, the truth-degrees are given by the power set of Belnap’s truth values, i.e. 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 [30], to which we refer to for a thorough investigation of SIXTEEN, the definitions of logical connectives and their se- mantics. Briefly speaking, there exists a set of connectives ∨? , ∧? , ¬? for two distinct logics L? with ? ∈ {t, f } and a logic given by their union, denoted Ltf . Additionally, multiple different entailment relations |=? for ? ∈ {t, f, tf } can be considered. An embedding of logics based on SIXTEEN into HOL for use in ATP systems is sketched in [32]. Representation. The representation of the L? is more involved as we need a non- quantified language with different infix operators denoting the different logical connectives. The following syntax representation could be seen as a generalization and restriction of 61 11 Representation of Quantified Non-Classical Logics Wisniewski, Steen and Benzmüller FOF, where we add new infix connectives but restrict the problem not to contain first- order ingredients (such as quantifiers). Consequently, we add infix operators &t, |t, ~t, =>t, &f, |f, ~f and =>f to the language. The problem statements are then straight-forward, an example is given by sxf(1, axiom, (a |t b)). sxf(2, axiom, (a |f b)). sxf(3, conjecture, (a =>t b)). where a, b are ad-hoc introduced individuals symbols as supported by FOF. 4 Conclusion In this paper, we discussed means of representing both problems and meta-logical speci- fication 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 pa- rameters. 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. Addition- ally, 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 [6]. 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 Gö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. References [1] C. A. Anderson. Some emendations of Gödel’s ontological proof. Faith and Philosophy, 7(3), 1990. [2] N. D. Belnap. A useful four-valued logic. In G. Epstein and J. M. Dunn, editors, Mod- ern Uses of Multiple-Valued Logic, pages 7–37. Reidel Publishing Company, Boston, 1977. [3] C. Benzmüller. Automating quantified conditional logics in HOL. In F. Rossi, editor, 23rd International Joint Conference on Artificial Intelligence (IJCAI-13), pages 746– 753, Beijing, China, 2013. [4] C. Benzmüller, L. C. Paulson, N. Sultana, and F. Theiß. The higher-order prover LEO-II. Journal of Automated Reasoning, 55(4):389–404, 2015. [5] C. Benzmüller and B. Woltzenlogel Paleo. The inconsistency in Gödel’s ontological argument: A success story for AI in metaphysics. In IJCAI 2016, 2016. [6] Christoph Benzmüller and Lawrence Paulson. Multimodal and intuitionistic logics in simple type theory. The Logic Journal of the IGPL, 18(6):881–892, 2010. [7] Christoph Benzmüller and Lawrence Paulson. Quantified multimodal logics in simple type theory. Logica Universalis (Special Issue on Multimodal Logics), 7(1):7–20, 2013. 12 62 Representation of Quantified Non-Classical Logics Wisniewski, Steen and Benzmüller [8] Christoph Benzmüller and Dana Scott. Automating free logic in Isabelle/HOL. In G.-M. Greuel, T. Koch, P. Paule, and A. Sommese, editors, Mathematical Software – ICMS 2016, 5th International Congress, Proceedings, volume 9725 of LNCS, Berlin, Germany, 2016. Springer. To appear. [9] Christoph Benzmüller and Bruno Woltzenlogel Paleo. Higher-order modal logics: Au- tomation and applications. In Adrian Paschke and Wolfgang Faber, editors, Reasoning Web 2015, number 9203 in LNCS, pages 32–74, Berlin, Germany, 2015. Springer. [10] P Blackburn. Representation, reasoning, and relational structures: a hybrid logic manifesto. Logic Journal of IGPL, 8(3):339–365, 2000. [11] C.E. Brown. Satallax: An automated higher-order prover. In B. Gramlich, D. Miller, and U. Sattler, editors, Proc. of IJCAR 2012, volume 7364 of LNAI, pages 111 – 117. Springer, 2012. [12] B.F. Chellas. Basic conditional logic. Journal of Philosophical Logic, 4(2):133–153, 1975. [13] A. Church. A formulation of the simple theory of types. Journal of Symbolic Logic, 5:56–68, 1940. [14] J.P. Delgrande. On first-order conditional logics. Artificial Intelligence, 105(1-2):105– 137, 1998. [15] M. Fitting and R.L. Mendelsohn. First-Order Modal Logic. Synthese Library Studies in Epistemology Logic, Methodology, and Philosophy of Science Volume 277. Springer, 1998. [16] N. Friedman, J.Y. Halpern, and D. Koller. First-order conditional logic for default reasoning revisited. ACM Transactions on Computational Logic, 1(2):175–207, 2000. [17] K. Gödel. Über formal unentscheidbare Sätze der Principia Mathematica und ver- wandter Systeme. Monatshefte für Mathematik und Physik, 38(1):173–198, 1931. [18] R. Goldblatt. Mathematical modal logic: a view of its evolution. Journal of Applied Logic, 1(5):309–392, 2003. [19] L. Henkin. Completeness in the theory of types. Journal Symbolic Logic, 15(2):81–91, 1950. [20] F. Lindblad. agsyHol website. https://github.com/frelindb/agsyHOL, 2012. [21] Reinhard Muskens. Higher order modal logic. Handbook of modal logic, 3, 2007. [22] T. Nipkow, L.C. Paulson, and M. Wenzel. Isabelle/HOL: A Proof Assistant for Higher- Order Logic. Number 2283 in LNCS. Springer, 2002. [23] J. Nolt. Free logic. In E. N. Zalta, editor, The Stanford Encyclopedia of Philosophy. Winter 2014 edition, 2014. [24] D. Nute. Topics in conditional logic. Reidel, Dordrecht, 1980. [25] S. P. Odintsov. On Axiomatizing Shramko-Wansing’s Logic. Studia Logica, 91(3):407– 428, 2009. [26] J. Otten. MleanCoP: A Connection Prover for First-Order Modal Logic. In S. Demri, D. Kapur, and C. Weidenbach, editors, Automated Reasoning: 7th International Joint Conference, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 19-22, 2014. Proceedings, pages 269–276, Cham, 2014. Springer. [27] T. Raths and J. Otten. The QMLTP Problem Library for First-Order Modal Logics. In B. Gramlich, D. Miller, and U. Sattler, editors, IJCAR 2012, volume 7364 of LNCS, pages 454–461. Springer, 2012. [28] D. Scott. Existence and description in formal logic. In R. Schoenman, editor, Bertrand Russell: Philosopher of the Century, pages 181–200. George Allen & Unwin, London, 1967. [29] Y. Shramko and H. Wansing. Some useful 16-valued logics: How a computer network 63 13 Representation of Quantified Non-Classical Logics Wisniewski, Steen and Benzmüller should think. Journal of Philosophical Logic, 34(2):pp. 121–153, 2005. [30] Y. Shramko and H. Wansing. Truth and Falsehood: An Inquiry into Generalized Logical Values. Trends in Logic. Springer Netherlands, 2011. [31] R.C. Stalnaker. A theory of conditionals. In Studies in Logical Theory, pages 98–112. Blackwell, 1968. [32] A. Steen and C. Benzmüller. Sweet SIXTEEN: Automation via Embedding into Classical Higher-Order Logic. In 7th International Conference Non-Classical Logic – Theory and Applications, Toruń, Poland, 2015. [33] A. Steen, M. Wisniewski, and C. Benzmüller. Agent-based HOL reasoning. In G.-M. Greuel, T. Koch, P. Paule, and A. Sommese, editors, The 5th International Congress on Mathematical Software (ICMS 2016), volume 9725 of LNCS, Berlin, Germany, 2016. Springer. To appear. [34] G. Sutcliffe. The TPTP problem library and associated infrastructure. J. Autom. Reasoning, 43(4):337–362, 2009. [35] G. Sutcliffe and C. Benzmüller. Automated reasoning in higher-order logic using the TPTP THF infrastructure. Journal of Formalized Reasoning, 3(1):1–27, 2010. [36] M. Wisniewski and A. Steen. Embedding of Quantified Higher-Order Nominal Modal Logic into Classical Higher-Order Logic. In C. Benzmüller and J. Otten, editors, 1st International Workshop on Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2014) Vienna, Austria, Proceedings, volume 33 of EasyChair Proceedings in Computing, pages 59–64. EasyChair, 2014. 14 64 Representation of Quantified Non-Classical Logics Wisniewski, Steen and Benzmüller A Example: Gödel’s ontological argument The following example is an encoding of Gö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 [5]). tpi(1,set_logic,modal([’quantification’ = ’varying’, ’constants’ = ’rigid’, ’consequence’ = ’global’ ’modalities’ = [(a, s5)]])). hmf(positive_const,type,(p: ($i>$o)>$o)). hmf(A1,axiom,(![Phi: $i>$o]: ((p @ (^[X:$i]: ~(Phi @ X)) <=> ~(P @ Phi))))). hmf(A2,axiom,(![Phi: $i>$o,Psi: $i>$o]: (((p @ Phi) & #box(a): (![X:$i]: ((Phi @ X) => (Psi @ X)))) => (p @ Psi)))). hmf(god_const,type,(g: $i>$o)). hmf(god,definition,(g = (^[X:$i]: (![Phi: $i>$o]: ((p @ Phi) => (Phi @ X)))))). hmf(A3,axiom,(p @ g)). hmf(A4,axiom,(![Phi: $i>$o]: ((p @ Phi) => #box(a): (p @ Phi)))). hmf(essence_const,type,(ess: ($i>$o)>$i>$o)). hmf(essence,definition,(ess = (^[Phi: $i>$o,X: $i]: ((Phi @ X) & (![Psi: $i>$o]: ((Psi @ X) => #box(a): (![Y:$i]: ((Phi @ Y) => (Psi @ Y))))))))). hmf(necessary_existence_const,type,(ne: $i>$o)). hmf(necessary_existence,definition,(ne = (^[X:i]: (![Phi: $i>$o]: ((ess @ Phi @ X) => #box(a): (?[Y:$i]: (Phi @ Y))))))). hmf(A5,axiom,(p @ ne)). hmf(T3,conjecture,(#box(a): (?[X:$i]: (g @ X)))). 65 15