The higher-order ATP system Leo-III is demonstrated. Leo-III supports flexible and effective reasoning in every common semantical variation of normal modal logics. Many powerful automated and interactive theorem proving systems for first-order and higher-order logics have been developed over the past decades. However, with a few notable exceptions, most available systems focus on classical logics only. In particular for quantified non-classical logics only a small number of implemented systems is available to date. This is in contrast to an increasing number of challenging and interesting applications for such systems in artificial intelligence, computer science, mathematics and philosophy [10, 8, 9, 5, 6, 7]. Metaphysics, for example, is an area where higher-order modal logics (HOMLs) play an important role. The development of ATPs for HOMLs, however, is still in its infancy. The Leo-III prover, which is presented here, is addressing this gap. Leo-III [4] is in the first place an automated theorem prover for classical higher-order logic (HOL) with Henkin semantics and choice [1]. Despite its primary focus on HOL, Leo-III comes with effective means for reasoning in HOMLs. In fact, reasoning in every normal modal logic variant is supported in Leo-III. To achieve this, the prover internally implements a shallow semantical embedding approach [2, 3]. The key idea of this approach is to provide and exploit faithful mappings for HOML input problems to HOL. This is orthogonal to the direct implementation of specialised theorem provers, which usually focus on a small subset of modal logic systems only. The semantical embedding approach realised in Leo-III, in contrast, allows for a quick adaptation to a broad variety of expressive, non-classical logics. Leo-III in particular supports (but is not limited to) first-order and higher-order extensions of the well known modal logic cube for different concrete choices of Quantification semantics, including cumulative, decreasing, constant and varying domains, Rigidity, including rigid and world-dependent constant symbols, and Consequence, including the usual notions of local and global consequence.
Automation of HOML. In order to automate reasoning in HOMLs, Leo-III exploits the semantical embedding approach and internally translates modal logic problems into equivalent problems formulated within classical higher-order logic. To that end, the de-facto standard TPTP THF input syntax is augmented to include the modal connectives. Fig. 1 displays an example modal logic formula that is an instance of a corollary of Becker’s postulate, with $box and $dia representing the (mono-)modal operators 2 and 3, respectively, and the usual TPTP text representatives of the remaining logical connectives. This example formula is valid in S5 but not in any weaker system.
The logic specification format displayed in the example from Fig. 1 is stemming from an ongoing TPTP language extension proposal.1 In this logic specification, the identifiers $constants, $quantification and $consequence specify the exact semantical settings for the rigidity of constant symbols, the quantification semantics and the consequence relation, respectively. Finally, $modalities specify the properties of the modal connectives. Valid values are either pre-defined identifiers representing the usual modal logic systems, as in $modalities := $modal_system_S5 for the specification of an S5 modal logic, or lists of individual modal axiom schemes, as in $modalities := [$modal_axiom_K, $modal_axiom_B].
The reasoning process of Leo-III proceeds as follows: 1. The user inputs a HOML problem in the adapted TPTP syntax from above (Fig. 1). 2. Leo-III analyses the logic specification contained within the input and automatically selects the definitions and axioms to be added to the embedded problem representation. 3. The problem statement itself is translated into its embedded equivalent using the definitions from the previous step. 4. Finally, Leo-III starts reasoning in (meta-logic) HOL and returns SZS compliant result information and, if successful, also a proof object just as for standard HOL problems. Summary. At the ARQNL 2018 event we will demonstrate Leo-III, which, in terms of supported logics, is the most widely applicable automated theorem prover available to date. The embedding procedure is also available as stand-alone implementation at github.com/leoprover and can be used in conjunction with every THF-compliant ATP.
1 See http://www.cs.miami.edu/~tptp/TPTP/Proposals/LogicSpecification.html for more details. A
Installation and Usage of Leo-III
Leo-III is freely available on GitHub (https://github.com/leoprover/Leo-III) under BSD3 license. The most current release (version 1.2) is accessible under https://github.com/ leoprover/Leo-III/releases/latest. To get it, simply download the source archive and extract it so some location. > wget https://github.com/leoprover/Leo-III/archive/v1.2.tar.gz > tar -xvzf v1.2.tar.gz After extraction, Leo-III can be built using Make. Simply cd to the extracted directory and run make: > cd Leo-III-1.2/ > make > make install
> leo3 becker.p -p After building, there should be a directory bin/, relative from the current directory. This directory contains the binary leo3 of Leo-III.
Leo-III can optionally be installed by invoking which copies the binary to the directory $HOME/bin by default.
Leo-III is invoked via command-line (assuming the leo3 executable is in $PATH):
For the example of Becker’s postulate of Fig. 1, running
will invoke Leo-III for proving this conjecture (the -p option enables the output of a proof
certificate). This will produce the following result:
thf(mforall_const__o__d_i_t__o_mworld_t__d_o_c__c__def, definition, (
mforall_const__o__d_i_t__o_mworld_t__d_o_c__c_ = (^ [A:(($i > (mworld > $o)) > (mworld > $o)),B:mworld]:
! [C:($i > (mworld > $o))]: (A @ C @ B)))).
thf(mforall_const__o__d_i_c__type, type, mforall_const__o__d_i_c_: (($i > (mworld > $o)) > (mworld > $o))).
thf(mforall_const__o__d_i_c__def, definition, (mforall_const__o__d_i_c_ = (^ [A:($i > (mworld > $o)),B:mworld
]: ! [C:$i]: (A @ C @ B)))).
thf(mforall_const__o__d_i_t__d_i_c__type, type, mforall_const__o__d_i_t__d_i_c_: ((($i > $i) > (mworld > $o))
> (mworld > $o))).
thf(mforall_const__o__d_i_t__d_i_c__def, definition, (mforall_const__o__d_i_t__d_i_c_ = (^ [A:(($i > $i) > (
mworld > $o)),B:mworld]: ! [C:($i > $i)]: (A @ C @ B)))).
thf(sk1_type, type, sk1: mworld).
thf(sk2_type, type, sk2: ($i > (mworld > $o))).
thf(sk3_type, type, sk3: ($i > $i)).
thf(sk4_type, type, sk4: $i).
thf(sk5_type, type, sk5: mworld).
thf(sk6_type, type, sk6: (($i > $i) > mworld)).
thf(1,conjecture,((mvalid @ (mforall_const__o__d_i_t__o_mworld_t__d_o_c__c_ @ (^ [A:($i > (mworld > $o))]: (
mforall_const__o__d_i_t__d_i_c_ @ (^ [B:($i > $i)]: (mforall_const__o__d_i_c_ @ (^ [C:$i]: (
mexists_const__o__d_i_t__d_i_c_ @ (^ [D:($i > $i)]: (mimplies @ (mdia @ (mbox @ (A @ (B @ C)))) @ (mbox
@ (A @ (D @ C)))))))))))))),file(’becker.p’,1)).
thf(2,negated_conjecture,((~ (mvalid @ (mforall_const__o__d_i_t__o_mworld_t__d_o_c__c_ @ (^ [A:($i > (mworld
> $o))]: (mforall_const__o__d_i_t__d_i_c_ @ (^ [B:($i > $i)]: (mforall_const__o__d_i_c_ @ (^ [C:$i]: (
mexists_const__o__d_i_t__d_i_c_ @ (^ [D:($i > $i)]: (mimplies @ (mdia @ (mbox @ (A @ (B @ C)))) @ (mbox
@ (A @ (D @ C))))))))))))))),inference(neg_conjecture,[status(cth)],[
mworld: $tType )). % declare accessibility relations thf(mrel_type,type,(
mrel: mworld > mworld > $o )). % define accessibility relation properties thf(mreflexive_type,type,(
mreflexive: ( mworld > mworld > $o ) > $o )). thf(mreflexive_def,definition, ( mreflexive = ( ^ [R: mworld > mworld > $o] : ! [A: mworld] :
( R @ A @ A ) ) )). thf(meuclidean_type,type,(
meuclidean: ( mworld > mworld > $o ) > $o )). % assign properties to accessibility relations thf(mrel_mreflexive,axiom,(
mreflexive @ mrel )). thf(mrel_meuclidean,axiom,(
meuclidean @ mrel )). % define valid operator thf(mvalid_type,type,(
mvalid: ( mworld > $o ) > $o )). thf(mvalid_def,definition, ( mvalid = ( ^ [S: mworld > $o] : ! [W: mworld] :
( S @ W ) ) )). % define nullary, unary and binary connectives which are no quantifiers thf(mimplies_type,type,(
mimplies: ( mworld > $o ) > ( mworld > $o ) > mworld > $o )). thf(mimplies,definition, ( mimplies = ( ^ [A: mworld > $o,B: mworld > $o,W: mworld] : ( ( A @ W ) => ( B @ W ) ) ) )). thf(mdia_type,type,(
mdia: ( mworld > $o ) > mworld > $o )). thf(mdia_def,definition, ( mdia = ( ^ [A: mworld > $o,W: mworld] : ? [V: mworld] : ( ( mrel @ W @ V ) & ( A @ V ) ) ) )). thf(mbox_type,type,(
mbox: ( mworld > $o ) > mworld > $o )). thf(mbox_def,definition, ( mbox = ( ^ [A: mworld > $o,W: mworld] : ! [V: mworld] : ( ( mrel @ W @ V ) => ( A @ V ) ) ) )). % define exists quantifiers thf(mexists_const_type__o__d_i_t__d_i_c_,type,(
mexists_const__o__d_i_t__d_i_c_: ( ( $i > $i ) > mworld > $o ) > mworld > $o )). thf(mexists_const__o__d_i_t__d_i_c_,definition, ( mexists_const__o__d_i_t__d_i_c_ = ( ^ [A: ( $i > $i ) > mworld > $o,W: mworld] : ? [X: $i > $i] :
( A @ X @ W ) ) )). % define for all quantifiers thf(mforall_const_type__o__d_i_t__o_mworld_t__d_o_c__c_,type,(
mforall_const__o__d_i_t__o_mworld_t__d_o_c__c_: ( ( $i > mworld > $o ) > mworld > $o ) > mworld > $o )). thf(mforall_const__o__d_i_t__o_mworld_t__d_o_c__c_,definition, ( mforall_const__o__d_i_t__o_mworld_t__d_o_c__c_ = ( ^ [A: ( $i > mworld > $o ) > mworld > $o,W: mworld] : ! [X: $i > mworld > $o] :
( A @ X @ W ) ) )). thf(mforall_const_type__o__d_i_c_,type,(
mforall_const__o__d_i_c_: ( $i > mworld > $o ) > mworld > $o )). thf(mforall_const__o__d_i_c_,definition, ( mforall_const__o__d_i_c_ = ( ^ [A: $i > mworld > $o,W: mworld] : ! [X: $i] :
( A @ X @ W ) ) )). thf(mforall_const_type__o__d_i_t__d_i_c_,type,(
mforall_const__o__d_i_t__d_i_c_: ( ( $i > $i ) > mworld > $o ) > mworld > $o )). thf(mforall_const__o__d_i_t__d_i_c_,definition, ( mforall_const__o__d_i_t__d_i_c_ = ( ^ [A: ( $i > $i ) > mworld > $o,W: mworld] : ! [X: $i > $i] :
( A @ X @ W ) ) )).