In recent years some papers have addressed the problem of the validity in Intuitionistic Propositional Logic and in some intermediate propositional logics using the approach proposed by Claessen and Rosén of reduction to Satisfiability Modulo Theories (SMT). This approach depends on an initial preprocessing phase that reduces the input formula in the intuitionistic language to an equivalent sequent in the language of clauses. In this work we present an extension of the clauses used by Claessen and Rosén that allows us to define a natural relationship between the semantics of the extended clauses and Kripke semantics. As an application, we show how Answer Set Programming can be used to check the intuitionistic validity of a formula and to generate Kripke countermodels for countersatisfiable formulas.
shown that there is a close connection between the intuit approach and the known prooftheoretic methods. Actually, the intuit decision procedure mimics a standard root-first proof search strategy for LJTSAT, a variant of Dyckhof’s calculus LJT [3] (alias G4ip). In [2], the intuit search procedure is rephrased so that, given a sequent , a formal derivation of in LJTSAT or a countermodel for is returned.
The intuit approach has been refined in [ 4] where the decision procedure has been redesigned; the obtained prover is called intuitR (intuit with Restart). Diferently from intuit, the intuitR procedure has a simple structure, consisting of two nested loops and its performances improve those of intuit. Finally, in [5, 6] the intuit approach is extended to some intermediate and non-classical logics.
Despite these significant improvements of the original intuit procedure, many aspects have not been fully investigated. Undoubtedly, a central aspect in the definition of intuit is related to the form of clauses, specifically the role of implication clauses. At first glance, it is not clear why such clauses are necessary and one may wonder if other clausal forms are possible, in order to get a clearer and more explicit semantic mapping, as well as more eficient clausification procedures. Moreover, in a more general sense, it is worth exploring whether there exist clausal forms that can be applied to other logics with Kripke-style semantics. For this reason, in this paper we introduce a diferent approach to clausification based on two phases.
In the first phase we translate a formula in a clausal form for intuitionistic logic based on the notion of IPL-clause. The IPL-clausification procedure translates a formula in an intuitionistically equivalent set of IPL-clauses. This is the only phase which introduces new propositional variables and hence the role of the new propositional variables can be studied in a purely intuitionistic setting.
In the second step we translate IPL-clauses in the classical setting using the notion of general clause. General clauses extend classical ones by introducing literals of the form ̸→ , where and are atoms and ̸→ is a new operator; intuitively, ̸→ corresponds to the intuitionistic negation of → . A general clause is a disjunction of general literals, where a general literal is either a classical literal of the form or ∼ or a literal of the form ̸→ ; note that general clauses not containing ̸→-literals are classical clauses. For general clauses we can define a semantics, we call realizability, based on sets of classical interpretations with minimum, which admit a natural translation in Kripke models. Such a semantics is the bridge to apply standard techniques for testing classical satisfiability to check IPL validity and to generate countermodels for non-valid formulas. Even if in this paper we only consider the case of intuitionistic logic, in principle the above approach can be also applied to other logics with a Kripke semantics, provided that we can define a clausal form for the logic and the relationship between the semantics of general clauses and the semantics of the logic at hand.
Here, as an application of our approach, following the ideas of [7], we tackle the problem of intuitionistic validity using a strategy based on model generation formalized in the Answer Set Programming (ASP) setting [8, 9]. To check the intuitionistic validity of a formula , we apply the clausification procedure to generate a sequent = Δ ⇒ , where Δ is a set of general clauses and is an atom, which is equivalent to . Then we define an ASP program Π such that an answer set of Π corresponds to a countermodel for (and hence a countermodel for ); if no answer set for Π exists, there is no countermodel for and this implies that is valid in IPL. The implementation, based on the Potassco tool Clingo [10], is available at https://github.com/cfiorentini/clausificationIPL.
Formulas, denoted by lowercase Greek letters, are built from an enumerable set of propositional variables , the constants ⊤, ⊥ and the connectives ∧, ∨, →; moreover, ¬ (intuitionistic negation) stands for → ⊥ and ↔ stands for ( → ) ∧ ( → ). We refer to the above language as the intuitionistic language to stress the fact that this is the language for which we provide an intuitionistic interpretation over Kripke models. In Sec. 4 we introduce general clauses, an extension of classical clauses; to define them, we use the classical connectives ∼ , | and the non-classical binary connective ̸→. Elements of the set ∪ {⊥, ⊤} are called atoms and are denoted by lowercase Roman letters, uppercase Greek letters denote sets of formulas. By we denote the set of propositional variables occurring in . The notation is extended to sets of formulas: Ω is the union of such that ∈ Ω; Ω,Ω′ and Ω, stand for Ω∪Ω′ and Ω∪{ } respectively.
A (classical) interpretation is a subset of , identifying the propositional variables assigned to true. By |= we mean that is true in . Let Ω be a set of formulas; by |= Ω we mean that |= for every ∈ Ω. Classical Propositional Logic (CPL) is the set of formulas true in every interpretation.
A (rooted) Kripke model [11] is a quadruple ⟨, ≤ , , ⟩ where is a finite and non-empty set (the set of worlds), ≤ is a reflexive and transitive binary relation over , the world (the root of ) is the minimum of w.r.t. ≤ , and (the valuation function) is a map from to 2 obeying the persistence condition: for every pair of worlds 1 and 2 of , 1 ≤ 2 implies (1) ⊆ (2). The valuation is extended to a forcing relation between worlds of and formulas as follows: , ⊩ if ∈ (), ∀ ∈ , ⊩ ⊤ , ⊮ ⊥ , ⊩ ∧ if , ⊩ and , ⊩ , ⊩ ∨ if , ⊩ or , ⊩ , ⊩ → if ∀′ ≥ , , ′ ⊩ implies , ′ ⊩ .
Note that, since ¬ stands for → ⊥, we have , ⊩ ¬ if ∀′ ≥ , , ′ ⊮ . Given a set of formulas Ω, by , ⊩ Ω we mean that , ⊩ for every ∈ Ω. A formula is valid in the model = ⟨, ≤ , , ⟩ if , ⊩ . Propositional Intuitionistic Logic (IPL) is the set of formulas valid in all Kripke models. Accordingly, if there is a model such that , ⊮ (where is the root of ), then is not IPL-valid; we call a countermodel for .
The intuitionistic consequence relation, denoted by |=i, is defined as follows ( Ω is a set of formulas, is a formula):
• Ω |=i if, for every model = ⟨, ≤ , , ⟩, if , ⊩ Ω then , ⊩ .
Note that is IPL-valid if |=i (namely, ∅ |=i ). The next lemma shows that the decision problem |=i can be reduced to the problem → |=i , with a new propositional variable.
Lemma 1 Let be a formula and ̸∈ . Then, |=i if → |=i . ⊤ ∧ ↦→ ⊤ ∨ ↦→ ⊤ ⊤ → ↦→
∧ ⊤ ↦→ ∨ ⊤ ↦→ ⊤ → ⊤ ↦→ ⊤ ⊥ ∧ ↦→ ⊥ ⊥ ∨ ↦→ ⊥ → ↦→ ⊤ ∧ ⊥ ↦→ ⊥ ∨ ⊥ ↦→
Proof. The proof that |=i implies
→ |=i is immediate. Conversely, let us assume
̸|=i . Then, there exists a Kripke model = ⟨, ≤ , , ⟩ such that , ⊮ . We define
the model ′ obtained from by modifying the valuation so that in ′ simulates the
forcing of in . Formally, ′ = ⟨, ≤ , , ′⟩ where: ′() = () ∪ {} if , ⊩ ;
′() = () ∖ {} if , ⊮ . One can easily check that, for every world in and every
formula , the following property holds: (
→ . Let ∈ be such that ′, ⊩ . By (
We introduce IPL-clauses, a clausal form for intuitionistic formulas, and a procedure ClauIPL to turn a simplified formula into an equivalent set of IPL-clauses.
An IPL-clause is defined by the following grammar: := ⊥ | 1 ∨ · · · ∨
| | ( 1 ∧ · · · ∧ | ( 1 ∧ · · · ∧ ∧ (1 → 1) ∧ · · · ∧ ∧ (1 → 1) ∧ · · · ∧ ( → ) ) → ⊥ ( → ) ) → (1 ∨ · · · ∨ ) ≥ 1, + ≥ 1
∈ , ∈ ∪ {⊥}, ∈ , ∈ We call non-classical the IPL-clauses containing at least two occurrences of →. We remark that IPL-clauses are a generalizations of the clauses introduced in [1]; indeed, in [1] only non-classical clauses of the form ( → ) → are admitted. To clausify a formula, we exploit the clausification procedure ClauIPL defined in Fig. 2 and discussed below. Given a simplified formula , ClauIPL computes a (possibly empty) set of IPL-clauses Θ which is equivalent to in the sense stated by the following theorem: Ω, |=i if Ω, ClauIPL( ) |=i .
Theorem 2 Let be a formula and let Ω ∪ { } be a set of formulas such that Ω, ⊆ . Then, Since |=i , as an immediate consequence of Th. 2 we get: Proposition 3 ClauIPL( ) |=i .
|=i , where is a simplified formula, to the problem Θ |=i , where Θ is a finite set of IPL-clauses and a propositional variable. Indeed, let be any simplified formula and let be a new propositional variable (namely, ̸∈ ). By Lemma 1, |=i if and only if → |=i . Let Θ = ClauIPL( → ); by Th. 2, → |=i if Θ |=i . Thus: ClauIPL( → ) |=i .
Theorem 4 Let be a simplified formula and ∈ such that ̸∈ . Then, |=i if
The clausification procedure
ClauIPL is defined in Fig. 2, by a case analysis on the input formula ; we stress that is assumed to be simplified, and this reduces the number of cases to consider. We write that ≡ 1 ∨ 2; for instance 0 → (1 ∧ (2 ∨ 3) ∧ 4) ≡ 0 → ((3 ∨ 2) ∧ 4 ∧ 1). permuting the order of conjuncts or disjuncts in subformulas of of the kind 1 ∧ 2 and
In the clausification process, we introduce new propositional variables to represent some of the subformulas of ; we write ˜ to denote the propositional variable associated with the subformula of . If = ⊤, then Θ is the empty set; if is an IPL-clause, then Θ is the set { }. Otherwise, ClauIPL( ) is defined by distinguishing some cases. One can easily check that, since is simplified, the list of cases is exhaustive; moreover, the cases do not overlap. In the computation of ClauIPL( ), we have to define the values of ˜ . Given , whenever ˜ is mentioned and ˜ has not been defined yet, a new propositional variable must be chosen (namely, does not occur in and in any of the formulas processed so far) and we set ˜ = . ′ if ′ can be obtained from by ⊥) → ⊥, where 1 = ∨ ¬. We get: Example 1 Let be the simplified formula ¬¬( ∨ ¬). Note that has the form ( 1 →
ClauIPL( ) ClauIPL(˜ 1 → 1) ClauIPL(˜¬ → ¬)
ClauIPL( ) = { (˜ 1 → ⊥) → ⊥ } ∪ ClauIPL(˜ 1 → 1) = { ˜ 1 → ( ∨ ˜¬) } ∪ ClauIPL(˜¬ → ¬) = ClauIPL((˜¬ ∧ ) → ⊥) = { (˜¬ ∧ ) → ⊥ } = { (˜ 1 → ⊥) → ⊥, ˜ 1 → ( ∨ ˜¬), (˜¬ ∧ ) → ⊥ } from and ˜ 1.
We point out that ˜ 1 can be any propositional variable diferent from and ˜¬ must be distinct ♢ of a logical operator ⊙ , denoted by wg(⊙ ) (⊙ ∈ { ∧ , ∨, → }) are defined as follows: Now we show that ClauIPL terminates. The size of a formula , denoted by | |, and of weight | | = ⎧ ⎨0
if ∈ ∪ {⊥, ⊤} ⎩| 1 | + | 2 | + wg(⊙ ) if = 1 ⊙ 2 wg(∧) = 1 wg(∨) = 3 wg(→) = 2 The weights of logical operators have been chosen so to guarantee the following property: ⊤ is an IPL-clause ∅ { } ClauIPL( 1) ∪ ClauIPL( 2) { 2 ∨ ˜ 1 ∨ · ·· ∨ ˜ } ∪ Θ1 ∪ · ·· ∪
Θ Θ = ClauIPL(˜ → ), ∈ {1, .. . ,} ClauIPL( 1 → 1) ∪ ClauIPL( 1 → 2) ClauIPL(( 1 ∧ 1) → 2) ClauIPL( 1 → ) ∪ ClauIPL( 2 → ) { (˜1 → ˜2) → ˜ } ∪ Θ1 ∪ Θ2 ∪ Θ3 ≡ ( 1 ∧ 1 ∧ · · · ∧
) → ( 2 ∨ 1 ∨ · ·· ∨ ) + ≥ 1 if 1 ∈ ∪ {⊥} otherwise if 2 ∈ ∪ {⊥} otherwise if ∈ ∪ {⊥} otherwise ˜1 = ˜2 = ˜ = Θ1 = Θ2 = {︃ 1 ˜ 1 2 ˜ 2 ˜
{︃ {︃ {︃ {︃ {︃ Θ3 = ∅ if ∈ ∪ {⊥} ∅ if 1 ∈ ∪ {⊥} ClauIPL(˜ 1 → 1) otherwise ∅ if 2 ∈ ∪ {⊥} ClauIPL( 2 → ˜ 2) otherwise
ClauIPL(˜ → ) otherwise { ( 1 ∧ ˜ 1 ∧ ·· · ∧ ˜
) → ( 2 ∨ ˜ 1 ∨ ·· · ∨ ˜ ) } ∪Θ′1 ∪ · ·· ∪ Θ′ ∪ Θ′1′ ∪ · ·· ∪
Θ′′ Θ′ = ClauIPL( → ˜ ), ∈ {1, .. . ,} Θ′′ = ClauIPL(˜ → ), ∈ {1, .. . ,} 1 = 1 ∧ · ·· ∧ ∧ (1 → 1) ∧ · ·· ∧
( → ) 2 = 1 ∨ · ·· ∨ 1, . . ., , 1, . . ., are non-atomic formulas
Lemma 5 Let be a simplified formula and let ClauIPL( ′) be any of the recursive calls invoked by ClauIPL( ) (see Fig. 2). Then, | ′ |<| |.
Proof. The assertion can be easily proved by a case analysis. As an example, let ≡ ( 1 ∧ 1 ∧ · · · ∧
) → ( 2 ∨ 1 ∨ · · · ∨ recursive calls in the definition of ClauIPL( ). We have two possible cases: ) (last case in Fig. 2), and let ClauIPL( ′) be any of the (a) ′ = → ˜ , where ∈ {1, . . . , }; (b) ′ = ˜ → , where ∈ {1, . . . , }.
In Case (a), the formula contains at least one of the displayed occurrences of ∧, thus | |≥| | +1 + 2 (the latter is the weight of the main operator → of ). On the other hand | ′ |=| | +2, and this proves that | ′ |<| |. The discussion of Case (b) is similar. □ By Lemma 5, it immediately follows that ClauIPL is terminating. Finally, we remark that the procedure ClauIPL satisfies Th. 2 (see the proof in the Appendix available at https://github. com/cfiorentini/clausificationIPL).
We introduce general clauses, an extension of classical clauses that can be used to capture non-classical logics, such as intermediate and modal logics. Moreover, we exhibit a one-to-one translation of IPL-clauses into general clauses.
Classical clauses are built over propositional variables, using the the operators ∼ (classical negation) and | (classical disjunction). A classical literal is a formula of the kind or ∼ , where is a propositional variable. A classical clause is a set of classical literals {1, . . . , }, denoted by 1 | . . . | ; if = 0, then is the empty clause, denoted by □ . We point out that the order of the literals occurring in a clause is immaterial; for instance, |∼ and ∼ | denote the same clause. Given two classical clauses = 1 | . . . | and ′ = 1′ | . . . | ′, where ≥ 0 and ≥ 0, by | ′ we denote the classical clause 1 | . . . | | 1′ | . . . | ′. Given a classical interpretation and a classical clause , the relation |= is defined as follows: ̸|= □ |= if ∈ |=∼ if ̸∈ |= 1 | . . . | if ∃ : |= .
We extend classical clauses by introducing the binary operator ̸→, which is a sort of negation of intuitionistic implication. A general literal is either a classical literal or a ̸→-formula of the kind ̸→ , where ∈ and ∈ ∪ {⊥}. A general clause is a set of general literals {1, . . . , }, denoted by 1 | . . . | ; we stress that the order of the literals is immaterial. We call non-classical a general clause containing at least one occurrence of ̸→.
Semantics of general clauses. We introduce a semantics for general clauses, we call realizability semantics, based on sets of classical interpretations, that plays a crucial role to establish the relationship between general clauses and IPL-clauses.
Let be a nonempty set of classical interpretations; we define the realizability relations ◁0 and ◁ between the interpretations in and general clauses. Given an interpretation in and a general clause = | 1 ̸→ 1 | . . . | ̸→ , where is a classical clause and ≥ 0, the relations ◁0 and ◁ are defined as follows: • ◁0 if |= , or there is ′ ∈ and ∈ {1, . . . , } such that ⊆ ′ and ′ |= and ′ ̸|= .
• ◁ if, for every ′ ∈ , if ⊆ ′ then ′ ◁0 . Ψ( ) = ⎪⎧□ ⎪ ⎪⎪⎪⎪1 | . . . | ⎪ ⎪ ⎪ ⎪⎨ ∼ 1 | . . . |∼ | 1 ̸→ 1 | . . .
. . . | ̸→ ⎪ ⎪ ⎪ ⎪ ⎪⎪⎪ 1 | . . . | |∼ 1 | . . . ⎪ ⎪ ⎪ ⎩ . . . |∼ | 1 ̸→ 1 | . . . | ̸→ if = ⊥ if = 1 ∨ · · · ∨ if = ( 1 ∧ · · · ∧ ∧ (1 → 1) ∧ . . .
· · · ∧ ( → ) ) → ⊥ if = ( 1 ∧ · · · ∧ ∧ (1 → 1) ∧ . . .
· · · ∧ ( → ) ) → (1 ∨ · · · ∨ ) = 1 | . . . | |∼ 1 | . . . |∼ | 1 ̸→ 1 | . . . | ̸→ ⎧ ⎪⊥ ⎪ ⎪ ⎪ ⎪⎪⎪¬(1 ∧ · · · ∧ ) ⎪ ⎪⎪⎪⎪1 ∨ · · · ∨ Φ( ) = ⎨
( 1 ∧ · · · ∧ ) → (1 ∨ · · · ∨ ) ⎪⎪⎪⎪⎪¬(1 ∧ · · · ∧ ∧ (1 → 1) ∧ · · · ∧ ( → )) ⎪ ⎪ ⎪⎪ ( 1 ∧ · · · ∧ ∧ (1 → 1) ∧ · · · ∧ ( → ) ) → ⎪ ⎪⎪⎩ (1 ∨ · · · ∨ ) if = □ ( = = = 0) if = = 0 and > 0 if > 0 and = = 0 if > 0, > 0 and = 0 if = 0, > 0 and > 0 otherwise
In general ◁0 is not monotone w.r.t. the inclusion relation ⊆ . For instance, let = { ∅, {} }; 0 0 then ∅◁ ∼ and ∅ ⊆ { }, but {} ⋫ ∼ . Instead, ◁ is monotone by definition. Given a set of general clauses Δ, by ◁0 Δ (resp., ◁ Δ) we mean ◁0 (resp., ◁ ) for every in Δ.
Let be a finite set of classical interpretations; the minimum of is the minimum element of with respect to the subset relation ⊆ (namely, ⊆ for every ∈ ). Let be a ifnite set of interpretations with minimum . By ( ) we denote the structure ⟨, ≤ , , ⟩ where: ≤ coincides with the subset relation ⊆ ; is the identity map. It is easy to check that ( ) is a Kripke model such that ( ), ⊩ if ∈ .
From IPL-clauses to general clauses. In Fig. 3 we display the bijective map Ψ between IPLclauses and general clauses and its inverse Φ; note that non-classical IPL-clauses are mapped to non-classical general clauses, and vice versa. We investigate the relationship between the semantics of IPL-clauses (Kripke models) and the semantics of general clauses (realizability). The next proposition shows that the forcing relation on ( ) mirrors the realizability relation ◁ . Proposition 6 Let be a general clause, let be a set of classical interpretations having minimum element. For every in , ◁ if ( ), ⊩ Φ( ).
Proof. We only consider the most general case where: Ψ( ) =
1 | . . . | |∼ 1 | . . . |∼ | 1 ̸→ 1 | . . . | ̸→ = ( 1 ∧ · · · ∧ ∧ (1 → 1) ∧ . . . ( → ) ) → (1 ∨ · · · ∨ ) ⏞ ⏟ ⏞ ⏟ ⏟
⏞ where ≥ 1, ≥ 1, ≥ 1 Let us assume ◁ ; we show ⊩
Φ( ) 1, namely ⊩ the height of in ( ), defined as the length of the longest path from of ( ) w.r.t. ≤ . We start by considering the base case h() = 0 namely, is a maximal world in ( ) w.r.t. ≤ ; we point out that is maximal in w.r.t. ⊆ . Let us assume ⊩ , we prove ⊩ . We have: ⊩ , for every ∈ {1, . . . , } and ⊮ or ⊩ , for every ∈ {1, . . . , }. This implies that: |= , for every ∈ {1, . . . , } and ̸|= or |= , for every ∈ {1, . . . , }. Since ◁0 and is maximal in w.r.t. ⊆ , there exists ∈ {1, . . . , } ⊩ such that |= . It follows that ⊩ , which implies ⊩ . This concludes the proof of → in the base case. Now, let h() > 0 and let ′ ∈ such that ≤ ′ and ′ ⊩ ; → . We proceed by induction on to a maximal world we show that ′ ⊩ . If < ′, then ⊂ holds that ′ ◁ ; by the induction hypothesis, we get ′ ⊩ ′ and h(′) < h(). Since ◁ is monotone, it → , and this implies ′ ⊩ .
On the other hand, if ′ = then ⊩ , hence: ⊩ , for every ∈ {1, . . . , } and ′ ⊮ or ′ ⊩ , for every ′ ∈ s.t. ≤ ′ and every ∈ {1, . . . , }. This implies that: |= , for every ∈ {1, . . . , } and ′ ̸|= or ′ |= , for every ′ ∈ s.t. ≤ ∈ {1, . . . , }. Since ◁0 , there is ∈ {1, . . . , } such that |= , hence ⊩ . We have ′ and every Φ( ); accordingly, ◁ implies ⊩ Φ( ). get ◁0 . Let us assume ̸|= ; then: |= , for every ∈ {1, . . . , } and ̸|= , for every ∈ {1, . . . , }. This implies that: ⊩ , for every ∈ {1, . . . , } and ⊮ , for every ∈ {1, . . . , }. Since ⊩
→ and ⊮ , it holds that ⊮ ; hence there is ∈ {1, . . . , }
such that ⊮ → . It follows that there is ′ ∈ such that ≤
′ ⊮ , hence ⊆ ′ and ′ |= and ′ ̸|= . We get ◁0 , and this proves point (
→ , namely ⊩
(
According with Th. 4, the problem of IPL-validity of a formula can be reduced to the decidability of Θ |=i , where is a propositional variable and Θ is a set of IPL-clauses; in the rest of the paper, we focus on the problem Θ |=i . , ⊩
We can show that Θ ̸|=i by exhibiting a Kripke (counter)model = ⟨, ≤ , , ⟩ such that Θ and , ⊮ . By Prop. 6, this is equivalent to search for a set of interpretations having minimum element such that ◁ Ψ(Θ) and ⋫ Ψ(), namely ̸∈ . To formalize 1Here and below we leave understood the model ( ).
3 : , , , ,
0 : 1 : , ,
2 : , , Δ Φ(Δ) = = { |∼ , |∼ , | , | ̸→ , | ̸→ , ∼ | ̸→ ⊥ } { → , → , ∨ , ( → ) → , ( → ) → , ¬( ∧ ¬) } 0 ◁ Δ, ( ), 0 ⊩ Φ(Δ) the latter problem, we introduce the notions of sequent and countermodel. A sequent Δ ⇒ is a pair where Δ is a set of general clauses and is an atom. A countermodel for Δ ⇒ is a set of classical interpretations with minimum such that ◁ Δ and ̸∈ . A sequent is countersatisfiable if there exists a countermodel for .
Example 2 In Fig. 4 we define a sequent = Δ ⇒ and we show a countermodel for . The countermodel consists of the classical interpretations 0, 1, 2, 3; for each interpretation we list the propositional variables in ; thick lines represent the inclusion relation2. One can easily check that 0 ◁ Δ and ̸∈ 0; accordingly, is countermodel for . It is easy to prove that there are not countermodels for having less than four interpretations. The same picture also represents the Kripke model ( ) = ⟨, ≤ , 0, ⟩; in this case each must be understood as a world of the model (with the list of variables in ()) and thick lines denote the relation ≤ . One can easily check that 0 ⊩ Φ(Δ) and 0 ⊮ , hence Φ(Δ) ̸|=i . ♢
The crucial property of countersatisfiable sequents is stated in the next proposition: Proposition 7 A sequent = Δ ⇒ is countersatisfiable if Φ(Δ) ̸|=i .
Proof. Let be countersatisfiable, let be a countermodel for and the minimum of . Since ◁ Δ, by Prop. 6 we get ( ), ⊩ Φ(Δ); since ̸∈ , it also holds that ( ), ⊮ . Accordingly, the Kripke model ( ) witnesses that Φ(Δ) ̸|=i .
Conversely, let us assume Φ(Δ) ̸|=i and let be a Kripke model such that , ⊩ Φ(Δ)
and , ⊮ , with the root of . One can easily define a set of interpretations such
that the model is isomorphic to the model ( ); note that the root of is mapped to the
minimum of . By Prop. 6, we get ◁ Δ; since ̸∈ , is a countermodel for , hence
is countersatisfiable. □
2Redundant lines are omitted, e.g. self-loops, the line connecting 0 with 3.
atomSet( w(0..1, 0..1, 0..1, 0..1, 0..1) ). % shorthand for:
% atomSet(w(0,0,0,0,0)). atomSet(w(
We describe an ASP program Π that, given a sequent , searches for a countermodel for . According with the ASP paradigm (see e.g. [12]), Π is a Prolog-like program consisting of two components I and Gen. The component I encodes the instance of the problem determined by the input sequent ; the component Gen implements the model generator. A solution to Π = Gen ∪ I , called answer set, corresponds to a countermodel for ; if Π has no answers, then no countermodel for exists. We exploit the ASP solver clingo [13]. The clause language is encoded as follows: atoms are represented by Clingo constants, with ⊥ denoted by false; atoms representing propositional variables are indexed by natural numbers using the idxOfAtom/2 predicate. General literals of the kind ∼ and ̸→ are encoded using the function symbols neg/1 and negImp/2 respectively. We have to introduce names for classical clauses and general (non-classical) clauses by using the predicates clClause/1 and genClause/1. To define the literals belonging to a general clause (either classical or not), we use the predicate litOf/2. The right atom of a sequent is specified by the predicate rightAtom/1. In Fig. 5 we display the encoding of the sequent defined in Fig. 4.
Countermodels are sets of worlds, and each world is represented by a set of propositional
variables (atomSet). Let be the number of distinct propositional variables occurring in ;
an atomSet is represented by a term of the form w(0, ..., − 1), where each argument is
a boolean value, namely = 0 or = 1. Let be the atom having index , as set by the
predicate idxOfAtom/2; the term w(0, ..., − 1) represents the set of such that = 1. For
instance, the encoding in Fig. 5 yields the following representation:
w(0, 0, 0, 0, 0) ↦→ ∅
w(
w(
The predicate atomSet/1 enumerates all the atomSet’s; since the arity of w depends on the input sequent , the definition of atomSet/1 (as well as the definition of other auxiliary predicates) must be supplied by I (see Fig. 5).
The countermodel generation algorithm is encoded in the component Gen. The classical validity of a literal in an atomSet (seen as a classical interpretation) is computed by the predicate satisfies_lit/2 defined by the following clauses (the auxiliary predicate atom/1 specifies the defined atoms, member/2 implements the membership relation on atomSet’s): satisfies_lit(W,Atm) :- atomSet(W), atom(Atm), member(Atm,W). satisfies_lit(W,neg(Atm)) :- atomSet(W), atom(Atm), not member(Atm,W). The predicate satisfies_clClause/2 checks whether an atomSet satisfies a classical clause , namely: satisfies all the literals in ; such a condition is expressed by a cardinality constraint built over the aggregate #count. We also introduce the auxiliary predicate satisfies_all_clClauses/1 to check whether an atomSet satisfies all the classical clauses. satisfies_clClause(W,C) :- atomSet(W),clClause(C),
#count{ Lit : litOf(Lit,C), satisfies_lit(W,Lit) } > 0. satisfies_all_clClauses(W) :- atomSet(W),
#count{ C : clClause(C), not satisfies_clClause(W,C) } = 0.
The generator has to guess a set a worlds, where a world is an atomSet satisfying all the classical clauses, and to check if the set of selected worlds is a countermodel for the input sequent . Worlds are denoted by the predicate world/1 and are generated by the following rule, which selects zero or more worlds out of the atomSet’s satisfying all the classical clauses: { world(W) : atomSet(W), satisfies_all_clClauses(W) }.
The set of selected worlds is a candidate solution, which must be checked by introducing suitable constraints. The predicate realizes_genLit/2 encodes the realizability relation ◁0 between worlds and general clauses; below we only display the non-trivial case of the definition ( leq/2 encodes the subset relations between worlds). realizes_genLit( W, negImp(Atm1,Atm2) ) :- world(W), atom(Atm1), atom(Atm2), #count{ W1 : world(W1), leq(W,W1), member(Atm1,W1) , not member(Atm2, W1) } > 0. The predicate realizes_genClause/2 encodes the realizability relation between worlds and general clauses, and is similar to satisfies_clClause/2. To rule out solutions where worlds do no satisfy all the general clauses, we introduce the following constraint: :- world(W), #count{ C : genClause(C), not realizes_genClause(W,C) } > 0. % it is false that W is a world and the number of C s.t. W does not realize C is > 0 We force that exactly one world, denoted by root/1, does not contain the right atom of the input sequent; we also require that the root world is the minimum w.r.t. subset relation (this rules out dead worlds). :- rightAtom(G) , #count{ W : world(W), not member(G,W) } != 1. % it is false that G is the rightAtom and the number of W non containing G is != 1 root(W) :- world(W), rightAtom(G), not member(G,W). :- root(W0), world(W1), not leq(W0,W1).
Let us consider the program Π = Gen ∪ I . If is a solution to Π (answer set), then the set of worlds in is a countermodel for . Conversely, if Π has no solution, then there is no countermodel for . We remark that we can ask clingo to search for a minimal countermodel with respect to the number of worlds, by exploiting the #minimize feature: numberOfWorlds(N) :- #count{ W : world(W) } = N. % N is the number of worlds #minimize { N : numberOfWorlds(N) }.
In our implementation, the source file generator.lp encodes the component Gen, while the
#minimize statement is set apart in the file minimize.lp. Assuming that the component I
is encoded by sigma.lp, we can issue the commands :
clingo generator.lp sigma.lp % (
0 = w(
We can use Π to decide IPL-validity. Indeed, let be a simplified formula and let be the sequent Ψ(Θ) ⇒ , where ̸∈ and Θ = ClauIPL( → ). If Π has no answer, then the sequent is not countersatisfiable; by Prop. 7 it follows that Θ |=i and, by Th. 4, we conclude |=i . Conversely, let us assume that Π has a solution and let be the set of worlds in one of the computed answer set; then is a countermodel for , thus ◁ Ψ(Θ) and ̸∈ , where is the minimum of . Let us consider the Kripke model ( ); by Prop. 6 we get ( ), ⊩ Θ and ( ), ⊮ . Since Θ |=i → (see Prop. 3), it follows that ( ), ⊩ → , thus ( ), ⊮ . We conclude that is not IPL-valid and ( ) is a countermodel for . Note that this approach presents an odd asymmetry: if is not IPL-valid, we get a concrete certificate of it, namely a countermodel for ; on the contrary, if is IPL-valid, we gain no evidence of it. We leave as future work the investigation of a more informative procedure. Example 4 Let be the formula ( → ) ∨ ( → ) and let Θ = ClauIPL( → ). We have: Θ = ClauIPL(( → ) → ) ∪ ClauIPL(( → ) → ) = { ( → ) → , ( → ) → ) } = { | ̸→ , | ̸→ } 1 : ,
2 : ,
0
Let = Ψ(Θ) ⇒ and let be encoded by assigning the indexes 0, 1, 2 to a, b, g respectively.
The program Π generates a minimum countermodel for consisting of the worlds 0 =
w(0, 0, 0), 1 = w(
In this paper we have presented a new approach to clausification for Intuitionistic Propositional Logic which difers from the one used in [ 1, 2, 4, 5, 6] and it is based on two phases. The first phase provides a clausification in the pure intuitionistic setting and this allows us to clarify the role of the propositional variables introduced by the clausification procedure. The second phase translates the intuitionistic clauses in the classical setting exploiting the notion of general clause. The realizability semantics of general clauses provides a natural bridge with the Kripke semantics of intuitionistic clauses.
As a future work, we aim to implement a prover for IPL exploiting the approach based on SMT along the lines of [1, 2, 4, 5, 6]. Moreover, we aim to apply our approach to other non-classical logics with Kripke semantics such as modal logics.
As for the application we have presented in this paper, we aim to investigate the role that intuitionistic simplifications, such as the ones defined in [ 14], can play in the reduction of the size of the models generated by the ASP program. [5] C. Fiorentini, M. Ferrari, SAT-based proof search in intermediate propositional logics, in: J. Blanchette, L. Kovács, D. Pattinson (Eds.), IJCAR, volume 13385 of LNCS, Springer, 2022, pp. 57–74. [6] R. Goré, C. Kikkert, CEGAR-tableaux: Improved modal satisfiability via modal clauselearning and SAT, in: A. Das, S. Negri (Eds.), TABLEAUX 2021, volume 12842 of LNCS, Springer, Cham, 2021, pp. 74–91. [7] C. Fiorentini, An ASP Approach to Generate Minimal Countermodels in Intuitionistic
Propositional Logic, in: S. Kraus (Ed.), IJCAI, ijcai.org, 2019, pp. 1675–1681. [8] C. Baral, Knowledge Representation, Reasoning and Declarative Problem Solving, Cambridge University Press, 2010. [9] E. Dantsin, T. Eiter, G. Gottlob, A. Voronkov, Complexity and expressive power of logic programming, ACM Comput. Surv. 33 (2001) 374–425. [10] M. Gebser, R. Kaminski, B. Kaufmann, T. Schaub, Answer Set Solving in Practice, Synthesis Lectures on Artificial Intelligence and Machine Learning, Morgan & Claypool Publishers, 2012. [11] A. V. Chagrov, M. Zakharyaschev, Modal Logic, volume 35 of Oxford logic guides, Oxford
University Press, 1997. [12] C. Baral, Knowledge Representation, Reasoning and Declarative Problem Solving, Cambridge University Press, 2010. [13] M. Gebser, R. Kaminsk, B. Kaufmann, T. Schaub, Answer Set Solving in Practice, Synthesis Lectures on Artificial Intelligence and Machine Learning, Morgan and Claypool Publishers, 2012. [14] M. Ferrari, C. Fiorentini, G. Fiorino, Simplification Rules for Intuitionistic Propositional Tableaux, ACM Trans. Comput. Log. 13 (2012) 14:1–14:23.