=Paper=
{{Paper
|id=Vol-3428/paper15
|storemode=property
|title=A New Approach to Clausification for Intuitionistic Propositional Logic
|pdfUrl=https://ceur-ws.org/Vol-3428/paper15.pdf
|volume=Vol-3428
|authors=Camillo Fiorentini,Mauro Ferrari
|dblpUrl=https://dblp.org/rec/conf/cilc/Fiorentini023
}}
==A New Approach to Clausification for Intuitionistic Propositional Logic==
https://ceur-ws.org/Vol-3428/paper15.pdf
A New Approach to Clausification for Intuitionistic
Propositional Logic
Camillo Fiorentini1 , Mauro Ferrari2
1
Dep. of Computer Science, Università degli Studi di Milano, Italy
2
Dep. of Theoretical and Applied Sciences, Università degli Studi dell’Insubria, Italy
Abstract
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 pre-
processing 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.
Keywords
Intuitionistic Propositional Logic, countermodels construction, Answer Set Programming.
1. Introduction
In [1] Claessen and Rosén have introduced intuit, a decision procedure for Intuitionistic
Propositional Logic (IPL) that exploits advanced techniques in automated theorem proving;
actually, the decision problem is formalized as a Satisfiability Modulo Theories (SMT) search
procedure, where the bulk of the computation is performed by an incremental SAT-solver.
This approach requires a pre-processing phase to reduce the input formula to a semantically
equivalent sequent Δ ⇒ 𝑔, where Δ is a set of clauses and 𝑔 an atom. To capture IPL semantics,
two
⋀︀ kinds⋁︀of clauses are used: flat clauses and implication clauses. The former have the form
𝐴1 → 𝐴2 , where 𝐴1 and 𝐴2 are sets of atoms and are understood as classical clauses.
The latter have the form (𝑎 → 𝑏) → 𝑐, where 𝑎, 𝑏, 𝑐 are atoms and → is the intuitionistic
implication. In the SMT approach, implication clauses are part of the theory of the SMT search
procedure. The sequent 𝜎 = Δ ⇒ 𝑔 obtained by clausifying an input formula 𝛼 enjoys some
relevant properties: first of all, 𝛼 is valid in IPL if and only if the sequent 𝜎 is provable in IPL.
Secondly, clausification preserves countermodels: if 𝒦 is a countermodel for 𝜎 (namely, 𝒦 is a
Kripke model such that at its root all the formulas in Δ are forced and 𝑔 is not forced), then 𝒦
is a countermodel for 𝛼 as well (𝛼 is not forced at the root of 𝒦).
The proof-theoretical counterpart of the above approach has been studied in [2] where it is
CILC’23: 38th Italian Conference on Computational Logic, June 21–23, 2023, Udine, Italy
$ fiorentini@di.unimi.it (C. Fiorentini); mauro.ferrari@uninsubria.it (M. Ferrari)
0000-0003-2152-7488 (C. Fiorentini); 0000-0002-7904-1125 (M. Ferrari)
© 2023 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
CEUR
Workshop
Proceedings
http://ceur-ws.org
ISSN 1613-0073
CEUR Workshop Proceedings (CEUR-WS.org)
1
shown that there is a close connection between the intuit approach and the known proof-
theoretic methods. Actually, the intuit decision procedure mimics a standard root-first proof
search strategy for LJTSAT , a variant of Dyckhoff’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 re-
designed; the obtained prover is called intuitR (intuit with Restart). Differently 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 efficient 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 different 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.
2. Basic Definitions
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:
𝒦, 𝑤 ⊩ 𝑝 iff 𝑝 ∈ 𝜗(𝑤), ∀𝑝 ∈ 𝒱 𝒦, 𝑤 ⊩ ⊤ 𝒦, 𝑤 ⊮ ⊥
𝒦, 𝑤 ⊩ 𝛼 ∧ 𝛽 iff 𝒦, 𝑤 ⊩ 𝛼 and 𝒦, 𝑤 ⊩ 𝛽 𝒦, 𝑤 ⊩ 𝛼 ∨ 𝛽 iff 𝒦, 𝑤 ⊩ 𝛼 or 𝒦, 𝑤 ⊩ 𝛽
𝒦, 𝑤 ⊩ 𝛼 → 𝛽 iff ∀𝑤′ ≥ 𝑤, 𝒦, 𝑤′ ⊩ 𝛼 implies 𝒦, 𝑤′ ⊩ 𝛽.
Note that, since ¬𝛼 stands for 𝛼 → ⊥, we have 𝒦, 𝑤 ⊩ ¬𝛼 iff ∀𝑤′ ≥ 𝑤, 𝒦, 𝑤′ ⊮ 𝛼. Given a
set of formulas Ω, by 𝒦, 𝑤 ⊩ Ω we mean that 𝒦, 𝑤 ⊩ 𝛼 for every 𝛼 ∈ Ω. A formula 𝛼 is valid
in the model 𝒦 = ⟨𝑊, ≤, 𝑟, 𝜗⟩ iff 𝒦, 𝑟 ⊩ 𝛼. 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 𝛼 iff, for every model 𝒦 = ⟨𝑊, ≤, 𝑟, 𝜗⟩, if 𝒦, 𝑟 ⊩ Ω then 𝒦, 𝑟 ⊩ 𝛼.
Note that 𝛼 is IPL-valid iff |=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 𝛼 iff 𝛼 → 𝑔 |=i 𝑔.
⊤ ∧ 𝛼 ↦→ 𝛼 𝛼 ∧ ⊤ ↦→ 𝛼 ⊥ ∧ 𝛼 ↦→ ⊥ 𝛼 ∧ ⊥ ↦→ ⊥
⊤ ∨ 𝛼 ↦→ ⊤ 𝛼 ∨ ⊤ ↦→ ⊤ ⊥ ∨ 𝛼 ↦→ 𝛼 𝛼 ∨ ⊥ ↦→ 𝛼
⊤ → 𝛼 ↦→ 𝛼 𝛼 → ⊤ ↦→ ⊤ ⊥ → 𝛼 ↦→ ⊤
Figure 1: Boolean reductions.
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: (1) if 𝑔 ̸∈ 𝒱𝛽 , then 𝒦′ , 𝑤 ⊩ 𝛽 iff 𝒦, 𝑤 ⊩ 𝛽. We show
that 𝒦′ , 𝑟 ⊩ 𝛼 → 𝑔. Let 𝑤 ∈ 𝑊 be such that 𝒦′ , 𝑤 ⊩ 𝛼. By (1), it holds that 𝒦, 𝑤 ⊩ 𝛼; by
definition of 𝜗′ we get 𝒦′ , 𝑤 ⊩ 𝑔; this shows that 𝒦′ , 𝑟 ⊩ 𝛼 → 𝑔. Since 𝒦′ , 𝑟 ⊩ 𝛼 → 𝑔 and
𝒦′ , 𝑟 ⊮ 𝑔 (indeed, 𝒦, 𝑟 ⊮ 𝛼), the model 𝒦′ ascertains that 𝛼 → 𝑔 ̸|=i 𝑔. □
To streamline the presentation, we only consider simplified formulas. Formally, a formula 𝛼 is
simplified if none of the boolean reductions in Fig. 1 can be applied to subformulas of 𝛼. We
stress that, given a formula 𝛽, by repeatedly applying such reductions, we eventually get a
simplified formula 𝛼; moreover, since each rewriting step preserves intuitionistic validity, it
holds that |=i 𝛼 ↔ 𝛽.
3. Clauses for IPL
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:
Theorem 2 Let 𝛼 be a formula and let Ω ∪ {𝛽} be a set of formulas such that 𝒱Ω,𝛽 ⊆ 𝒱𝛼 . Then,
Ω, 𝛼 |=i 𝛽 iff Ω, ClauIPL(𝛼) |=i 𝛽.
Since 𝛼 |=i 𝛼, as an immediate consequence of Th. 2 we get:
Proposition 3 ClauIPL(𝛼) |=i 𝛼.
Clausification allows us to reduce the validity problem |=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 𝑔 iff Θ |=i 𝑔. Thus:
Theorem 4 Let 𝛼 be a simplified formula and 𝑔 ∈ 𝒱 such that 𝑔 ̸∈ 𝒱𝛼 . Then, |=i 𝛼 iff
ClauIPL(𝛼 → 𝑔) |=i 𝑔.
IPL-clausification 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 𝛼 ≡ 𝛼′ iff 𝛼′ can be obtained from 𝛼 by
permuting the order of conjuncts or disjuncts in subformulas of 𝛼 of the kind 𝛽1 ∧ 𝛽2 and
𝛽1 ∨ 𝛽2 ; for instance 𝑝0 → (𝑝1 ∧ (𝑝2 ∨ 𝑝3 ) ∧ 𝑝4 ) ≡ 𝑝0 → ((𝑝3 ∨ 𝑝2 ) ∧ 𝑝4 ∧ 𝑝1 ).
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 𝑝 ˜𝛿 = 𝑞.
Example 1 Let 𝛼 be the simplified formula ¬¬(𝑎 ∨ ¬𝑎). Note that 𝛼 has the form (𝛼1 →
⊥) → ⊥, where 𝛼1 = 𝑎 ∨ ¬𝑎. We get:
ClauIPL(𝛼) = { (𝑝
˜𝛼1 → ⊥) → ⊥ } ∪ ClauIPL(𝑝
˜ 𝛼1 → 𝛼 1 )
˜𝛼1 → 𝛼1 )
ClauIPL(𝑝 = {𝑝
˜𝛼1 → (𝑎 ∨ 𝑝
˜¬𝑎 ) } ∪ ClauIPL(𝑝
˜¬𝑎 → ¬𝑎)
˜¬𝑎 → ¬𝑎)
ClauIPL(𝑝 ˜¬𝑎 ∧ 𝑎) → ⊥) = { (𝑝
= ClauIPL((𝑝 ˜¬𝑎 ∧ 𝑎) → ⊥ }
ClauIPL(𝛼) = { (𝑝
˜𝛼1 → ⊥) → ⊥, 𝑝
˜𝛼1 → (𝑎 ∨ 𝑝 ˜¬𝑎 ∧ 𝑎) → ⊥ }
˜¬𝑎 ), (𝑝
We point out that 𝑝
˜𝛼1 can be any propositional variable different from 𝑎 and 𝑝
˜¬𝑎 must be distinct
from 𝑎 and 𝑝
˜ 𝛼1 . ♢
Now we show that ClauIPL terminates. The size of a formula 𝛼, denoted by | 𝛼 |, and of weight
of a logical operator ⊙, denoted by wg(⊙) (⊙ ∈ { ∧, ∨, → }) are defined as follows:
⎧
⎨0 if 𝛼 ∈ 𝒱 ∪ {⊥, ⊤} wg(∧) = 1
|𝛼| = wg(∨) = 3
⎩| 𝛼 | + | 𝛼 | + wg(⊙) if 𝛼 = 𝛼 ⊙ 𝛼
1 2 1 2 wg(→) = 2
The weights of logical operators have been chosen so to guarantee the following property:
𝛼 Θ
⊤ ∅
𝛼 is an IPL-clause {𝛼}
𝛼1 ∧ 𝛼2 ClauIPL(𝛼1 ) ∪ ClauIPL(𝛼2 )
𝛼 ≡ 𝜂 2 ∨ 𝛽1 ∨ · · · ∨ 𝛽𝑦 { 𝜂2 ∨ 𝑝
˜𝛽1 ∨ · · · ∨ 𝑝
˜ 𝛽 𝑦 } ∪ Θ1 ∪ · · · ∪ Θ𝑦
𝑦≥1 ˜𝛽𝑗 → 𝛽𝑗 ), 𝑗 ∈ {1, . . . , 𝑦}
Θ𝑗 = ClauIPL(𝑝
𝛼1 → (𝛽1 ∧ 𝛽2 ) ClauIPL(𝛼1 → 𝛽1 ) ∪ ClauIPL(𝛼1 → 𝛽2 )
𝛼1 → (𝛽1 → 𝛽2 ) ClauIPL((𝛼1 ∧ 𝛽1 ) → 𝛽2 )
(𝛼1 ∨ 𝛼2 ) → 𝛽 ClauIPL(𝛼1 → 𝛽) ∪ ClauIPL(𝛼2 → 𝛽)
(𝛼1 → 𝛼2 ) → 𝛽
{ (𝛼
˜1 → 𝛼
˜ 2) → 𝛽 ˜ } ∪ Θ1 ∪ Θ2 ∪ Θ3
{︃
𝛼1 if 𝛼1 ∈ 𝒱 ∪ {⊥}
𝛼
˜1 =
𝑝
˜ otherwise
{︃ 𝛼1
𝛼2 if 𝛼2 ∈ 𝒱 ∪ {⊥}
𝛼
˜2 =
𝑝
˜ otherwise
{︃ 𝛼2
˜ 𝛽 if 𝛽 ∈ 𝒱 ∪ {⊥}
𝛽 =
𝑝
˜ otherwise
{︃ 𝛽
∅ if 𝛼1 ∈ 𝒱 ∪ {⊥}
Θ1 =
ClauIPL(𝑝˜𝛼1 → 𝛼1 ) otherwise
{︃
∅ if 𝛼2 ∈ 𝒱 ∪ {⊥}
Θ2 =
ClauIPL(𝛼2 → 𝑝 ˜𝛼2 ) otherwise
{︃
∅ if 𝛽 ∈ 𝒱 ∪ {⊥}
Θ3 =
ClauIPL(𝑝˜𝛽 → 𝛽) otherwise
𝛼 ≡ (𝜂1 ∧ 𝛼1 ∧ · · · ∧ 𝛼𝑥 )
→ (𝜂2 ∨ 𝛽1 ∨ · · · ∨ 𝛽𝑦 ) { ( 𝜂1 ∧ 𝑝 ˜ 𝛼𝑥 ) → ( 𝜂2 ∨ 𝑝
˜𝛼1 ∧ · · · ∧ 𝑝 ˜𝛽𝑦 ) }
˜ 𝛽1 ∨ · · · ∨ 𝑝
∪Θ′1 ∪ · · · ∪ Θ′𝑥 ∪ Θ′′1 ∪ · · · ∪ Θ′′𝑦
𝑥+𝑦 ≥1
Θ′𝑖 = ClauIPL(𝛼𝑖 → 𝑝˜𝛼𝑖 ), 𝑖 ∈ {1, . . . , 𝑥}
Θ′′𝑗 = ClauIPL(𝑝
˜𝛽𝑗 → 𝛽𝑗 ), 𝑗 ∈ {1, . . . , 𝑦}
𝜂1 = 𝑐1 ∧ · · · ∧ 𝑐𝑚 ∧ (𝑎1 → 𝑏1 ) ∧ · · · ∧ (𝑎𝑛 → 𝑏𝑛 ) 𝜂2 = 𝑑1 ∨ · · · ∨ 𝑑𝑙
𝛼1 , . . . , 𝛼𝑥 , 𝛽1 , . . . , 𝛽𝑦 are non-atomic formulas
Figure 2: Definition of the recursive procedure ClauIPL(𝛼), where 𝛼 is simplified.
.
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 ∨ · · · ∨ 𝛽𝑦 ) (last case in Fig. 2), and let ClauIPL(𝛼′ ) be any of the
recursive calls in the definition of ClauIPL(𝛼). We have two possible cases:
(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).
4. General Clauses
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:
𝑀 ̸|= □ 𝑀 |= 𝑎 iff 𝑎 ∈ 𝑀 𝑀 |=∼ 𝑎 iff 𝑎 ̸∈ 𝑀 𝑀 |= 𝑙1 | . . . | 𝑙𝑛 iff ∃𝑘 : 𝑀 |= 𝑙𝑘 .
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 realiz-
ability 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𝑊 𝛿 iff 𝑀 |= 𝛾, or there is 𝑀 ′ ∈ 𝑊 and 𝑖 ∈ {1, . . . , 𝑛} such that 𝑀 ⊆ 𝑀 ′ and
𝑀 ′ |= 𝑎𝑖 and 𝑀 ′ ̸|= 𝑏𝑖 .
• 𝑀 ◁𝑊 𝛿 iff, for every 𝑀 ′ ∈ 𝑊 , if 𝑀 ⊆ 𝑀 ′ then 𝑀 ′ ◁0𝑊 𝛿.
⎧
⎪
⎪ □ if 𝜂 = ⊥
⎪
𝑑1 | . . . | 𝑑𝑙 if 𝜂 = 𝑑1 ∨ · · · ∨ 𝑑𝑙
⎪
⎪
⎪
⎪
⎪
⎪
⎨ ∼ 𝑐1 | . . . |∼ 𝑐𝑚 | 𝑎1 ̸→ 𝑏1 | . . .
⎪
if 𝜂 = ( 𝑐1 ∧ · · · ∧ 𝑐𝑚 ∧ (𝑎1 → 𝑏1 ) ∧ . . .
Ψ(𝜂) =
⎪
⎪ . . . | 𝑎𝑛 ̸→ 𝑏𝑛 · · · ∧ (𝑎𝑛 → 𝑏𝑛 ) ) → ⊥
⎪
⎪
⎪
𝑑1 | . . . | 𝑑𝑙 |∼ 𝑐1 | . . . if 𝜂 = ( 𝑐1 ∧ · · · ∧ 𝑐𝑚 ∧ (𝑎1 → 𝑏1 ) ∧ . . .
⎪
⎪
⎪
⎪
⎪
⎩
. . . |∼ 𝑐𝑚 | 𝑎1 ̸→ 𝑏1 | . . . | 𝑎𝑛 ̸→ 𝑏𝑛 · · · ∧ (𝑎𝑛 → 𝑏𝑛 ) ) → (𝑑1 ∨ · · · ∨ 𝑑𝑙 )
𝛿 = 𝑑1 | . . . | 𝑑𝑙 |∼ 𝑐1 | . . . |∼ 𝑐𝑚 | 𝑎1 ̸→ 𝑏1 | . . . | 𝑎𝑛 ̸→ 𝑏𝑛
⎧
⎪
⎪ ⊥ if 𝛿 = □ (𝑙 = 𝑚 = 𝑛 = 0)
⎪
⎪
⎪
⎪
⎪
⎪ ¬(𝑐1 ∧ · · · ∧ 𝑐𝑚 ) if 𝑙 = 𝑛 = 0 and 𝑚 > 0
⎪
⎨𝑑1 ∨ · · · ∨ 𝑑𝑙 if 𝑙 > 0 and 𝑚 = 𝑛 = 0
⎪
⎪
⎪
Φ(𝛿) = ( 𝑐1 ∧ · · · ∧ 𝑐𝑚 ) → (𝑑1 ∨ · · · ∨ 𝑑𝑙 ) if 𝑙 > 0, 𝑚 > 0 and 𝑛 = 0
⎪
⎪
⎪
⎪
⎪
⎪ ¬(𝑐1 ∧ · · · ∧ 𝑐𝑚 ∧ (𝑎1 → 𝑏1 ) ∧ · · · ∧ (𝑎𝑛 → 𝑏𝑛 )) if 𝑙 = 0, 𝑚 > 0 and 𝑛 > 0
⎪
( 𝑐1 ∧ · · · ∧ 𝑐𝑚 ∧ (𝑎1 → 𝑏1 ) ∧ · · · ∧ (𝑎𝑛 → 𝑏𝑛 ) ) → otherwise
⎪
⎪
⎪
⎪
⎪
(𝑑1 ∨ · · · ∨ 𝑑𝑙 )
⎩
Figure 3: Translations between IPL-clauses and general clauses.
In general ◁0𝑊 is not monotone w.r.t. the inclusion relation ⊆. For instance, let 𝑊 = { ∅, {𝑎} };
then ∅◁0𝑊 ∼ 𝑎 and ∅ ⊆ {𝑎}, but {𝑎} ⋫0𝑊 ∼ 𝑎. 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
finite 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 𝒦(𝑊 ), 𝑤 ⊩ 𝑝 iff 𝑝 ∈ 𝑤.
From IPL-clauses to general clauses. In Fig. 3 we display the bijective map Ψ between IPL-
clauses 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 𝑊 , 𝑤 ◁𝑊 𝛿 iff 𝒦(𝑊 ), 𝑤 ⊩ Φ(𝛿).
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 𝑤 ⊩ 𝛼 → 𝛽. We proceed by induction on
the height of 𝑤 in 𝒦(𝑊 ), defined as the length of the longest path from 𝑤 to a maximal world
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 show that 𝑤′ ⊩ 𝛽. If 𝑤 < 𝑤′ , then 𝑤 ⊂ 𝑤′ and h(𝑤′ ) < h(𝑤). Since ◁𝑊 is monotone, it
holds that 𝑤′ ◁𝑊 𝛿; by the induction hypothesis, we get 𝑤′ ⊩ 𝛼 → 𝛽, 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. 𝑤 ≤ 𝑤′ and every
𝑗 ∈ {1, . . . , 𝑛}. Since 𝑤 ◁0𝑊 𝛿, there is 𝑘 ∈ {1, . . . , 𝑙} such that 𝑤 |= 𝑑𝑘 , hence 𝑤 ⊩ 𝛽. We have
proved that 𝑤 ⊩ 𝛼 → 𝛽, namely 𝑤 ⊩ Φ(𝛿); accordingly, 𝑤 ◁𝑊 𝛿 implies 𝑤 ⊩ Φ(𝛿).
To prove the converse, we show that:
(1) If 𝑤 ⊩ Φ(𝛿), then 𝑤 ◁0𝑊 𝛿.
We assume 𝑤 ⊩ Φ(𝛿), namely 𝑤 ⊩ 𝛼 → 𝛽, and we show 𝑤 ◁0𝑊 𝛿. If 𝑤 |= 𝛾, we immediately
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 𝑤 ≤ 𝑤′ and 𝑤′ ⊩ 𝑎𝑗 and
𝑤′ ⊮ 𝑏𝑗 , hence 𝑤 ⊆ 𝑤′ and 𝑤′ |= 𝑎𝑗 and 𝑤′ ̸|= 𝑏𝑗 . We get 𝑤 ◁0𝑊 𝛿, and this proves point (1).
Let us assume 𝑤 ⊩ Φ(𝛿) and let 𝑤′ ∈ 𝑊 such that 𝑤 ≤ 𝑤′ . Since 𝑤′ ⊩ Φ(𝛿), by (1) we get
𝑤 ◁0𝑊 𝛿. This proves that 𝑤 ◁𝑊 𝛿, and this concludes the proof of the proposition.
′ □
Sequents. 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
1
Here and below we leave understood the model 𝒦(𝑊 ).
𝑤3 : 𝑎, 𝑏, 𝑐, 𝑑, 𝑔
𝑤1 : 𝑏, 𝑑, 𝑔 𝑤2 : 𝑎, 𝑑, 𝑔
𝑤0 : 𝑑
Δ = { 𝑎 |∼ 𝑐 , 𝑏 |∼ 𝑐 , 𝑑 | 𝑔 , 𝑔 | 𝑎 ̸→ 𝑏 , 𝑔 | 𝑏 ̸→ 𝑎 , ∼ 𝑑 | 𝑐 ̸→ ⊥ }
Φ(Δ) = { 𝑐 → 𝑎 , 𝑐 → 𝑏 , 𝑑 ∨ 𝑔 , (𝑎 → 𝑏) → 𝑔 , (𝑏 → 𝑎) → 𝑔 , ¬(𝑑 ∧ ¬𝑐) }
𝑤0 ◁𝑊 Δ, 𝒦(𝑊 ), 𝑤0 ⊩ Φ(Δ)
Figure 4: Countermodel 𝑊 = {𝑤0 , 𝑤1 , 𝑤2 , 𝑤3 } for 𝜎 = Δ ⇒ 𝑔 (see Ex. 2).
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 iff 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 iff Φ(Δ) ̸|=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. □
2
Redundant lines are omitted, e.g. self-loops, the line connecting 𝑤0 with 𝑤3 .
% index of atoms
idxOfAtom(a,0). idxOfAtom(b,1). idxOfAtom(c,2). idxOfAtom(d,3). idxOfAtom(g,4).
%% classical clauses (3)
% c1 = a | ~c
clClause(c1). litOf(a, c1). litOf(neg(c), c1).
% c2 = b | ~c
clClause(c2). litOf(b, c2). litOf(neg(c), c2).
% c3 = d | g
clClause(c3). litOf(d, c3). litOf(g, c3).
%% non-classical clauses (3)
% gc1 = g | a-/->b
genClause(gc1). litOf(g, gc1). litOf(negImp(a, b), gc1).
% gc2 = g | b-/->a
genClause(gc2). litOf(g, gc2). litOf(negImp(b, a), gc2).
% gc3 = ~d | c-/->false
genClause(gc3). litOf(neg(d), gc3). litOf(negImp(c, false), gc3).
rightAtom(g). % right atom
atomSet( w(0..1, 0..1, 0..1, 0..1, 0..1) ). % shorthand for:
% atomSet(w(0,0,0,0,0)). atomSet(w(0,0,0,0,1)). ... atomSet(w(1,1,1,1,1)).
Figure 5: The component I𝜎 corresponding to the sequent 𝜎 defined in Ex. 2.
5. ASP Encoding
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(0, 0, 0, 0, 1) ↦→ {𝑔} ... w(1, 0, 1, 0, 1) ↦→ {𝑎, 𝑐, 𝑔} ...
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 cardi-
nality 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 % (1) search for a solution
clingo generator.lp minimize.lp sigma.lp % (2) search for a minimal solution
Example 3 Let sigma.lp be the instance I𝜎 in Fig. 5. The command (2) yields:
world(w(0,0,0,1,0)) world(w(0,1,0,1,1)) world(w(0,0,0,1,1)) world(w(1,1,1,1,1))
memberOfWorld(d,w(0,0,0,1,0)) memberOfWorld(b,w(0,1,0,1,1)) ....
Optimization: 4
OPTIMUM FOUND
The computed answer set defines the worlds
𝑤0 = w(0, 0, 0, 1, 0) 𝑤1 = w(0, 1, 0, 1, 1) 𝑤2 = w(1, 0, 0, 1, 1) 𝑤3 = w(1, 1, 1, 1, 1)
The solution corresponds to the countermodel in Fig. 4. ♢
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
Figure 6: Countermodel 𝑊 = {𝑤0 , 𝑤1 , 𝑤2 } for 𝛼 = (𝑎 → 𝑏) ∨ (𝑏 → 𝑎) (see Ex. 4).
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(0, 1, 1), 𝑤2 = w(1, 0, 1) (see Fig. 6). It is immediate to check that 𝒦(𝑊 ) is a
countermodel for the input formula 𝛼. ♢
The implementation of the procedures presented in the paper are available at https://github.
com/cfiorentini/clausificationIPL.
6. Conclusion and Future Work
In this paper we have presented a new approach to clausification for Intuitionistic Propositional
Logic which differs 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.
References
[1] K. Claessen, D. Rosén, SAT Modulo Intuitionistic Implications, in: M. Davis, A. Fehnker,
A. McIver, A. Voronkov (Eds.), LPAR-20, volume 9450 of LNCS, Springer, 2015, pp. 622–637.
[2] C. Fiorentini, R. Goré, S. Graham-Lengrand, A Proof-Theoretic Perspective on SMT-Solving
for Intuitionistic Propositional Logic, in: S. Cerrito, A. Popescu (Eds.), TABLEAUX 2019,
volume 11714 of LNCS, Springer, 2019, pp. 111–129.
[3] R. Dyckhoff, Contraction-free sequent calculi for intuitionistic logic, J. Symb. Log. 57
(1992) 795–807.
[4] C. Fiorentini, Efficient SAT-based proof search in intuitionistic propositional logic, in:
A. Platzer, G. Sutcliffe (Eds.), CADE 28, volume 12699 of LNCS, Springer, 2021, pp. 217–233.
[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 clause-
learning 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, Cam-
bridge 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, Cam-
bridge 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.