This paper introduces a non-clausal connection calculus for intuitionistic first-order logic. It is an extension of the non-clausal connection calculus for classical logic by prefixes and an additional prefix unification, which encode the Kripke semantics of intuitionistic logic. nanoCoP-i is a first implementation of this intuitionistic non-clausal connection calculus. Details of the compact Prolog code are presented, which extends the non-clausal connection prover nanoCoP for classical logic. Experimental evaluations on the ILTP and the TPTP problem libraries show a solid performance of the nanoCoP-i prover. In comparison to the ileanCoP prover, the resulting non-clausal proofs are not only shorter, but can also be more easily translated into, e.g., sequent proofs. Intuitionistic (or constructive) logic is one of the most popular non-classical logics. It is often used when constructing provably correct software, for example within the NuPRL [6] proof development system. Other interactive proof assistants, such as Coq [3], use a constructive logic as well. Hence, automated reasoning in intuitionistic logic is an important task and many applications would benefit from more powerful reasoning tools. During the last decade the development of automated theorem proving (ATP) systems for classical first-order logic has made significant progress. Extending these ATP systems to intuitionistic logic is usually not (easily) possible, as many of the underlying calculi and techniques can not be adapted to intuitionistic logic. Most leading ATP systems for classical logic require the translation of the input formulae into a clausal form, i.e. into disjunctive or conjunctive normal form. For intuitionistic logic there is no validity-preserving translation into such a (simple) clausal form. Nevertheless, ileanCoP, one of the fastest ATP systems for intuitionistic first-order logic, uses a clausal connection calculus and additional prefixes to capture the semantics of intuitionistic logic [16]. While the use of a clausal form technically simplifies the proof search, the standard translation as well as the definitional translation [22] into clausal form introduce a significant overhead into the proof search [17]. Furthermore, a translation into clausal form modifies the structure of the original formula and the translation of the clausal form proof back into one of a more readable proof of the original formula is not straightforward [24, 25]. On the other hand, fully automated theorem provers that use nonclausal calculi, such as standard tableau or sequent calculi, have a significant lower performance [16]. The paper is structured as follows. Section 2 introduces the non-clausal connection calculus for intuitionistic first-order logic, which works on prefixed non-clausal matrices. The non-clausal connection calculus and the prefix unification that is additionally required are presented. An implementation of the intuitionistic non-clausal connection calculus is described in Section 3. It provides details about the non-clausal prefixed matrices, the source code of the non-clausal proof search and the prefix unification algorithm. Section 4 presents an evaluation of the implementation on the ILTP and the TPTP problem libraries. The paper concludes with a short summary and an outlook on future work in Section 5.
2
The prefixed non-clausal matrix is the main concept used in the intuitionistic connection calculus. The intuitionistic connection calculus uses prefixes and requires an additional prefix unification algorithm. 2.1
The standard notation for first-order formulae is used. Terms (denoted byt) are built up from functions (denoted by f ), constants and (term) variables (denoted by x). An atomic formula (denoted by A) is built up from predicate symbols and terms. A (first-order) formula (denoted by F, G, H ) is built up from atomic formulae, the connectives ¬, ∧, ∨, ⇒, and the standard first-order quantifiers∀ and ∃. A literal L has the form A or ¬A. Its complement L is A if L is of the form ¬A; otherwise L is ¬L.
A connection is a set {A, ¬A} of literals with the same predicate symbol but different polarity. A term substitution σQ assigns terms to variables.
Intuitionistic logic [
The intuitionistic non-clausal connection calculus is based on Wallen’s matrix characterization [
Definition 2.1 (Prefix). A prefix(denoted by p) is a string, i.e., a sequence of characters over an alphabet Φ ∪ Ψ, in which Φ is a set of prefix variables(V1, ...) and Ψ is a set of prefix constants(a1, ...).
Semantically, a prefix encodes a sequence of worlds in a Kripke model. Proof-theoretically, prefix
constants and variables represent applications of the rules ¬-right, ⇒-right, ∀-right, and ¬-left, ⇒-left,
∀-left in the sequent calculus [
Definition 2.2 (Intuitionistic substitution, σ-complementary). An intuitionistic substitution σJ : Φ → (Φ ∪ Ψ)∗ maps elements of Φ to strings over Φ ∪ Ψ. For a combined substitution σ := (σQ, σJ ), a connection {L1 : p1, L2 : p2} is σ-complementary iff σQ(L1) = σQ(L2) and σJ (p1) = σJ (p2).
An additional domain condition on σ ensures that σQ and σJ are mutually consistent [
An intuitionistic non-clausal matrix is a set of prefixed clauses, which consist of prefixed literals and prefixed (sub)matrices. Thepolarity 0 or 1 is used to represent negation in a matrix, i.e. literals of the form A and ¬A are represented by A0 and A1, respectively, Definition 2.3 (Intuitionistic non-clausal matrix). Let F be a formula, pol be a polarity, and p be a prefix. The prefixed (non-clausal) matrix M (F pol:p) of a prefixed formula F pol:p is a set of prefixed clauses, in which a prefixed clause is a set of prefixed literals and prefixed (non-clausal) matrices, and defined inductively according to Table 1. G[x\t] denotes the formula G in which all free occurrences of x are replaced by t. x∗ is a new term variable, t∗ is the Skolem term f ∗(x1, . . . , xn) in which f ∗ is a new function symbol and x1, . . . , xn are all free term and prefix variables in (∀xG)0 : p or (∃xG)1 : p. V ∗ is a new prefix variable, a∗ is a prefix constant of the form f ∗(x1, . . . , xn) in which f ∗ is a new function symbol and x1, . . . , xn are all free term and prefix variables in A0 : p, (¬G)0 : p, (G⇒H)0 : p, or (∀xG)0 : p. The intuitionistic (non-clausal) matrix M (F ) of F is the prefixed matrix M (F 0 : ε).
In the graphical representation of a matrix, its clauses are arranged horizontally, while the literals and (sub-)matrices of each clause are arranged vertically.
For example, the formula
( man(Socrates) ⇒ man(Socrates) ) ∧ ( ( man(Plato) ∧ ∀x(man(x)⇒mortal(x)) ) ⇒ mortal(Plato) ) has the (simplified, i.e. redundant brackets are removed) intuitionistic non-clausal matrix {{ {{man(Socrates)0 : a1V1}, {man(Socrates)1 : a1a2}}, {{man(Plato)1 : a3V2}, {man(x)0 : a3V3V4a4(V3, x, V4), mortal(x)1 : a3V3V4V5}, {mortal(Plato)0 : a3a5}} }} , and the following graphical representation man(Socrates)0:a1V1
man(Socrates)1:a1a2 man(Plato)1:a3V2 . 2.3
The non-clausal connection calculus for intuitionistic logic extends the non-clausal connection calculus
for classical logic [
For example, the proof of formula (2) and its matrix (3) consists of three connections, which are represented by a line in the following graphical matrix representation. The three connections are σ-complementary with σ = (σQ, σJ ) and σQ(x) = Plato, σJ (V1) = a2, σJ (V2) = a4(ε, Plato, ε), σJ (V3) = ε, σJ (V4) = ε, σJ (V5) = a5 (where ε is the empty string). . (4) man(Socrates)0:a1V1
man(Socrates)1:a1a2 man(Plato)1:a3V2
{{man(Socrates)0 : a1}, {man(Socrates)1 : a2}} .
There is only one connection {man(Socrates)0 : a1, man(Socrates)1 : a2} which is σ-complementary if the two prefixesa1 and 2 can be unified. There is no substitutionσJ with σJ (a1) = σJ (a2) and, hence, no connection proof of this matrix. Therefore, the formula man(Socrates) ∨ ¬man(Socrates) is not valid in intuitionistic logic.
A few additional concepts are required as follows in order to specify which clauses can be used within the generalized non-clausal extension rule.
Definition 2.4 (α-related, parent clause, clause copy). A clause C contains a literal L (or clause C00) iff L ∈ C or C0 contains L (C = C00 or C0 contains C00) for a matrix M 0 ∈ C with C0∈ M . A clause C is α-related to a literal L iff it occurs besides L in the graphical matrix representation; more precisely, C is α-related to a literal L iff {C0, C00} ⊆ M 0 for some matrix M 0 such that C0 contains L and C00 contains C. C0 is a parent clause of C iff M 0 ∈ C0 and C ∈ M 0 for some matrix M 0. In the copy of a clause C all free variables in C are replaced by fresh variables. M [C1\C2] denotes the matrix M , in which the clause C1 is replaced by the clause C2.
For example, in the matrix (3) the clauses {man(Plato)1 : a3V2} and {mortal(Plato)0 : a3a5} are αrelated. { {{man(Socrates)0 : a1V1}, {man(Socrates)1 : a1a2}}, {{man(Plato)1 : a3V2}, {man(x)0 : a3V3V4a4(V3, x, V4), mortal(x)1 : a3V3V4V5}, {mortal(Plato)0 : a3a5}} } is the parent clause of all other clauses in the matrix, e.g., of the clause {man(Socrates)0 : a1V1}.
{}, M, P ath C2, M, {} ε, M, ε
C, M, P ath∪{L2 : p2} C∪{L1 : p1}, M, P ath∪{L2 : p2} and C2 is copy of C1∈M C3, M [C1\C2], P ath∪{L1: p1} C, M, P ath C∪{L1: p1}, M, P ath and {L1 : p1, L2 : p2} is σ-complementary and C3:=β-clauseL2 (C2), C2 is copy of C1, C1 is e-clause of M wrt. P ath ∪ {L1:p1}, C2 contains L2:p2, {L1:p1, L2:p2} is σ-complementary
C ∪ C1, M, P ath C∪{M1}, M, P ath
and C1∈M1 Definition 2.5 (Extension clause, β-clause). C is an extension clause (e-clause) of the matrix M with respect to a set of literals P ath iff either (a) C contains a literal of P ath, or (b) C is α-related to all literals of P ath occurring in M and if C has a parent clause, it contains a literal of P ath. In the β-clause of C2 with respect to L2, denoted by β-clauseL2 (C2), L2 and all clauses that are α-related to L2 are deleted from C2 (in the new subgoal C3).
The non-clausal connection calculus for intuitionistic logic has the same axiom, start rule, and
reduction rule as the clausal connection calculus [
Definition 2.6 (Intuitionistic non-clausal connection calculus). The axiom and the rules of the intuitionistic (non-clausal) connection calculus are given in Fig. 1. It works on tuples “ C, M, P ath”, where M is a prefixed non-clausal matrix, C is a prefixed (subgoal) clause or ε and (the active) P ath is a set of prefixed literals or ε. σ = (σQ, σJ ) is a combined term and prefix substitution. An intuitionistic (non-clausal) connection proof of a prefixed matrix M is an intuitionistic connection proof of ε, M, ε.
The non-clausal connection calculus for intuitionistic logic is correct and complete, i.e. a formula
F is valid in intuitionistic logic if and only if there is an intuitionistic non-clausal connection proof
of its intuitionistic non-clausal matrix M (F ). It follows from the correctness and completeness of the
non-clausal connection calculus [
The analytic, i.e., bottom-up proof search in the non-clausal calculus is carried out in the same way
as in the clausal calculus. Additional backtracking might be required when choosing the clause C1
in the decomposition rule; no backtracking is required when choosing the matrix M1. The rigid term
and intuitionistic substitutions σQ and σJ are calculated whenever a reduction or extension rule is
applied. The term substitution is calculated by one of the well-known algorithms for term unification. The
intuitionistic substitution is calculated by a prefix unification algorithm (see Section 2.4).
Optimization techniques, such as positive start clauses, regularity, lemmata and restricted backtracking, can be
employed in a similar way as in the clausal connection calculus for intuitionistic logic [
The intuitionistic substitution σJ is calculated by a prefix unification algorithm [
Definition 2.7. The prefix unification for the prefixes equation {p = q} is carried out by applying the rewriting rules R1 to R10 in Figure 2. It is V, V¯ , V 0 ∈ Φ with V 6= V¯ , V 0 is a new prefix variable, a, b ∈ Ψ, X ∈ Φ ∪ Ψ, and u, w, z ∈ (Φ ∪ Ψ)∗. For rule 10 the restriction (∗) u = ε or w 6= ε or X ∈ Ψ applies. σJ (V ) = u is written {V \u}. The unification starts with the tuple ({p = ε|q}, {}). The application of a rewriting rule E → E0, τ replaces the tuple (E, σJ ) by the tuple (E0, τ (σJ )). E and E0 are prefix equations, σJ and τ are substitutions. The unification terminates when the tuple ({}, σJ ) is derived. In this case, σJ represents a most general unifier. Rules can be applied non-deterministically and lead to a minimal set of most general unifiers.
R1. {ε=ε|ε} R2. {ε=ε|Xu} → {}, {} → {Xu=ε|ε}, {} R3. {Xu=ε|Xw} → {u=ε|w}, {} R4. {au=ε|V w} → {V w=ε|au}, {} R5. {V u=z|ε} → {u=ε|ε}, {V \z}
R6.
R7.
R8.
{V u=ε|aw} {V u=z|abw} {V au=ε|V¯ w} → {u=ε|aw}, {V \ε} → {u=ε|bw}, {V \za} → {V¯ w=V |au}, {} R9.
R10. {V u=z|Xw} {V au=Xz|V¯ w} → {V¯ w=V 0|au}, {V \XzV 0}
→ {V u=zX|w}, {} (∗)
The following implementation of the intuitionistic non-clausal connection calculus of Fig. 1 follows
the lean methodology [
In a first step the input formulaF is translated into its intuitionistic non-clausal matrix M (F ) according
to Table 1; redundant brackets of the form “ {{. . .}}” are removed [
For example, the matrix 3 from Sec. 2.2 is represented by the Prolog term [(2ˆK)ˆ[]ˆ[]: [4ˆK:[(5ˆK)ˆ[]ˆ[]:[-(man(socrates)): -([3ˆ[]])],
(7ˆK)ˆ[]ˆ[]:[man(socrates):[3ˆ[]]] ], 10ˆK:[(11ˆK)ˆ[]ˆ[]:[-(man(plato)): -([8ˆ[]])], (13ˆK)ˆ[V,X,W]ˆ[X:[8ˆ[],W]]:[man(X):[8ˆ[],W,V],
-(mortal(X)):-([8ˆ[],W,V])],
(19ˆK)ˆ[]ˆ[]:[mortal(plato):[8ˆ[]]] ] ] ]
in which the Prolog variable K is instantiated later on in order to enumerate clause copies; as an
optimization, prefix characters introduced by atomic formulae are only considered during the unification. In
the second step the matrix M (F ) is written into Prolog’s database. For every literal Lit in M the fact
lit(Lit,ClaB,ClaC,Grnd)
is asserted into the database where ClaC ∈ M is the (largest) clause in which Lit occurs and ClaB
is the β-clause of ClaC with respect to Lit. Grnd is set to g if the smallest clause in which Lit
occurs is ground, i.e. does not contain any variables; otherwise Grnd is set to n. Storing literals of M
in the database in this way is called lean Prolog technology [
The nanoCoP-i source code is shown in Fig. 3. It is an extension of the non-clausal connection prover
nanoCoP [
First, nanoCoP-i performs a classical proof search, in which the prefixes of each connection are stored in PreS. If the search succeeds, the domain condition is checked and the prefixes in PreS are unified (line 4), using the predicatesdomain_cond and prefix_unify (see Section 3.3), respectively.
The predicate prove(Mat,PathLim,Set,Proof) implements the start rule (lines 1–4) and iterative deepening on the length of the active path (lines 5–9). Mat is the prefixed matrix generated in the preprocessing step, PathLim is the maximum size of the active path used for iterative deepening, Set is a list of options used to control the proof search, and Proof contains the returned intuitionistic (non-clausal) connection proof. Start clauses are restricted to positive clauses (line 2): after member selects a start clause, positiveC(Cla,Cla1) returns the clause Cla1 in which all clauses that are not positive in Cla are deleted. A clause is positive if all of its elements (matrices and literals) are positive; a matrix is positive if it contains at least one positive clause; a literal is positive if its polarity is 0.
The predicate prove(Cla,Mat,Path,PathI,PathLim,Lem,PreS,VarS,Set,Proof) implements the axiom (line 10), the decomposition rule (lines 11–16), the reduction rule (lines 17–20, 24–26, 37–38), and the extension rule (lines 17–20, 28–49) of the non-clausal connection calculus in Fig. 1. (39) (40) (41) (42) (43) (44) (45) (46) (47) (48) (49) % start rule prove(Mat,PathLim,Set,[(Iˆ0)ˆV:Cla1|Proof]) :member((Iˆ0)ˆVˆVS:Cla,Mat), positiveC(Cla,Cla1), Cla1 \=!, prove(Cla1,Mat,[],[Iˆ0],PathLim,[],PreS,VarS, Set,Proof), append(VarS,VS,VarS1), domain_cond(VarS1), prefix_unify(PreS). prove(Mat,PathLim,Set,Proof) :retract(pathlim) -> ( member(comp(PathLim),Set) -> prove(Mat,1,[],Proof) ;
PathLim1 is PathLim+1, prove(Mat,PathLim1,Set,Proof) ) ; member(comp(_),Set) -> prove(Mat,1,[],Proof). % axiom prove([],_,_,_,_,_,[],[],_,[]). % decomposition rule prove([JˆK:Mat1|Cla],MI,Path,PI,PathLim,Lem,PreS,VarS, Set,Proof) :- !, member(Iˆ_ˆFV :Cla1,Mat1), prove(Cla1,MI,Path,[I,JˆK|PI],PathLim,Lem,PreS1,VarS1, Set,Proof1), prove(Cla,MI,Path,PI,PathLim,Lem,PreS2,VarS2,Set,Proof2), append(PreS2,PreS1,PreS), append(FV,VarS1,VarS3), append(VarS2,VarS3,VarS), append(Proof1,Proof2,Proof). % reduction and extension rules prove([Lit:Pre|Cla],MI,Path,PI,PathLim,Lem,PreS,VarS,Set,Proof) :
Proof=[[IˆV:[NegLit|ClaB1]|Proof1]|Proof2], \+ (member(LitC,[Lit:Pre|Cla]), member(LitP,Path), LitC==LitP), (-NegLit=Lit;-Lit=NegLit) -> ( member(LitL,Lem), Lit:Pre==LitL, PreS3=[], VarS3=[],
ClaB1=[], Proof1=[] ; member(NegL:PreN,Path), unify_with_occurs_check(NegL,NegLit), \+ \+ prefix_unify([Pre=PreN]), PreS3=[Pre=PreN], VarS3=[], ClaB1=[], Proof1=[] ; lit(NegLit:PreN,ClaB,Cla1,Grnd1), ( Grnd1=g -> true ; length(Path,K), K<PathLim -> true ;
\+ pathlim -> assert(pathlim), fail ), \+ \+ prefix_unify([Pre=PreN]), prove_ec(ClaB,Cla1,MI,PI,IˆVˆFV :ClaB1,MI1), prove(ClaB1,MI1,[Lit:Pre|Path],[I|PI],PathLim,Lem,PreS1,VarS1,
Set,Proof1), PreS3=[Pre=PreN|PreS1], append(VarS1,FV,VarS3) ), ( member(cut,Set) -> ! ; true ), prove(Cla,MI,Path,PI,PathLim,[Lit:Pre|Lem],PreS2,VarS2,Set,Proof2), append(PreS3,PreS2,PreS), append(VarS2,VarS3,VarS). % extension clause (e-clause) prove_ec((IˆK)ˆV:ClaB,IV:Cla,MI,PI,ClaB1,MI1) :append(MIA,[(IˆK1)ˆV1:Cla1|MIB],MI), length(PI,K), ( ClaB=[JˆK:[ClaB2]|_], member(JˆK1,PI), unify_with_occurs_check(V,V1), Cla=[_:[Cla2|_]|_], append(ClaD,[JˆK1:MI2|ClaE],Cla1), prove_ec(ClaB2,Cla2,MI2,PI,ClaB1,MI3), append(ClaD,[JˆK1:MI3|ClaE],Cla3), append(MIA,[(IˆK1)ˆV1:Cla3|MIB],MI1) ; (\+member(IˆK1,PI);V \==V1;V\=[]ˆ[] ) -> ClaB1=(IˆK)ˆV:ClaB, append(MIA,[IV:Cla|MIB],MI1) ).
Cla, Mat, and Path represent the subgoal clause C, the prefixed matrixM and the (active) P ath.
The indexed path PathI contains the indices of all clauses and matrices that contain literals of Path;
it is used for calculating extension clauses. The list Lem is used for the lemmata rule and contains
all literals that have been “solved” already [
nanoCoP-i uses additional optimization techniques that are already used in the classical connection
provers leanCoP [
append(Z,[X],Z1), tunify([V|S],Z1,T).
The following evaluations were conducted on a 3.4 GHz Xeon system with 4 GB of RAM running
Linux 3.13.0 and ECLiPSe Prolog 5.10. The CPU time limit was set to 10 seconds.
The ILTP problem library [
JProver [
JProver 11-2005 177 171 6 ileanTAP 1.17 251 248 3 ft (C) 1.23 260 258 2 — ileanCoP 1.2 — [nodef] [def] 636 652 566 572 70 80 —- nanoCoP-i 1.0 —[ ] [cut,comp(6)] 731 872 636 717 95 155
Again, nanoCoP-i proves more problem than both clausal translations of ileanCoP. The “full” version of ileanCoP1.2 proves 932 problems. Compared to ileanCoP [nodef], 92% of the nanoCoP-i proofs are on average 28% shorter; 7% of the proofs are larger, 1% have the same size. Compared to ileanCoP [def], 94% of the nanoCoP-i proofs are on average 34% shorter; 5% of the proofs are larger, 1% have the same size. 5
This paper introduces a non-clausal connection calculus for intuitionistic first-order logic andnanoCoP-i, a compact implementation of this calculus. Using prefixed non-clausal matrices, the proof search works directly on the original structure of the input formula; no translation steps to any clausal or other normal form are required. This combines the advantages of more natural non-clausal tableau or sequent provers with the goal-oriented efficiency of connection provers.
Even though the non-clausal inferences introduce a slight overhead, nanoCoP-i outperforms both clausal form translations of the ileanCoP core prover on the ILTP and the TPTP problem library. It is expected that the integration of strategy scheduling into nanoCoP-i will also outperform the “full” ileanCoP prover. More than 90% of the returned non-clausal proofs are on average about 30% shorter than their clausal counterparts.
Both, the standard translation as well as a definitional translation [
By considering the intuitionistic substitution, the returned connection proof can be translated into
an intuitionistic sequent proof [
In contrast to the calculus used in nanoCoP-i, the non-clausal connection calculus used in JProver [
Future work include the adaption of the non-clausal connection calculus and the nanoCoP-i prover to
other non-classical logics, such as modal or description logics, for which so far only clausal connection
calculi exist [