We present automated theorem provers implementing systems for intermediate logics, in the propositional and first-order setting. They use an axiomatic embedding into intuitionistic logic based on cut-restricted sequent calculi. All provers are evaluated on a large benchmark set of propositional and first-order formulas. Intermediate logics lie between intuitionistic logic and classical logic in terms of subset inclusion, in the propositional or first-order setting. Intermediate logics offer a more nuanced approach to the usual 2-valued classical logic and this motivates their study in logic, computer science, and artificial intelligence. While many theorem provers exist for classical logic and several for intuitionistic logic, only very few are available for intermediate logics. Our aim is to address this gap by presenting provers for intermediate logic-propositional and first-order-in a systematic manner. On the proof-theoretic side, it is well known that most propositional intermediate logics lack a cut-free sequent calculus. This is a formidable obstacle for automated theorem proving, and meta-theoretic investigations, since cut-freeness is the typical route towards a proof calculus with the subformula property, and the latter property is crucial for pruning in backward proof search. Indeed, recall the situation that arises with a Hilbert proof calculus where it is unclear when and on what formula the rule of modus ponens needs to be applied backwards. Ciabattoni et al. [1] present a general solution via cut-free hypersequent calculi for extensions of intuitionistic propositional logic (IPL) with axioms up to P 3′ in the substructural hierarchy. Although the hypersequent calculus is a natural generalisation of the sequent calculus (use a multiset of sequents instead of a single sequent), from the perspective of automated theorem proving it is much more complex to implement, and the hypersequent calculus formalism is much less well-known outside the structural proof theory community. A new solution is proposed by Ciabattoni et al. [2, 3]: sound and complete sequent calculi for propositional intermediate (and substructural) logics by permitting restricted cuts (as mentioned above, without a restriction on the cuts, the backward proof search space is simply too large). Specifically, the cut-formulas are restricted to instantiations of the axioms with conjunctions of subformulas of the end sequent. In the case of intermediate logics, the restricted cuts can be traded for a cut-free proof in the intuitionistic calculus with axiom instances added to the antecedent, making use of the deduction theorem in the latter. Consequently, the intermediate logics embed into intuitionistic logic. Our focus is on the implementations of the theory described above, and also for first-order intermediate logics that are obtained through the addition of quantification rules. After describing the theoretical foundation in Section 2, we present our implementations in Section 3 and evaluate them in Section 4. We conclude with a summary, outlook and related research in Section 5.
Propositional formulas are defined inductively from propositional atoms p, q, . . . and constants ⊥ and ⊤ using the connectives ∧, ∨, →, and ¬. In the first-order setting, the propositional atoms are replaced by predicates on terms built from variables and function symbols, and the language is extended with first-order quantifiers. A term is a variable or f (t1, . . . , tn) for a n-ary function symbol f and terms t1, . . . , tn. First-order formulas are defined inductively as the constants ⊥ and ⊤, P (t1, . . . , tn) for an n-ary predicate symbol P and terms t1, . . . , tn, and A ∧ B, A ∨ B, A → B, ¬A, ∀x.A and ∃x.A for formulas A and B. Free variables in a formula are those not in the scope of a quantifier. Also, A(t/x) denotes the formula obtained by uniformly substituting the term t for all occurrences of the variable x that are free.
Throughout, we identify a logic with the set of its theorems. An axiomatic extension L + A is obtained by extending the base logic L with every instantiation of the atomic formulas of the axiom schema A by arbitrary formulas, and closing under the axioms and rules of the proof calculus.
The Hilbert proof calculus consists of axioms and rules that directly manipulate the logical formulas. There are many equivalent variants for IPL e.g., [4, Section 6]. A Hilbert calculus for first-order intuitionistic logic (IL) is obtained by adding the following to IPL. Here x is not a free variable in C.
C → A(y/x)
C → ∀x.A
A(y/x) → C ∃x.A → C ∀x.A → A(t/x)
A(t/x) → ∃x.A
For economy of notation, we use IPL to denote the set of theorems of intuitionistic propositional logic and also its Hilbert proof calculus, and similarly for intuitionistic first-order logic IL.
A sequent calculus is a type of proof calculus that manipulates sequents of the form A1, . . . , Am ⇒ Am+1 . . . , Am+n where A1, . . . , Am+n are formulas. The intended interpretation of a sequent is the formula A1 ∧ . . . ∧ Am → Am+1 ∨ . . . ∨ Am+n. When required, ⊤ and ⊥ serve as the identity element for conjunction and disjunction respectively. A sequent (calculus) is single-succedent if at most a single formula is permitted on the right-hand side of the sequent, i.e. n ∈ {0, 1}, else it is multi-succedent. Roughly speaking, the meta-level implication and conjunction/disjunction provided by ⇒ and comma permit reasoning inside the formula (fixed depth deep inference), and this is what enables the definition of inference rules with nice properties that aid automated theorem proving and meta-theoretic investigations.
The theoretical foundations can be described using any reasonable cut-free sequent calculus for
intuitionistic logic. For the sake of concreteness, we use the well-known sequent calculus LJ presented
by Gentzen [
In this work, we consider the propositional axiomatic extensions of IPL listed further below.
The soundness and completeness with respect to sequent calculi with restricted cuts was established
in [
While the above axiom schema for Gödel logic is the standard one, we will actually use the
equivalent axiomatisation IPL + (A → B) ∨ ((A → B) → A) + ¬A ∨ ¬¬A. As observed in
[
First-order axiom schemas. In the first-order setting, the above axiom schemas are written as universal sentences. For example, ∀x¯(¬A ∨ ¬¬A) and ∀x¯((A → B) ∨ (B → A)).
Let FLJJ and FLJG denote first-order the sequent calculi obtained from LJJ and LJG by adding the usual Gentzen first-order quantifiers. Here, the eigenvariable y must not occur in the conclusion of the (R∀) and (L∃) rules.
A(t/x), Γ ⇒ C ∀xA, Γ ⇒ C (L∀) Γ ⇒ A(y/x) Γ ⇒ ∀xA (R∀)
A(y/x), Γ ⇒ C ∃xA, Γ ⇒ C (L∃) Γ ⇒ A(t/x) Γ ⇒ ∃xA (R∃)
We observe that FLJJ and FLJG are sound and complete for the corresponding cut-free hypersequent
calculi HLJJ and HLJG by a straightforward extension of the argument in [
It still remains to clarify the relationship between the first-order hypersequent calculus and the Hilbert calculus1. Consider the following Hilbert calculus rule with the condition that x is not free in C. ∀x(C ∨ A(y/x))
C ∨ ∀xA (QSR)
Armed with this rule, for each rule in the hypersequent calculus, there is a derivation in the Hilbert calculus of the conclusion from the premises under the standard formula translation. It follows that FLJJ is sound for IL + ∀x¯(¬A ∨ ¬¬A) + (QSR). Completeness is immediate since HLJJ has cut-elimination. Similarly, FLJG is sound and complete for IL + ∀x¯(A → B ∨ B → A) + (QSR).
In certain cases, the (QSR) rule may be replaced by an axiom schema. For example, it is easy to see that IL+∀x¯(A → B ∨B → A)+(QSR) is equivalent to IL+∀x¯(A → B ∨B → A)+∀z¯∀x(C ∨A(y/x)) → ∀z¯(C ∨ ∀x¯A) where x is not free in C in the latter axiom.
We have already noted that the sequent calculi obtained in [
F 7→ {A | A ∈ ψ(A, F )}
Ciabattoni et al. [
• The set-bounding function ψs(A, F ) contains all instances of formulas in A whose atomic formulas are substituted by non-repeating conjunctions of subformulas of F . • The formula-bounding function ψf (A, F ) contains all instances of formulas in A whose atomic formulas have been substituted by subformulas of F . • The variable-bounding function ψv(A, F ) contains all instances of formulas in A whose atomic formulas have been substituted by atoms in F .
We have omitted the multiset-bounding function, as it is not relevant for intermediate logics. Observe that the set-bounding function has as image a set whose size is exponential in the size of F .
Notice that ψv(A, F ) ⊂ ψf (A, F ) ⊂ ψs(A, F ) for any F containing two distinct subformulas. In
certain cases including Jankov logic and Gödel logic, it is possible to identify an axiomatisation that
supports the preferred variable-bounding function. As Ciabattoni et al. [
The set of axiom instances (and hence cut formulas) that are required in a proof of F in Jankov logic and Gödel logic are explicitly described below. It is precisely this variable-bounding function that we implement in the embedding-preprocessing step of the provers.
{¬A ∨ ¬¬A | A 7→ atoms in F } {(A → B) ∨ ((A → B) → A) | A, B 7→ atoms in F } ∪ {¬A ∨ ¬¬A | A 7→ atoms in F } From Restricted Cuts to Embedding into Intuitionistic Logic Observe that a proof of ⇒ F in the intuitionistic calculus with cuts from a finite set Ω (in the present setting, this represents the image of the bounding function) can be transformed to a proof of ∧Ω ⇒ F ; simply replace each left premise Γ ⇒ A of a cut instance (A ∈ Ω) with the trivial proof in LJ, where (L∧)* denotes multiple applications of the left conjunction rule.
∧AΩ,,ΓΓ⇒⇒AA (L∧)*
Now proceed downwards, applying the obvious weakenings and contractions as required; the end
sequent is then transformed to ∧Ω ⇒ F . By cut-elimination in the intuitionistic calculus, we obtain
a cut-free proof of the latter sequent that witnesses an embedding of the intermediate logic into
intuitionistic logic. What this means is that the prover can now conduct backward proof search in the
setting of a cut-free intuitionistic proof of ∧Ω ⇒ F . This is the embedding perspective [
We remark that the number of subformulas of F is bounded by the size |F | of F , and the number of atomic formulas in each of the Gödel axioms listed above is ≤ 2, and the Jankov axiom has just a single atomic formula. Hence the set-bounding function yields an exponential embedding of Gödel logic into intuitionistic logic, and the variable-bounding function that we actually implement in the prover yields a linear and quadratic embedding of Jankov and Gödel logic, respectively.
SuperJ is an automated theorem prover written in Haskell that supports many intermediate propositional logics via an embedding-preprocessing step followed by intuitionistic proof search.
A, Γ ⇒ B Γ ⇒ Δ, A → B (R→)
A, B, Γ ⇒ Δ A, A → B, Γ ⇒ Δ (mp)
A → (B → C), Γ ⇒ Δ (A ∧ B) → C, Γ ⇒ Δ (L→∧) A → p, B → p, p → C, Γ ⇒ Δ
(A ∨ B) → C, Γ ⇒ Δ A, p → C, B → p, Γ ⇒ p C, Γ ⇒ Δ (A → B) → C, Γ ⇒ Δ (L→∨) fresh atomic p (L→→) fresh atomic p
SuperJ automatically selects one of the three bounding functions mentioned earlier based on the propagation properties in the embedding step. Besides supporting arbitrary axiomatisations, the prover explicitly supports Classical Propositional Logic (CPL), IPL, Jankov logic and Gödel logic. For IPL the embedding step is omitted, and for CPL the prover immediately switches to classical proof search. The two intermediate logics are supported through the variable-bounded axiomatisations as noted in the previous section.
The intuitionistic proof search procedure of SuperJ is based on that of Avellone et al. [
The most important optimization follows from the addition of boolean simplification and replacement
rules [
When possible, SuperJ reverts to classical proof search through the sequent calculi LK* [12] for classical logic. This happens whenever the succedent of the sequent is empty. Furthermore, the classical provability of the sequent is checked before attempting to apply a left non-invertible left rule, which allows pruning of the search space when false. Finally, for non-invertible right rules, backtracking can be avoided in the case of a singleton succedent.
The theorem prover ileanSeP-im is an axiomatic extension of the intuitionistic sequent prover ileanSeP for Jankov and Gödel first-order logics. ileanSeP is a compact Prolog implementation of the singlesuccedent intuitionistic sequent calculus. Similar to tableau calculi, it uses a bottom-up proof search, free variables and a dynamic skolemization to deal with quantifiers. Together with the occurs check of term unification, this ensures that the eigenvariable condition is respected.
The theorem prover ileanTAP-im is an axiomatic extension of the intuitionistic tableau prover ileanTAP for Jankov and Gödel first-order logics. ileanTAP [13] is a compact Prolog implementation of a prefixed tableau calculus, similar to Fitting [14]. It extends the classical calculus [15] by adding prefixes to capture the Kripke semantics of intuitionistic logic, uses free prefix variables [16] and extends skolemization to prefix constants. First, ileanTAP-im performs a classical proof search collecting prefixes of literals that close branches. If this search succeeds, a prefix unification is used to unify these prefixes. A0 : p {{A0 : pa∗}} (G ∧ H)1 : p {{M (G1 : p)}}, {{M (H1 : p)}} (G ∨ H)0 : p {{M (G0 : p)}}, {{M (H0 : p)}} (G → H)0:p {{M (G1 : pa∗)}}, {{M (H0 : pa∗)}} (G ∧ H)0 : p {{M (G0 : p), M (H0 : p)}} (G ∨ H)1 : p {{M (G1 : p), M (H1 : p)}} (G → H)1:p {{M (G0 : pV ∗), M (H1 : pV ∗)}}
type atomic α γ δ
F pol : p A1 : p (¬G)0 : p (¬G)1 : p (∀xG)1 : p (∃xG)0 : p (∀xG)0 : p (∃xG)1 : p
M (F pol : p) {{A1 : pV ∗}} M (G1 : pa∗) M (G0 : pV ∗) M (G[x\x∗]1 : pV ∗) M (G[x\x∗]0 : p) M (G[x\t∗]0 : pa∗) M (G[x\t∗]1 : p) The automated theorem prover nanoCoP-im is an axiomatic extension of the intuitionisitic non-clausal connection prover nanoCoP-i for the Jankov and Gödel first-order logics. nanoCoP-i is a compact Prolog implementation of the non-clausal connection calculus for first-order intuitionistic logic (with equality) [17, 18] and an extension of the classical prover nanoCoP [19, 20]. It is based on a prefixed non-clausal connection calculus [17]. In contrast to sequent and tableau calculi, which are connectivedriven, connection calculi use a connection-driven search strategy. A connection is a set {A10, A21} of literals with the same predicate symbol but different polarities.
The non-clausal connection calculus works on non-clausal matrices, where a matrix M is a set of clauses and a clause C is a set of literals L and (sub)matrices. It represents a formula in negation normal form. A prefix is a string consisting of variables (V ) and constants (a) and assigned to each literal.
For a formula F , polarity pol ∈ {0, 1} and prefix p, the intuitionistic non-clausal matrix M (F pol) of F pol is defined inductively according to Table 1. x* is a new term variable, t* is the Skolem term f * (x1, . . . , xn), V * is a new prefix variable, a* is the prefix constant of the form f * (x1, . . . , xn), f * is a new function symbol and x1, . . . , xn are all free term and prefix variables in the corresponding formula F pol : p. The intuitionistic non-clausal matrix M i(F ) of F is the matrix M (F 0 : ε). A term substitution σT assigns terms to variables, a prefix substitution σP assigns strings to prefix variables (and is calculated by a prefix unification). For intuitionistic logic, a connection {A10 : p1, A21 : p2} is σ-complementary iff σT (A1) = σT (A2) and σP (p1) = σP (p2) for a combined substitution σ = (σT , σP ).
The non-clausal connection calculus for intuitionistic logic [17] is given in Figure 2. An intuitionistic connection proof for F is a derivation of ε, M i(F ), ε. Compared to the formal clausal connection calculus [21, 22], the extension rule is generalized and a decomposition rule is added [23, 19].
First, nanoCoP-im performs a classical proof search, in which the prefixes of each connection are collected. If the search succeeds the prefixes of the literals in each connection are unified. Additional optimization techniques are regularity, lemmata, restricted backtracking and strategy scheduling [24, 18].
Axiom (A) Reduction (R) Extension (E) {}, M, Path
C, M, Path∪{L2: p2} C∪{L1 : p1}, M, Path∪{L2 : p2} C3, M [C1\C2], Path∪{L1 : p1}
C, M, Path C∪{L1: p1}, M, Path
C2, M, {} ε, M, ε Start (S)
and C2 is copy of C1∈M and {L1:p1, L2:p2} is σ-complementary
C3:=β-clauseL2 (C2), C2 is copy of C1, C1 is e-clause of M wrt. Path ∪ {L1 : p1}, C2 contains L2 : p2, {L1:p1, L2:p2} is σcomplementary Decomposition (D)
C ∪ C1, M, Path C∪{M1}, M, Path
and C1∈M1
At present, sets of formulas for testing automated theorem provers for intermediate logic are not available. As the syntax of intermediate logic is the same as classical and intuitionistic logic, we can use existing benchmark formulas of these logics. As intermediate logics are an extension of intuitionistic logic, we decided to use the ILTP problem library for intuitionistic logic [25].
Version 1.1.2 of the ILTP problem library contains 274 propositional and 2550 first-order formulas with status and difficulty rating information. The problems are in TPTP syntax and divided into 24 categories. While the propositional formulas belong mainly to the intuitionistic syntactic category (SYJ), the firstorder formulas are taken from a wide range of domains, from general algebra (ALG), computing (COM), set (SET) and number (NUM) theory to software creation (SWC) and verification (SWV).
The SuperJ prover described in Section 3 was evaluated on all 274 propositional problems of the ILTP library v1.1.2. The test were conducted on a 3.6 GHz Ryzen system with 32 GB of RAM running Ubuntu 23.10 with kernel version 5.15. Running time was restricted to 60 seconds of CPU time per individual problem. Table 2 shows the number of problems solved within the time limit, and the required time in seconds, best results for each logic are marked bold.
Performance results of intuitRIL have also been collected for comparison. This intermediate propositional logic prover, due to Fiorentini and Ferrari [26], is the only automated theorem prover known to us that supports the same selection of intermediate propositional logics. It was obtained through modification of an existing SAT-based theorem prover for intuitionistic propositional logic. Their methods have similar theoretical foundations, though more akin to using restricted cuts, as opposed to our embedding approach.
intuitRIL outperforms (or matches) SuperJ in intuitionistic propositional logic, particularly so for domains SYJ206 and SYJ209. Except for SYJ208, SuperJ is only ever faster with a minimal constant factor, this might be due to there being a slightly smaller preprocessing overhead compared to intuitRIL that uses a clausification procedure.
For Jankov logic, intuitRIL solved the same number of problems within almost the same amount of time as for IPL. There is no real slowdown by the addition of the axiom instantiations for this prover. The SuperJ prover is more sensitive to the addition of the axiom instantiations, e.g., it finds a proof earlier for problems in SYJ209 but is slower in SYJ201-SYJ205, SYJ211 and SYJ212. intuitRIL (Jan) Solved Time 2 0.024 12 0.144 20 2.754 10 14.322 20 0.243 20 0.244 20 0.248 20 0.239 20 0.612 20 2.306 20 0.240 20 0.240 20 0.241 20 0.241 20 0.239
SuperJ (Göd) Solved Time 2 0.023 8 0.092 1 0.022 1 0.012 3 1.724 3 0.326 0 — 4 3.946 20 0.496 10 1.446 4 23.207 4 4.636 1 3.132 5 19.868 19 0.218 intuitRIL (Göd) Solved Time 2 0.024 12 0.144 20 2.754 10 14.352 20 0.244 20 0.242 20 0.242 20 0.243 20 1.054 17 165.925 20 0.264 20 0.313 20 97.985 20 0.302 20 0.252
Finally, for Gödel logic, intuitRIL again managed to solve most of the problems within the time limit. However, compared to itself for other logics, it is slower for domains SYJ208 and SYJ211. The performance of SuperJ on the same logic is below that of intuitRIL, except for domains LCL and SYJ207. Perhaps this is not so surprising, considering the axiomatisation of Gödel logic contains (nested) implications, a known weak point for sequent based provers such as SuperJ.
The automated theorem provers for first-order intermediate logic described in Section 3 were evaluated on the problems of the ILTP library. All test were conducted on a 2.0 GHz Xeon server with 64 GB of RAM running Linux Mint with kernel version 3.10 and ECLiPSe Prolog 5.10. Table 3 shows the results of the evaluation on all 2550 first-order problems of the ILTP library v1.1.2 [25] for a CPU time limit of 10 seconds. Included are the provers ileanSeP-im 1.0, ileanTAP-im 1.17 and nanoCoP-im 2.0. Each of these implementations were tested for intuitionistic logic (“IL”), Jankov logic (“Jan”) and Gödel logic (“Göd”). Furthermore, the prover leanCoP 2.2 for classical first-order logic was included, which provides an upper limit for the number of problems that can be proved by one of the provers for intermediate logic. nanoCoP-im proves the most problems for each of the non-classical logics. ileanSeP-im proves slightly less problems than ileanTAP-im for IL, but more problems than ileanTAP-im for Jankov and Gödel logic. nanoCoP-im also refutes the largest number of problems for all three logics.
All three provers prove less problems for Jankov logic than for IL and less problems for Gödel logic than for Jankov logic. This is explained by the overhead in the search space caused by the additional intermediate axioms that are added to the formulas. In general, the problems proved in Gödel logic are a subset of the problems proved in Jankov logic, which are again a subset of the problems proved in IL. Table 4 shows the few exceptions where a problem was proved in Jankov (or Gödel) logic but not in IL, or proved in Gödel logic but not in Jankov logic. The entries show the CPU time in seconds necessary to prove a problem or (in parentheses) to refute it. These problems are from the domains Set Theory (SET), Software Verification (SWV) and Syntactic (SYN). Given a larger CPU time limit, the problems in the SET and SWV domains can be proved in IL by nanoCoP-i or Slakje [18], i.e., they are valid in IL. — nanoCoP-im — IL Jan Göd – 7.5 – – 7.9 – – 9.7 – – 8.9 – – 9.3 – – 0.2 0.2 (0.1) (0.1) 0.1 leanCoP 2.2
Classical 0.6 0.1 0.3
– 2.1 0.1 0.1
We implemented four provers for Jankov and Gödel logic via proof search for intuitionistic logic and bounding functions: SuperJ for the propositional Jankov and Gödel logics and ileanSeP-im, ileanTAP-im and nanoCoP-im for the first-order Jankov and Gödel logics. The SuperJ implementation is available at https://github.com/bhaaksema/superintuition, the ileanSeP-im, ileanTAP-im and nanoCoP-im implementations are available at https://leancop.de/imed/. While bounding functions could be added to any existing intuitionistic theorem prover, SuperJ is a new prover aimed at facilitating quick experimentation with heuristics. To the best of our knowledge, ileanSeP-im, ileanTAP-im and nanoCoP-im are the first provers for first-order Jankov and first-order Gödel logic.
Our tests have shown that very few problems in the ILTP library which are valid in Jankov or Gödel logic are not valid in intuitionistic logic. Therefore, it seems advisable to build a collection of such problems for future benchmarking, possibly generated by (forward) proofs in the sequent calculus.
The methodology applies to other intermediate logics, e.g., Scott’s and Kreisel-Putnam logic axiomatized over IPL respectively by ((¬¬A → A) → (A ∨ ¬A)) → (¬¬A ∨ ¬A) and (¬A → (B ∨ C)) → ((¬A → B) ∨ (¬A → C)). It would also be interesting to extend the methodology to substructural logics.
Fiorentini and Ferrari [26] give a propositional intermediate logic prover intuitRIL that modularly extends a SAT-based prover for IPL. Fiorino [27, 28] present duplication-free tableau calculi for Gödel logic and three other propositional intermediate logics, including Jankov logic. Kuznets and Lellmann [29] give semantically inspired constructions of nested sequent calculi for propositional intermediate logics including Gödel logic, and a prototype proof search implementation was also presented.
For classical logic, many state-of-the-art theorem provers use heuristics that select a subset of appropriate axioms in a preprocessing step before the actual proof search [30]. As our approach adds many axioms to the formula to be proven, integrating such heuristics will likely improve the performance of our provers. This will be part of future work, along with further optimization and evaluations of the provers. [10] M. Ferrari, C. Fiorentini, G. Fiorino, fcube: An efficient prover for intuitionistic propositional logic, in: Logic for Programming, Artificial Intelligence, and Reasoning, Springer, Berlin, Heidelberg, 2010, pp. 294–301. [11] M. Ferrari, C. Fiorentini, G. Fiorino, Simplification rules for intuitionistic propositional tableaux,
ACM Trans. Comput. Logic 13 (2012). doi:10.1145/2159531.2159536. [12] H. Ono, Proof Theory and Algebra in Logic, Short Textbooks in Logic, 1st ed., Springer, Singapore, 2019. doi:10.1007/978-981-13-7997-0. [13] J. Otten, ileanTAP: An intuitionistic theorem prover, in: D. Galmiche (Ed.), TABLEAUX 1997, volume 1227 of LNAI, Springer, Heidelberg, 1997, pp. 307–312. doi:10.1007/BFb0027422. [14] M. Fitting, Proof Methods for Modal and Intuitionistic Logics, D. Reidel, Dordrecht, 1983. [15] R. M. Smullyan, First-Order Logic, Springer, Berlin, Heidelberg, New York, 1968. [16] L. A. Wallen, Automated Deduction in Nonclassical Logics, MIT Press, Cambridge, 1990. [17] J. Otten, Non-clausal connection calculi for non-classical logics, in: R. Schmidt, C. Nalon (Eds.), TABLEAUX 2017, volume 10501 of LNAI, Springer, 2017, pp. 209–227. doi:10.1007/ 978-3-319-66902-1_13. [18] J. Otten, The nanoCoP 2.0 connection provers for classical, intuitionistic and modal logics, in: A. Das, S. Negri (Eds.), TABLEAUX 2021, volume 12842 of LNAI, Springer, 2021, pp. 236–249. doi:10.1007/978-3-030-86059-2\_14. [19] J. Otten, nanoCoP: A non-clausal connection prover, in: N. Olivetti, A. Tiwari (Eds.), IJCAR 2016, volume 9706 of LNAI, Springer, 2016, pp. 302–312. doi:10.1007/978-3-319-40229-1_21. [20] J. Otten, nanoCoP: Natural non-clausal theorem proving, in: C. Sierra (Ed.), Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI-17, Sister Conference Best Paper Track, IJCAI, 2017, pp. 4924–4928. doi:10.24963/ijcai.2017/695. [21] J. Otten, W. Bibel, leanCoP: lean connection-based theorem proving, Journal of Symbolic Computation 36 (2003) 139–161. doi:10.1016/S0747-7171(03)00037-3. [22] J. Otten, W. Bibel, Advances in connection-based automated theorem proving, in: M. Hinchey, J. P. Bowen, E.-R. Olderog (Eds.), Provably Correct Systems, NASA Monographs in Systems and Software Engineering, Springer, Cham, 2017, pp. 211–241. doi:10.1007/978-3-319-48628-4_ 9. [23] J. Otten, A non-clausal connection calculus, in: K. Brünnler, G. Metcalfe (Eds.), TABLEAUX 2011, volume 6793 of LNAI, Springer, 2011, pp. 226–241. doi:10.1007/978-3-642-22119-4_18. [24] J. Otten, Restricting backtracking in connection calculi, AI Commun. 23 (2010) 159–182. doi:10.
3233/AIC-2010-0464. [25] T. Raths, J. Otten, C. Kreitz, The ILTP problem library for intuitionistic logic, Journal of Automated
Reasoning 38 (2007) 261–271. doi:10.1007/s10817-006-9060-z. [26] C. Fiorentini, M. Ferrari, Sat-based proof search in intermediate propositional logics, in: Automated Reasoning, Springer International Publishing, Cham, 2022, pp. 57–74. doi:10.1007/ 978-3-031-10769-6_5. [27] G. Fiorino, An O(n log n)-space decision procedure for the propositional dummett logic., Journal of Automated Reasoning 27 (2001) 297–311. doi:10.1023/a:1017515831550. [28] G. Fiorino, Space-efficient Decision Procedures for Three Interpolable Propositional Intermediate
Logics, Journal of Logic and Computation 12 (2002) 955–992. doi:10.1093/logcom/12.6.955. [29] R. Kuznets, B. Lellmann, Interpolation for intermediate logics via injective nested sequents, Journal of Logic and Computation 31 (2021) 797–831. doi:10.1093/logcom/exab015. [30] K. Hoder, A. Voronkov, Sine qua non for large theory reasoning, in: N. Bjørner, V. SofronieStokkermans (Eds.), CADE-23, volume 6803 of LNCS, Springer, 2011, pp. 299–314. doi:10.1007/ 978-3-642-22438-6\_23.