Clausal Connection-Based Theorem Proving in Intuitionistic First-Order Logic

Jens Otten

Institut für Informatik, University of Potsdam August-Bebel-Str. 89, 14482 Potsdam-Babelsberg, Germany

                        jeotten@cs.uni-potsdam.de

Abstract. We present a clausal connection calculus for first-order intuitionistic logic. It extends the classical connection calculus by adding prefixes that encode the characteristics of intuitionistic logic. Our calculus is based on a clausal matrix characterisation for intuitionistic logic, which we prove correct and complete. The calculus was implemented by extending the classical prover leanCoP. We present some details of the implementation, called ileanCoP, and experimental results.

1 Introduction

Automated reasoning in intuitionistic first-order logic is an important task within the formal approach of constructing verifiable correct software. Interactive proof assistants, like NuPRL [5] and Coq [2], use constructive type theory to formalise the notion of computation and would greatly benefit from a higher degree of automation. Automated theorem proving in intuitionistic logic is considerably more difficult than in classical logic, because additional non-permutabilities in the intuitionistic sequent calculus [8] increase the search space. In classical logic (disjunctive or conjunctive) clausal forms are commonly used to simplify the problem of copying appropriate subformulae (so-called multiplicities). Once a formula is converted into clausal form multiplicities can be restricted to clauses. For intuitionistic logic a validity-preserving clausal form does not exist.

An elegant way of encoding the intuitionistic non-permutabilities was given by Wallen [30] by extending Bibel’s (non-clausal) characterisation of logical validity [3]. The development of proof calculi and implementations based on this characterisation (e.g. [11, 21, 22, 25]) were restricted to non-clausal procedures, making it difficult to use more established clausal methods (e.g. [3, 4, 13, 14]).

In this paper we present a clausal matrix characterisation for intuitionistic logic. Extending the usual Skolemization technique makes it possible to adapt a connection calculus that works on prefixed matrices in clausal form. It simplifies the notation of multiplicities and the use of existing clausal connection-based implementations for classical logic. Only a few changes are required to adapt the classical prover leanCoP to deal with prefixed matrices.

The paper is organised as follows. In Section 2 the standard (non-clausal) matrix characterisation is presented before Section 3 introduces a clausal characterisation using Skolemization and a prefixed connection calculus. The ileanCoP implementation with experimental results is described in Section 4. We conclude with a summary and a brief outlook on further research in Section 5.

2 Preliminaries

We assume the reader to be familiar with the language of classical first-order logic (see, e.g., [7]). We start by defining some basic concepts before briefly describing the matrix characterisation for classical and intuitionistic logic.

2.1 Formula Trees, Types and Multiplicities

Some basic concepts are formula trees, types and multiplicities (see [4, 7, 30]). Multiplicities encode the contraction rule in the sequent calculus [8].

Definition 1 (Formula Tree). A formula tree is the graphical representation of a formula F as a tree. Each node is labeled with a connective/quantifier or atomic subformula of F and marked with a unique name, its position, denoted by a_{0}, a_{1}, …. The set of all positions is denoted by Pos. The tree ordering < ⊆ Pos × Pos is the (partial) ordering on the positions in the formula tree, i.e. a_{i}<a_{j} iff position a_{i} is below position a_{j} in the formula tree.

Example 1. Figure 1 shows the formula tree for F_{1} = ∀xP x ⇒ P b ∧ P c with Pos = {a_{1}, …, a_{5}}. It is, e.g., a_{1}<a_{2} and a_{0}<a_{4}. Note that each subformula of a given formula corresponds to exactly one position in its formula tree, e.g. ∀xP x corresponds to the position a_{1}.

[figure: ⇒ a_{0}; ∀x a_{1}; ∧ a_{3}; P x a_{2}; P b a_{4} a_{5}; P c; a_{0} ⇒^{0} (α,ψ); a_{1} ∀^{1}x (γ,ϕ); a_{2} P^{1}a_{1} (ϕ); a_{6} ∀^{1}x (γ,ϕ); a_{7} P^{1}a_{6} (ϕ); a_{3} ∧^{0} (β); a_{4} P^{0}b (ψ); a_{5} P^{0}c (ψ); α]

Fig. 1. Formula tree for F_{1} and F_{1}^{μ} with μ(a_{1}) = 2

Definition 2 (Types, Polarity). The principal and intuitionistic type of a position is determined by its label and polarity according to Table 1 (e.g. a formula/position A ∧ B with polarity 1 has type α). Atomic positions have no principal type and some positions have no intuitionistic type. We denote the sets of positions of type γ, δ, ϕ, and ψ by Γ, Δ, Φ, and Ψ, respectively. The polarity (0 or 1) of a position is determined by the label and polarity of its predecessor in the formula tree according to table 1 (e.g. if A ∧ B has polarity 1 then both subformula A and B have polarity 1 as well). The root position has polarity 0.

Example 2. In the left formula tree for F_{1} in Figure 1 (ignore the additional branch for now) each node/position is marked with its types and its polarity. The positions a_{0}, a_{1}, a_{3} have principal type α, γ and β, respectively; the positions a_{1}, a_{2} and a_{0}, a_{4}, a_{5} have intuitionistic type ϕ and ψ, respectively.

Table 1. Principal type, intuitionistic type and polarity of positions/subformulae

principal type α  (A ∧ B)^{1}  (A ∨ B)^{0}  (A⇒B)^{0} (¬A)^{1} (¬A)^{0}
successor polarity  A^{1}, B^{1}  A^{0}, B^{0}  A^{1}, B^{0}  A^{0}  A^{1}
principal type β  (A ∧ B)^{0}  (A ∨ B)^{1}  (A⇒B)^{1}
successor polarity  A^{0}, B^{0}  A^{1}, B^{1}  A^{0}, B^{1}

principal type γ (∀xA)^{1} (∃xA)^{0}

successor polarity  A^{1}  A^{0}

principal type δ (∀xA)^{0} (∃xA)^{1}
successor polarity  A^{0}  A^{1}
intuitionistic type ϕ  (¬A)^{1}  (A⇒B)^{1}  (∀xA)^{1} P^{1} (P is atomic)
intuitionistic type ψ  (¬A)^{0}  (A⇒B)^{0}  (∀xA)^{0} P^{0} (P is atomic)

Definition 3 (Multiplicity). The multiplicity μ : Γ ∪ Φ → IN assigns each position of type γ and ϕ a natural number. By F^{μ} we denote an indexed formula. In the formula tree of F^{μ} multiple instances of subformulae — according to the multiplicity of its positions — have been considered. The branch instances of a subformula have an implicit node/position of type α as predecessor.

Example 3. The formula tree for F_{1} with μ(a_{1})=2 is shown in Figure 2. Here and in the following we will replace variables in atomic formulae by their quantifier positions. Thus positions of type γ and δ appear in atomic formulae.

2.2 Matrix Characterisation for Classical Logic

To resume the characterisation for classical logic [3, 4] we introduce the concepts of matrices, paths and connections. A path corresponds to a sequent and a connection to an axiom in the sequent calculus [8]. For the first-order case we also need the notation of first-order substitution and reduction ordering.

Definition 4 (Matrix,Path,Connection).

1. In the matrix(-representation) of an indexed formula F^{μ} we place the subformulae of a formula of principal type α side by side whereas subformulae of a subformula of principal type β are placed one upon the other. Furthermore, we omit all connectives and quantifiers.

2. A path through an indexed formula F^{μ} is a subset of the atomic formulae of its formula tree; it is a horizontal path through the matrix of F^{μ}.

3. A connection is a pair of atomic formulae with the same predicate symbol but with different polarities.

Example 4. The matrix for F_{1}^{μ} is given in Figure 2. There are two paths through F_{1}^{μ}: {P^{1}a_{1}, P^{1}a_{6}, P^{0}b} and {P^{1}a_{1}, P^{1}a_{6}, P^{0}c}. They contain the connections {P^{1}a_{1}, P^{0}b}, {P^{1}a_{6}, P^{0}b} and {P^{1}a_{1}, P^{0}c}, {P^{1}a_{6}, P^{0}c}, respectively. We will present a more formal definition of matrices and paths in Section 3.

[ P^{1}a_{1} P^{1}a_{6} \begin{matrix}P^{0}b \\ P^{0}c \end{matrix} ] \frac{Γ,A ⊢}{Γ ⊢ ¬A,Δ} \frac{Γ,A ⊢ B}{Γ ⊢ A⇒B,Δ} \frac{Γ ⊢ A[x\a]}{Γ ⊢ ∀xA,Δ}

¬-right  ⇒-right  ∀-right

Fig. 2. Matrix for F_{1}^{μ} and special intuitionistic sequent rules

Definition 5 (First-order Substitution, Reduction Ordering).

1. A first-oder substitution σ_{Q} : Γ → T assigns to each position of type γ a term t ∈ T . T is the set of terms made up of constants, functions and elements of Γ and Δ, which are called term variables and term constants, respectively. A connection {P^{0}s, P^{1}t} is said to be σ_{Q}-complementary iff σ_{Q}(s)=σ_{Q}(t). σ_{Q} induces a relation ⊏_{Q} ⊆ Δ × Γ in the following way: for all u ∈ Γ v⊏_{Q}u holds for all v ∈ Δ occurring in σ_{Q}(u).

2. The reduction ordering ⊲ := (< ∪ ⊏_{Q})^{+} is the transitive closure of the tree ordering < and the relation ⊏_{Q}. A first order substitution σ_{Q} is said to be admissible iff the reduction ordering ⊲ is irreflexive.

Theorem 1 (Characterisation for Classical Logic [4]). A (first-order) formula F is classically valid, iff there is a multiplicity μ, an admissible first-order substitution σ_{Q} and a set of σ_{Q}-complementary connections such that every path through F^{μ} contains a connection from this set.

Example 5. Let μ(a_{1})=2 and σ_{Q}={a_{1}\b, a_{6}\c}, i.e. σ_{Q}(a_{1})=b, σ_{Q}(a_{6})=c. σ_{Q} is admissible, since the induced reduction ordering (= tree ordering) is irreflexive. {{P^{1}a_{1}, P^{0}b}, {P^{1}a_{6}, P^{0}c}} is a σ_{Q}-complementary set of connections and every path through F_{1}^{μ} contains a connection from this set. Thus F_{1} is classically valid.

2.3 Matrix Characterisation for Intuitionistic Logic

A few extensions are necessary to adapt the characterisation of classical validity to intuitionistic logic. These are prefixes and an intuitionistic substitution. Prefixes encode the characteristics of the special rules (see Figure 2) in the intuitionistic sequent calculus (see [30]). Alternatively they can be seen as an encoding of the possible world semantics of intuitionistic logic (see [30]).

Definition 6 (Prefix). Let u_{1}<u_{2}< … <u_{n}≤u be the positions of type ϕ or ψ that dominate the position/formula u in the formula tree. The prefix of u, denoted pre(u), is a string over Φ ∪ Ψ and defined as pre(u) := u_{1}u_{2} … u_{n}.

Example 6. For the formula F_{1}^{μ} we obtain pre(a_{2})=a_{0}A_{1}A_{2}, pre(a_{7})= a_{0}A_{6}A_{7}, pre(a_{4})=a_{0}a_{4} and pre(a_{5})=a_{0}a_{5}. Positions of type ϕ are written in capitals.

Definition 7 (Intuitionistic/Combined Substitution, Admissibility).

1. An intuitionistic substitution σ_{J} : Φ → (Φ ∪ Ψ)^{∗} assigns to each position of type ϕ a string over the alphabet (Φ∪Ψ). Elements of Φ and Ψ are called prefix variables and prefix constants, respectively. σ_{J} induces a relation ⊏_{J} ⊆ Ψ ×Φ in the following way: for all u∈Φ v⊏_{J}u holds for all v∈Ψ occurring in σ_{J}(u).

2. A combined substitution σ:=(σ_{Q}, σ_{J}) consists of a first-order and an intuitionistic substitution. A connection {P^{0}s, P^{1}t} is σ-complementary iff σ_{Q}(s)=σ_{Q}(t) and σ_{J}(pre(P^{0}s))=σ_{J}(pre(P^{1}t)). The reduction ordering ⊲ := (< ∪ ⊏_{Q} ∪ ⊏_{J})^{+} is the transitive closure of <, ⊏_{Q} and ⊏_{J}.

3. A combined substitution σ=(σ_{Q}, σ_{J}) is said to be admissible iff the reduction ordering ⊲ is irreflexive and the following condition holds for all u ∈ Γ and all v ∈ Δ occurring in σ_{Q}(u): σ_{J}(pre(u))=σ_{J}(pre(v))∘q for some q ∈ (Φ∪Ψ)^{∗}.

Theorem 2 (Characterisation for Intuitionistic Logic [30]). A formula F is intuitionistically valid, iff there is a multiplicity μ, an admissible combined substitution σ = (σ_{Q}, σ_{J}), and a set of σ-complementary connections such that every path through F^{μ} contains a connection from this set.

Example 7. Let μ(a_{1})=2 and σ = (σ_{Q}, σ_{J}) with σ_{Q}={a_{1}\b, a_{6}\c} and σ_{J} = {A_{1}\ε, A_{2}\a_{4}, A_{6}\ε, A_{7}\a_{5}} in which ε denotes the empty string. Then σ is admissible and {{P^{1}a_{1}, P^{0}b}, {P^{1}a_{6}, P^{0}c}} is a σ_{Q}-complementary set of connections and every path through F_{1}^{μ} contains a connection from this set. Therefore F_{1} is intuitionistically valid.

3 Clausal Connection-Based Theorem Proving

This section presents a clausal version of the matrix characterisation for intuitionistic logic and a prefixed connection calculus based on this characterisation.

3.1 Prefixed Matrix and Skolemization

In order to develop a prefixed connection calculus more formal definitions of the concepts of a matrix and paths (as introduced in Definition 4) are required. Afterwards we will also introduce a Skolemization technique, which extends the Skolemization used for classical logic to intuitionistic logic.

A (non-clausal, i.e. nested) matrix is a set of clauses and contains α-related subformulae. A clause is a set of matrices and contains β-related subformulae. A (non-clausal) matrix is a compact representation of a (classical) formula and can be represented in the usual two dimensional graphical way. Adding prefixes will make it suitable to represent intuitionistic formulae as well. The formal definition of paths through a (matrix of a) formula is adapted accordingly.

Definition 8 (Prefixed Matrix).

1. A prefix p is a string with p ∈ (Φ ∪ Ψ)^{∗}. Elements of Φ and Ψ play the role of variables and constants, respectively. A prefixed (signed) formula F^{pol}:p is a formula F marked with a polarity pol ∈ {0, 1} and a prefix p.

2. A prefixed matrix M is a set of clauses in which a clause is a set of prefixed matrices and prefixed atomic formulae. The prefixed matrix of a prefixed formula F^{pol}:p is inductively defined according to Table 2. In Table 2 A, B are formulae, P s is an atomic formula, p ∈ (Φ ∪ Ψ)^{∗} is a prefix, Z ∈ Φ, a ∈ Ψ are new (unused) elements. A_{x} and A_{c} is the formula A in which y is replaced by new (unused) elements x ∈ Γ and c ∈ Δ, respectively. The prefixed matrix of a formula F, denoted matrix(F), is the prefixed matrix of F^{0}:ε.

Definition 9 (Path). A path through a (prefixed) matrix M or clause C is a set of prefixed atomic formulae and defined as follows: If M={{P^{pol}s:p}} is a matrix and P s an atomic formula then {P^{pol}s:p} is the only path through M. Otherwise if M={C_{1}, .., C_{n}} is a matrix and path_{i} is a path through the clause C_{i} then ⋃_{i=1}^{n} path_{i} is a path through M. If C={M_{1}, .., M_{n}} is a clause and path_{i} is a path through the matrix M_{i} then path_{i} (for 1≤i≤n) is a path through C.

Table 2. The prefixed matrix of a formula F^{pol}:p

Formula

Prefixed matrix M_{A}, M_{B} is
F^{pol}:p of F^{pol}:p matrix of
(P^{1}s):p {{P^{1}s:p∘Z}}
(P^{0}s):p {{P^{0}s:p ∘a}}
(A ∧ B)^{1}:p {{M_{A}}, {M_{B}}} A^{1}:p , B^{1}:p
(A ∨ B)^{0}:p {{M_{A}}, {M_{B}}} A^{0}:p , B^{0}:p
(A⇒B)^{0}:p {{M_{A}}, {M_{B}}} A^{1}:p , B^{0}:p
(∀yA)^{1}:p  M_{A}  A_{x}^{1}:p ∘Z
(∃yA)^{0}:p  M_{A}  A_{x}^{0}:p

Formula

Prefixed matrix M_{A}, M_{B} is

F^{pol}:p  of F^{pol}:p  matrix of
(¬A)^{1}:p  M_{A}  A^{0}:p∘Z
(¬A)^{0}:p  M_{A}  A^{1}:p ∘a
(A ∧ B)^{0}:p {{M_{A}, M_{B}}} A^{0}:p , B^{0}:p
(A ∨ B)^{1}:p {{M_{A}, M_{B}}} A^{1}:p , B^{1}:p
(A⇒B)^{1}:p {{M_{A}, M_{B}}} A^{0}:p , B^{1}:p
(∀yA)^{0}:p  M_{A}  A_{c}^{0}:p ∘a
(∃yA)^{1}:p  M_{A}  A_{c}^{1}:p

Example 8. The prefixed matrix of formula F_{1} (see examples in Section 2) is M_{1}=matrix(F_{1})= {{P^{1}x_{1}:a_{2}Z_{3}Z_{4}}, {P^{0}b:a_{2}a_{5}, P^{0}c:a_{2}a_{6}}}, in which submatrices of the form {{M_{1}, .., M_{n}}} have been simplified to M_{1}, .., M_{n}. The paths through M_{1} are {P^{1}x_{1}:a_{2}Z_{3}Z_{4}, P^{0}b:a_{2}a_{5}} and {P^{1}x_{1}:a_{2}Z_{3}Z_{4}, P^{0}c:a_{2}a_{6}}.

An indexed formula F^{μ} is defined in the usual way, i.e. each subformula F′ of type γ or ϕ is assigned its multiplicity μ(F′) ∈ IN encoding the number of instances to be considered. Before F^{μ} is translated into a matrix, each F′ is replaced with (F′_{1} ∧ … ∧ F′_{μ(F′)}) in which F′_{i} is a copy of F′. The notation of σ-complementary is slightly modified, i.e. a connection {P^{0}s:p, P^{1}t:q} is σcomplementary iff σ_{Q}(s)=σ_{Q}(t) and σ_{J}(p)=σ_{J}(q).

For a combined substitution σ to be admissible (see Definition 7) the reduction ordering ⊲ induced by σ has to be irreflexive. In classical logic this restriction encodes the Eigenvariable condition in the classical sequent calculus [8]. It is usually integrated into the σ-complementary test by using the well-known Skolemization technique together with the occurs-check of term unification. We extend this concept to the intuitionistic substitution σ_{J}. To this end we introduce a new substitution σ_{<}, which is induced by the tree ordering <. σ_{<} assigns to each constant (elements of Δ and Ψ) a Skolemterm containing all variables (elements of Γ and Φ) occurring below this constant in the formula tree. It is sufficient to restrict σ_{<} to these elements, since ⊏_{J} ⊆ Ψ × Φ and ⊏_{Q} ⊆ Δ × Γ.

Definition 10 (σ_{<}-Skolemization). A tree ordering substitution σ_{<} : (Δ∪Ψ) → T assigns a Skolemterm to every element of Δ ∪ Ψ. It is induced by the tree ordering < in the following way: σ_{<} := { c\c(x_{1}, ...x_{n}) | c ∈ Δ ∪ Ψ and for all x ∈ Γ ∪ Φ: (x ∈ {x_{1}, … x_{n}} iff x < c)}.

Example 9. The tree ordering of formula F_{1} induces the substitution σ_{<} = {a_{2}\a_{2}(), a_{5}\a_{5}(), a_{6}\a_{6}()}, since no variables occur before any constant.

Note that we follow a purely proof-theoretical view on Skolemization, i.e. as a way to integrate the irreflexivity test of the reduction ordering into the condition of σ-complementary. For classical logic this close relationship was pointed out by Bibel [4]. Like for classical logic the use of Skolemization simplifies proof calculi and implementations. There is no need for an explicit irreflexivity check and subformulae/-matrices can be copied by just renaming all their variables.

Lemma 1 (Admissibility Using σ_{<}-Skolemization). Let F be a formula and < be its tree ordering. A combined substitution σ = (σ_{Q}, σ_{J}) is admissible iff (1) σ′ = σ_{<}∪σ_{Q}∪σ_{J} is idempotent, i.e. σ′(σ′) = σ′, and (2) the following holds for all u ∈ Γ and all v ∈ Δ occurring in σ_{Q}(u): σ_{J}(pre(u))=σ_{J}(pre(v))∘q for some q ∈ (Φ ∪ Ψ)^{∗}.

Proof. It is sufficient to show that ⊲ is reflexive iff σ_{<}∪σ_{Q}∪σ_{J} is not idempotent. ”⇒”: Let ⊲ be reflexive. Then there are positions with a_{1}⊲ … ⊲a_{n}⊲a_{1}. For each a_{i}⊲a_{j} there is a_{i}<a_{j}, a_{i}⊏_{Q}a_{j} or a_{i}⊏_{J}a_{j}. According to Definition 10, 5 and 7 there is some substitution with {a_{j}\t} in σ_{<}, σ_{Q} or σ_{J}, respectively, in which a_{i} occurs in t. Then σ_{<}∪σ_{Q}∪σ_{J} is not idempotent. ”⇐”: Let σ_{<}∪σ_{Q}∪σ_{J} be not idempotent. Then there is σ′={a_{1}\..a_{n}.., a_{n}\..a_{n−1}.., …, a_{2}\..a_{1}..}⊆σ_{<}∪σ_{Q}∪σ_{J}. Each {a_{j}\..a_{i}..} ∈ σ′ is part of σ_{<}, σ_{Q} or σ_{J}. According to Definition 10, 5 and 7 it is a_{i}<a_{j}, a_{i}⊏_{Q}a_{j} or a_{i}⊏_{J}a_{j}. Therefore ⊲:=(<∪⊏_{Q}∪⊏_{J})^{+} is reflexive. □

3.2 A Clausal Matrix Characterisation

We will now define prefixed matrices in clausal form and adapt the notation of multiplicities to clausal matrices before presenting a clausal matrix characterisation for intuitionistic logic. The restriction of multiplicities to clauses makes it possible to use existing clausal calculi for which multiplicities can be increased during the proof search in an easy way. The transformation of a prefixed matrix to clausal form is done like for classical logic. Note that we apply the substitution σ_{<} to the clausal matrix, i.e. to terms and prefixes of atomic formulae.

Definition 11 (Prefixed Clausal Matrix). Let < be a tree ordering and M be a prefixed matrix. The (prefixed) clausal matrix of M, denoted clausal(M), is a set of clauses in which each clause is a set of prefixed atomic formulae. It is inductively defined as follows: If M has the form {{P^{pol}s:p}} then clausal(M):=M; otherwise clausal(M) := ⋃_{C ∈ M}{{⋃_{i=1}^{n} c_{i}} | c_{i} ∈ clausal(M_{i}) and C={M_{1}, …, M_{n}}}. The (prefixed) clausal matrix of a formula F (with tree ordering <), denoted M_{c} = matrix_{c}(F), is σ_{<}(clausal(matrix(F))).

Definition 12 (Clausal Multiplicity). The clausal multiplicity μ_{c} : M_{c} → IN assigns each clause in M_{c} a natural number, specifying the number of clause instances to be considered. matrix_{c}^{μ}(F) denotes the clausal matrix of F in which clause instances/copies specified by μ_{c} have been considered. Term and prefix variables in clause copies are renamed (Skolemfunctions are not renamed).

Example 10. For F_{1} let μ_{c}({P^{1}x_{1}:a_{2}()Z_{3}()Z_{4}()}) = 2. Then matrix_{c}^{μ}(F_{1}) = {{P^{1}x_{1}:a_{2}()Z_{3}Z_{4}}, {P^{1}x_{7}:a_{2}()Z_{8}Z_{9}}, {P^{0}b:a_{2}()a_{5}(), P^{0}c:a_{2}()a_{6}()}}.

Note that we use the same Skolemfunction (symbol) for instances of the same subformula/clause. This is an optimisation, which has a similar effect like the liberalised δ^{+}-rule for (classical) semantic tableaux [9]. Since we apply the substitution σ_{<} to the clausal matrix, term and prefix constants can now both contain term and prefix variables. Therefore the first-order and intuitionistic substitutions σ_{Q} and σ_{J} are extended so that they assign terms over Γ ∪Δ∪Φ∪Ψ to term and prefix variables (elements of Γ and Φ).

Theorem 3 (Clausal Characterisation for Intuitionistic Logic). A formula F is intuitionistically valid, iff there is a multiplicity μ_{c}, an admissible combined substitution σ = (σ_{Q}, σ_{J}), and a set of σ-complementary connections such that every path through matrix_{c}^{μ}(F) contains a connection from this set. Proof. Follows directly from the following Lemma 2 and Theorem 2. □

Lemma 2 (Equivalence of Matrix and Clausal Matrix Proofs). There is a clausal matrix proof for F iff there is a (non-clausal) matrix proof for F. Proof. Main idea: paths through clausal matrix and (non-clausal) matrix of F are identical and substitutions and multiplicities μ_{c}/μ can be transfered into each other. Note that in the following proof ”variable” refers to term and prefix variables. We assume that σ_{<} is applied to the non-clausal matrix as well. ”⇒”: Let (μ_{c}, σ, S) be a clausal matrix proof of F in which S is the connection set. We will construct a matrix proof (μ, σ′, S′) for F. Let M_{c}=matrix_{c}^{μ}(F) be the clausal matrix of F (with clause instances according to μ_{c}). We construct a matrix M=matrix(F^{μ}) in the following way: We start with the original matrix M. For each clause C_{i} ∈ M_{c} we identify the vertical path through M which represents C_{i} (modulo Skolemfunction names); see matrices on left side of Figure 3. If this vertical path shares variables with already identified clauses in M we copy the smallest subclause of M, so that the new path contains copies x′_{1}, .., x′_{n} of all (term and prefix) variables x_{1}, .., x_{n} in C_{i} with σ(x_{i})≠σ(x′_{i}). Note that Skolemfunctions in copied subclauses of M are renamed and therefore unique. The constructed matrix M determines μ. Let σ′:=σ and S′:=S. We identify every connection {P^{0}s:p, P^{1}t:q} ∈ S from M_{c} as {P^{0}s′:p′, P^{1}t′:q′} in M. If s′, t′, p′ or q′ contain a Skolemfunction f_{i} (which is unique in M), we rename Skolemfunctions in σ′ so that σ′(s′, p′)=σ(t′, q′). There can be no renaming conflict for the set S′: Let f(x_{1}), f(x_{2}), .. be the same Skolemfunctions in M_{c}, which are represented by different Skolemfunctions f_{1}(x_{1}), f_{2}(x_{2}), .. in M. If σ(x_{i})≠σ(x_{j}) then different Skolemfunctions do not matter, since f_{i}(x_{i}) and f_{j}(x_{j}) are never assigned to the same variable. The case σ(x_{i})=σ(x_{j}) does not occur according to the construction of M. If copies of the same variable are substituted by the same term, the branches in the formula tree can be folded up (see right side of Figure 3); otherwise the branches (and Skolemterms) differ. Every path through M contains a path from M_{c} as a subset. Therefore (μ, σ′, S′) is a proof for F.

M_{C}=matrix_{C}^{μ}(F)= ; [.. [ ⋮ ; ..f(x′).. ; ⋮ ; ⋮ ] ..] ; C_{i} ⇝ M=matrix(F^{μ})= ; [.. [ ^{…} ; [^{[ ..f_{1}(x).. ]} [ ..f_{2}(x′).. ; ⋮ ] ] ; ⋮ ] ..] ; C_{i}  [figure: ⇝; f(x); x; σ(f(x′)); σ(f(x))=; σ(x′); σ(x) =]

Fig. 3. Clause C_{i} in (non-)clausal matrix and folding up branches in formula tree

”⇐”: Let (μ, σ′, S′) be a (non-clausal) matrix proof for F. We will construct a clausal matrix proof (μ_{c}, σ, S). Let M=matrix(F^{μ}) be the matrix of F^{μ}. We construct a clausal matrix M_{c}=matrix_{c}^{μ}(F) in the following way: We start with the clausal form of the original formula F, i.e. M_{c}=matrix_{c}(F). We extend M_{c} by using an appropriate μ_{c}, so that it is the clausal form of M (modulo Skolemfunction and variable names). Let σ:=σ′ and S:=S′. We extend σ by unifying all variables x_{1}, x_{2}, .. in M_{c} which have the same image in M. Since copied Skolemfunction names in M differ, but are identical in M_{c} we can simply replace them with a unique name in σ. Then all connections in S are σ-complementary. By induction we can also show that every path through M_{c} contains a connection from S. Therefore (μ_{c}, σ, S) is a clausal proof for F. □

3.3 A Prefixed Connection Calculus

The clausal characterisation of intuitionistic validity in Theorem 3 serves as a basis for a proof calculus. Calculating the first-order substitution σ_{Q} is done by the well-known algorithms for term unification (see, e.g., [16]). Checking that all paths contain a connection can be done by, e.g., sequent calculi [8] tableau calculi [7] or connection-driven calculi [3, 4, 13, 14]. The clausal connection calculus is successfully used for theorem proving in classical logic (see, e.g., [12]). A basic version of the connection calculus for first-order classical logic is presented in [19]. The calculus uses a connection-driven search strategy, i.e. in each step a connection is identified along an active (sub-)path and only paths not containing the active path and this connection will be investigated afterwards. The clausal multiplicity μ_{c} is increased dynamically during the path checking process. We adapt this calculus to deal with intuitionistic logic (based on the clausal characterisation) by adding prefixes to the atomic formulae of each clause as specified in Definition 8 and 11.

Definition 13 (Prefixed Connection Calculus). The axiom and the rules of the prefixed connection calculus are given in Figure 3. M is a prefixed clausal matrix, C, C_{p}, C_{1}, C′_{2} are clauses of M and C_{p} is a positive clause (i.e. contains no atomic formulae with polarity 1), C_{1}∪\{\overline{L}\} contains no (term or prefix) variables, C′_{2}∪\{\overline{L′}\} contains at least one variable and C_{2}/\overline{L} are copies of C′_{2}/\overline{L′} in which all variables have been renamed. \{L, \overline{L}\} and \{L, \overline{L′}\} are σ-complementary connections, and P ath is the active path, which is a subset of some path trough M. A formula F is valid iff there is an admissible substitution σ = (σ_{Q}, σ_{J}) and a derivation for matrix_{c}(F) in which all leaves are axioms.

Axiom:  Start Rule:  Reduction Rule:
\overline{(\{\}, M, P ath)}  \frac{(C_{p}, M∪\{C_{p}\}, \{\})}{M∪\{C_{p}\}}  \frac{(C, M, P ath∪\{\overline{L}\})}{(C∪\{L\}, M, P ath∪\{\overline{L}\})}
\frac{(C,M,P ath) (C_{1}, M, P ath∪\{L\})}{(C∪\{L\}, M∪\{C_{1}∪\{\overline{L}\}\}, P ath)}  \frac{(C,M,P ath) (C_{2}, M∪\{C′_{2}∪\{\overline{L′}\}\}, P ath∪\{L\})}{(C∪\{L\}, M∪\{C′_{2}∪\{\overline{L′}\}\}, P ath)}

Extension Rule: Extension^{∗} Rule:

Fig. 4. The connection calculus for first-order logic

Example 11. Let matrix_{c}(F_{1})={{P^{1}x_{1}:a_{2}()Z_{3}Z_{4}},{P^{0}b:a_{2}()a_{5}(), P^{0}c:a_{2}()a_{6}()}} =M be the clausal matrix of F_{1}. The following is a derivation for M.

\frac{\overline{(\{\}, M, \{\})}  \overline{(\{\}, M, \{P^{0}c:a_{2}()a_{6}()\})}}{(\{P^{0}c:a_{2}()a_{6}()\}, M, \{\})}  \overline{(\{\}, M, \{P^{0}b:a_{2}()a_{5}()\})}
\overline{(\{P^{0}b:a_{2}()a_{5}(), P^{0}c:a_{2}()a_{6}()\}, M, \{\})}
\overline{\{\{P^{1}x_{1}:a_{2}()Z_{3}Z_{4}\}, \{P^{0}b:a_{2}()a_{5}(), P^{0}c:a_{2}()a_{6}()\}\}}

Axiom Axiom

Extension^{∗} Axiom

Extension^{∗} Start

This derivation is a proof for F_{1} with the admissible substitution σ=(σ_{Q}, σ_{J}) and σ_{Q}={x′_{1}\b, x′′_{2}\c}, σ_{J}={Z′_{3}\ε, Z′_{4}\a_{2}()a_{5}(), Z′′_{3}\ε, Z′′_{4}\a_{2}()a_{6}()}, i.e. F_{1} is valid.

The intuitionistic substitution σ_{J} can be calculated using the prefix unification algorithm in [20]. It calculates a minimal set of most general unifiers for a given set of prefixes {s_{1}=s_{1}, .., t_{n}=t_{n}} by using a small set of rewriting rules (similar to the algorithm in [16] for term unification). The following definition briefly describes this algorithm (see [20] for a detailed introduction).

Definition 14 (Prefix Unification). The prefix unification of two prefixes s and t is done by applying the rewriting rules defined in Table 3. The rewriting rules replace a tuple (E, σ_{J}) by a modified tuple (E′, σ_{J}′) in which E and E′ represent a prefix equation and σ_{J}, σ_{J}′ are intuitionistic substitutions. Rules are applied non-deterministically. We start with the tuple ({s = ε|t}, {}), for technical reasons we divide the right part of t, and stop when the tuple ({}, σ_{J}) is derived. In this case σ_{J} represents a most general unifier. There can be more than one most general unifier (see [20]). The algorithm can also be used to calculate a unifier for a set of prefix equations {s_{1}=t_{1}, .., s_{n}=t_{n}} in a stepwise manner.

We use these symbols: s, t, z ∈ (Φ∪Ψ)^{∗}, s^{+}, t^{+}, z^{+}∈ (Φ∪Ψ)^{+}, X ∈ (Φ∪Ψ), V, V_{1} V′ ∈ Φ and C, C_{1}, C_{2} ∈ Ψ. V′ is a new variable which does not refer to a position in the formula tree and does not occur in the substitution σ_{J} computed so far.

Table 3. Rewriting rules for prefix unification

R1. {ε = ε|ε}, σ_{J}  → {}, σ_{J}
R2. {ε = ε|t^{+}}, σ_{J}  → {t^{+} = ε|ε}, σ_{J}
R3. {Xs = ε|Xt}, σ_{J}  → {s = ε|t}, σ_{J}
R4. {Cs = ε|V t}, σ_{J}  → {V t = ε|Cs}, σ_{J}
R5. {V s = z|ε}, σ_{J}  → {s = ε|ε}, {V \z}∪σ_{J}
R6. {V s = ε|C_{1}t}, σ_{J}  → {s = ε|C_{1}t}, {V \ε}∪σ_{J}
R7. {V s = z|C_{1}C_{2}t}, σ_{J} → {s = ε|C_{2}t}, {V \zC_{1}}∪σ_{J}
R8. {V s^{+} = ε|V_{1}t}, σ_{J} → {V_{1}t = V |s^{+}}, σ_{J}  (V ≠V_{1})
R9. {V s^{+} = z^{+}|V_{1}t}, σ_{J} → {V_{1}t = V′|s^{+}}, {V \z^{+}V′}∪σ_{J}  (V′ ∈ Φ)
R10. {V s = z|Xt}, σ_{J}  → {V s = zX|t}, σ_{J}  (s=ε or t≠ε or X ∈ Ψ)

Example 12. In the first step/connection of the proof for F_{1} we need to unify the prefixes s = a_{2}Z′_{3}Z′_{4} and t = a_{2}a_{5}. This is done as follows: ({a_{2}Z′_{3}Z′_{4}=ε|a_{2}a_{5}}, {})

⟶^{R3} ({Z′_{3}Z′_{4}=ε|a_{5}}, {}) ⟶^{R6} ({Z′_{4}=ε|a_{5}}, {Z′_{3}\ε}) ⟶^{R10} ({Z′_{4}=a_{5}|ε}, {Z′_{3}\ε}) ⟶^{R5}

({ε=ε|ε}, {Z′_{3}\ε, Z′_{4}\a_{5}}) ⟶^{R1} ({}, {Z′_{3}\ε, Z′_{4}\a_{5}}). Note that the second (most

general) unifier can be calculated by using rule R10 instead of R6.

4 An Implementation: ileanCoP

The calculus presented in Section 3 was implemented in Prolog. We will present details of the implementation and performance results. The source code (and more information) can be obtained at http://www.leancop.de/ileancop/ .

4.1 The Code

leanCoP is an implementation of the clausal connection calculus presented in Section 3 for classical first-order logic [19]. The reduction rule is applied before extension rules are applied and open branches are selected in a depth-first way. We adapt leanCoP to intuitionistic logic by adding

a. prefixes to atomic formulae and a prefix unification procedure, b. to each clause the set of term variables contained in it and an admissibility

check in which these sets are used to check condition (2) of Lemma 1.

The main part of the ileanCoP code is depicted in Figure 5. The underlined text was added to leanCoP; no other changes were done. A prefix Pre is added to atomic formulae q:Pre in which Pre is a list of prefix variables and constants. The set of term variables Var is added to each clause Var:Cla in which Var is a list containing pairs [V,Pre] in which V is a term variable and Pre its prefix.

 (1)       prove(Mat,PathLim) :-
 (2)            append(MatA,[\underline{FV:}Cla|MatB],Mat), \+ member(-\underline{(} \underline{):} ,Cla),
 (3)            append(MatA,MatB,Mat1),
 (4)            prove([!\underline{:[]}],[\underline{FV:}[-\underline{(}!\underline{):(-[])}|Cla]|Mat1],[],PathLim\underline{,[PreSet,FreeV]})\underline{,}
 (5)            \underline{check addco(FreeV), prefix unify(PreSet)}.
 (6)       prove(Mat,PathLim) :-
 (7)  \+ ground(Mat), PathLim1 is PathLim+1, prove(Mat,PathLim1).
 (8)       prove([], , , \underline{,[[],[]]}).
 (9)       prove([Lit\underline{:Pre}|Cla],Mat,Path,PathLim\underline{,[PreSet,FreeV]}) :-
(10)            (-NegLit=Lit;-Lit=NegLit) ->
(11)               ( member(NegL\underline{:PreN},Path), unify with occurs check(NegL,NegLit)\underline{,}
(12)                 \underline{\+ \+ prefix unify([Pre=PreN]), PreSet1=[], FreeV3=[]}
(13)                 ;
(14)                 append(MatA,[Cla1|MatB],Mat), copy term(Cla1,\underline{FV:}Cla2),
(15)                 append(ClaA,[NegL\underline{:PreN}|ClaB],Cla2),
(16)                 unify with occurs check(NegL,NegLit),
(17)                 \underline{\+ \+ prefix unify([Pre=PreN]),}
(18)                 append(ClaA,ClaB,Cla3),
(19)                 ( Cla1==FV\underline{:Cla2} ->
(20)                      append(MatB,MatA,Mat1)
(21)                      ;
(22)                      length(Path,K), K<PathLim,
(23)                      append(MatB,[Cla1|MatA],Mat1)
(24)                 ),
(25)                 prove(Cla3,Mat1,[Lit\underline{:Pre}|Path],PathLim\underline{,[PreSet1,FreeV1]})\underline{,}
(26)                 \underline{append(FreeV1,FV,FreeV3)}
(27)               ),
(28)               prove(Cla,Mat,Path,PathLim\underline{,[PreSet2,FreeV2]})\underline{,}
(29)               \underline{append([Pre=PreN|PreSet1],PreSet2,PreSet),}
(30)               \underline{append(FreeV2,FreeV3,FreeV)}.

Fig. 5. Main part of the ileanCoP source code

Condition (2) of the admissibility check, check addco, and the unification of prefixes, prefix unify, are done after a classical proof, i.e. a set of connections, has been found. Therefore the set of prefix equations PreSet and the clause-variable sets FreeV are collected in an additional argument of prove. check addco and prefix unify require 5 and 26 more lines of code, respectively (see [20, 22]). Condition (1) of the admissibility check of Lemma 1 is realized by the occurs-check of Prolog during term unification. Two prefix constants are considered equal if they can be unified by term unification. Note that we perform a weak prefix unification (line 12 and 17) for each connection already during the path checking process (double negation prevents any variable bindings).

To prove the formula F_{1} from Section 2 and 3 we call prove(M,1). in which

M= [ [[X,[1^[],Z]]]:[-(p(X)): -([1^[],Z,Y])], []:[p(b):\[1^[],2^[]],p(c):

[1^[],3^[]]] ] is the prefixed matrix of F_{1} (with clause-variable sets added).

4.2 Refuting some First-Order Formulae

In order to obtain completeness ileanCoP performs iterative deepening on the proof depth, i.e. the size of the active path. The limit for this size, PathLim, is increased after the proof search for a given path limit has failed (line 7 in Figure 5). If the matrix contains no variables, the given matrix is refuted.

We will integrate a more restrictive method in which the path limit will only be increased if the current path limit was actually reached. In this case the predicate pathlim is written into Prolog’s database indicating the need to increase the path limit if the proof search fails. It can be realized by modifying the following lines of the code in Figure 5:

     (7)            retract(pathlim), PathLim1 is PathLim+1, prove(Mat,PathLim1).
    (22)                      length(Path,K), ( K<PathLim ->
    (23a)                     append(MatB,[Cla1|MatA],Mat1) ;
    (23b)  \+ pathlim -> assert(pathlim), fail )

The resulting implementation is able to refute a large set of first-order formulae (but it does not result in a decision procedure for propositional formulae).

4.3 Performance Results

We have tested ileanCoP on all 1337 non-clausal (so-called FOF) problems in the TPTP library [27] of version 2.7.0 that are classically valid or are not known to be valid/invalid. The tests were performed on a 3 GHz Xeon system running Linux and ECLiPSe Prolog version 5.7 (”nodbgcomp.” was used to generate code without debug information). The time limit for all proof attempts was 300 s.

The results of ileanCoP are listed in the last column of Table 4. We have also included the results of the following five theorem provers for intuitionistic first-order logic: JProver [25] (implemented in ML using a non-clausal connection calculus and prefixes), the Prolog and C versions of ft [24] (using an intuitionistic tableau calculus with many additional optimisation techniques and a contraction-free calculus [6] for propositional formulae), ileanSeP (using an intuitionistic tableau calculus; see http://www.leancop.de/ileansep) and ileanTAP [22] (using a tableau calculus and prefixes). The timings of the classical provers Otter [17], leanTAP [1] and leanCoP [19] are provided as well.

Table 4. Performance results of ileanCoP and other provers on the TPTP library

Otter leanTAP leanCoP ileanSeP JProver ft_{P rolog} ft_{C}  ileanTAP ileanCoP
solved  509  220  335  90  96  112  125  116  234
proved 509  220  335  87  94  99  112  113  188
refuted  0  0  0  3  2  13  13  3  46
0 to <1s 431  202  280  76  80  106  122  110  192
to <10s  54  9  23  8  9  5  1  2  16
to <100s  22  8  29  4  7  1  2  2  17
to <300s  2  1  3  2  0  0  0  2  9
intui. 0.0  -  -  -  60  76  74  76  76  76
to ≤0.7  -  -  -  21  20  33  40  34  39
to ≤1.0  -  -  -  9  0  5  9  6  119
class. 0.0 256  163  227  75  85  92  100  88  175
to ≤1.0 253  57  108  15  11  20  25  28  59
time out 360 1012  944  1173 1237 1171  667 1165 1041
error  468  105  58  74  4  54  545  56  62

Of the 234 problems solved by ileanCoP 112 problems could not be solved by any other intuitionistic prover. The rating (see rows eight to twelve) expresses the relative difficulty of the problems from 0.0 (easy) to 1.0 (very difficult). The intuitionistic rating is taken from the ILTP library [23].

4.4 Analysing Test Runs

The proof search process of ileanCoP can be divided into the following four sections: transformation into clausal form, search for a ”classical” proof (using weak prefix unification), admissibility check and prefix unification. We mark the transition to these sections with the letters a, b and c as follows:

a  b  c
clausal transformation ”classical”-proof admissibility check prefix unification

Table 5 contains information about how often each section is entered when running ileanCoP on the 1337 TPTP problems. The numbers assigned to the letters express the number of times this section is entered. For example the column a=b=c=1 means that each section is entered just once. The rows var(ø,max) contain the average and maximum number of variables collected when entering section b, whereas the rows pre(ø,max) contain the average and maximum number of prefix equations collected when entering section c.

Most of the problems (178 formulae) have been proved without backtracking in sections a/b (1st column) or section a (2nd column). This means that the corresponding classical sequent proofs can be converted into intuitionistic sequent proofs by simply reordering the rules. Most of the refuted problems (40 formulae) failed because of weak prefix unification in section a (5th column).

Table 5. Analysis of the TPTP test runs

a=b=c=1 a=b=1; c>1 a=1; b,c>1 a=1; b≥1; c=0 a=1; b=c=0 a=b=c=0
proved  159  19  10  -  -  -
var(ø,max) (13,216)  (21,62)  (11,23)  -  -  -
pre(ø,max) (29,1191) (22,119)  (13,26)  -  -  -
refuted  1  -  3  2  40  -
var(ø,max)  (2,2)  -  (3,5)  (5,5)  -  -
pre(ø,max)  (3,3)  -  (4,4)  -  -  -
time out  3  31  17  2  987  62
var(ø,max) (26,34)  (25,106)  (41,146)  (47,70)  -  -
pre(ø,max) (15,19)  (21,99)  (40,112)  -  -  -

For 987 problems no ”classical” proof could be found (5th column). For 62 problems (6th column) the size of the clausal form is too big and the transformation results in a stack overflow (”error” in Table 4). For 31 problems sections b and c did not finish after a ”classical” proof has been found (2nd column).

5 Conclusion

We have presented a clausal matrix characterisation for intuitionistic logic based on the standard characterisation [30] (see also [29]). Encoding the tree-ordering by an additional substitution replaces the reflexivity test of the reduction ordering by checking if the (extended) combined substitution is idempotent. Due to this Skolemization technique and the transformation into clausal form, multiplicities can be restricted to clauses and clause instances can be generated by just renaming the term and prefix variables of the original clauses. This allows the use of existing clausal calculi and implementations for classical logic (in contrast to specialised calculi [28]), without the redundancy caused by (relational) translations [18] into classical first-order logic. Instead an additional prefix unification is added, which captures the specific restrictions of intuitionistic logic, i.e.

first-order logic = propositional logic + term unification ,
intuitionistic logic = classical logic  + prefix unification .

We have adapted a clausal connection calculus and transformed the classical prover leanCoP into the intuitionistic prover ileanCoP with only minor additions. Experimental results on the TPTP library showed that the performance of ileanCoP is significantly better than any other (published) automated theorem prover for intuitionistic first-order logic available today. The correctness proof provides a way to convert the clausal matrix proofs back into non-clausal matrix proofs, which can then be converted into sequent-style proofs [26].

While a clausal form technically simplifies the proof search procedure, it has a negative effect on the size of the resulting clausal form and the search space. A non-clausal connection-based proof search, which increases multiplicities in a demand-driven way, would not suffer from this weakness. Whereas the used prefix unification algorithm is very straightforward to implement, it can be improved by solving the set of prefix equations in a more simultaneous way. The clausal characterisation, the clausal connection calculus and the implementation can be adapted to all modal logics considered within the matrix characterisation framework [30, 21, 11] by changing the unification rules [20]. By adding tests for the linear and relevant constraints within the complementary condition it can even be adapted to fragments of linear logic [10, 11, 15].

Acknowledgements

The author would like to thank Thomas Raths for providing the performance results for the listed classical and intuitionistic theorem proving systems.

References

1. B. Beckert, J. Posegga. leanTAP: lean, tableau-based theorem proving. 12^{t}^{h} CADE, LNAI 814, pp. 793–797, Springer, 1994.

2. Y. Bertot, P. Castéran. Interactive Theorem Proving and Program Development. Texts in Theoretical Computer Science, Springer, 2004.

3. W. Bibel. Matings in matrices. Communications of the ACM , 26:844–852, 1983.

4. W. Bibel. Automated Theorem Proving. Vieweg, second edition, 1987.

5. R. L. Constable et. al. Implementing Mathematics with the NuPRL proof development system. Prentice Hall, 1986.

6. R. Dyckhoff. Contraction-free sequent calculi for intuitionistic logic. Journal of Symbolic Logic, 57:795–807, 1992.

7. M. C. Fitting. First-Order Logic and Automated Theorem Proving. Springer, 1990.

8. G. Gentzen. Untersuchungen über das logische Schließen. Mathematische Zeitschrift, 39:176– 210, 405–431, 1935.

9. R. Hähnle, P. Schmitt The Liberalized δ-rule in free variable semantic tableaux. Journal of Automated Reasoning, 13:211–221, 1994.

10. C. Kreitz, H. Mantel, J. Otten, S. Schmitt Connection-based proof construction in linear logic. 14^{th} CADE, LNAI 1249, pp. 207–221, Springer, 1997.

11. C. Kreitz, J. Otten. Connection-based theorem proving in classical and non-classical logics. Journal of Universal Computer Science, 5:88–112, Springer, 1999.

12. R. Letz, J. Schumann, S. Bayerl, W. Bibel. Setheo: A high-performance theorem prover. Journal of Automated Reasoning, 8:183–212, 1992.

13. R. Letz, G. Stenz Model elimination and connection tableau procedures. Handbook of Automated Reasoning, pp. 2015–2114, Elsevier, 2001.

14. D. Loveland. Mechanical theorem proving by model elimination. JACM , 15:236–251, 1968.

15. H. Mantel, J. Otten. linTAP: A tableau prover for linear logic. 8^{th} TABLEAUX Conference, LNAI 1617, pp. 217–231, Springer, 1999.

16. A. Martelli, U. Montanari. An efficient unification algorithm. ACM Transactions on Programming Languages and Systems (TOPLAS), 4:258–282, 1982.

17. W. McCune. Otter 3.0 reference manual and guide. Technical Report ANL-94/6, Argonne National Laboratory, 1994.

18. H. J. Ohlbach et al. Encoding two-valued nonclassical logics in classical logic. Handbook of Automated Reasoning, pp. 1403–1486, Elsevier, 2001.

19. J. Otten, W. Bibel. leanCoP: lean connection-based theorem proving. Journal of Symbolic Computation, 36:139–161, 2003.

20. J. Otten, C. Kreitz. T-string-unification: unifying prefixes in non-classical proof methods. 5^{th} TABLEAUX Workshop, LNAI 1071, pp. 244–260, Springer, 1996.

21. J. Otten, C. Kreitz. A uniform proof procedure for classical and non-classical logics. KI-96: Advances in Artificial Intelligence, LNAI 1137, pp. 307–319, Springer, 1996.

22. J. Otten. ileanTAP: An intuitionistic theorem prover. 6^{th} TABLEAUX Conference, LNAI 1227, pp. 307–312, Springer, 1997.

23. T. Raths, J. Otten, C. Kreitz. The ILTP library: benchmarking automated theorem provers for intuitionistic logic. TABLEAUX 2005 , this volume, 2005. (http://www.iltp.de)

24. D. Sahlin, T. Franzen, S. Haridi. An intuitionistic predicate logic theorem prover. Journal of Logic and Computation, 2:619–656, 1992.

25. S. Schmitt et. al.JProver: Integrating connection-based theorem proving into interactive proof assistants. IJCAR-2001 , LNAI 2083, pp. 421–426, Springer, 2001.

26. S. Schmitt, C. Kreitz Converting non-classical matrix proofs into sequent-style systems. 13^{th} CADE, LNAI 1104, pp. 2–16, Springer, 1996.

27. G. Sutcliffe, C. Suttner. The TPTP problem library - CNF release v1.2.1. Journal of Automated Reasoning, 21: 177–203, 1998. (http://www.cs.miami.edu/∼tptp)

28. T. Tammet. A resolution theorem prover for intuitionistic logic. 13^{th} CADE, LNAI 1104, pp. 2–16, Springer, 1996.

29. A. Waaler Connections in nonclassical logics. Handbook of Automated Reasoning, pp. 1487– 1578, Elsevier, 2001.

30. L. Wallen. Automated deduction in nonclassical logic. MIT Press, 1990.