=Paper=
{{Paper
|id=Vol-212/paper-6
|storemode=property
|title=Tableau Decision Procedure for Propositional Intuitionistic Logic
|pdfUrl=https://ceur-ws.org/Vol-212/07_Fiorino.pdf
|volume=Vol-212
}}
==Tableau Decision Procedure for Propositional Intuitionistic Logic==
https://ceur-ws.org/Vol-212/07_Fiorino.pdf
A Tableau Decision Procedure for Propositional
Intuitionistic Logic
Alessandro Avellone, Guido Fiorino, Ugo Moscato
Dipartimento di Metodi Quantitativi per l’Economia,
Università Milano-Bicocca,Piazza dell’Ateneo Nuovo, 1, 20126 Milano, Italy
{alessandro.avellone,guido.fiorino,ugo.moscato}@unimib.it
November 3, 2006
Abstract
The contribution of this paper consists in some techniques to bound the proof
search space in propositional intuitionistic logic. These techniques are justified by
Kripke semantics and they are the backbone of a tableau based theorem prover
(PITP) implemented in C++ language. PITP and some known theorem provers
are compared by the formulas of ILTP v1.1.1 benchmark library. It turns out that
PITP is, at the moment, the propositional prover that solves most formulas of the
library.
1 Introduction
The development of effective theorem provers for intuitionistic and constructive logics
is of interest both for the investigations and applications of such logics to formal soft-
ware/hardware verification and program synthesis (see i.e. [ML84, Con86, ES99, Men00,
FFO02, BC04, AFF+ 06]).
In this paper we present a strategy and an implementation based on a tableau
calculus for propositional intuitionistic logic. Our decision procedure implements the
tableau calculus of [AFM04] (this calculus is an enhancement of the calculus given in
[Fit69] and it is related to the tableau and sequent calculi of [MMO97, Hud93, Dyc92]).
We introduce some new techniques utilized by our decision procedure to narrow the
search space and the width of the proofs. The PSPACE-completeness of intuitionistic va-
lidity ([Sta79]) suggests that backtracking and branching cannot be eliminated. In order
to improve the time efficiency of the implementations and make them usable, strategies
have to be developed to bound backtracking and branching as much as possible.
The optimizations we present are explained by the Kripke semantics for intuitionistic
logic. Such semantical techniques are related to the fact that tableau calculi are strictly
joined to the semantics of the logic at hand. Loosely speaking, a tableau proof for a
formula is the attempt to build a model satisfying the formula. The construction of such
a model proceeds by increasing, step by step, the information necessary to define such
a model (thus, step by step the accuracy of the model increases). If the proof ends in
a contradiction, then there is no model for the formula. Otherwise, a model satisfying
the formula is immediately derived from the proof. With this machinery at hand, first
we provide a sufficient condition allowing us to stop a tableau proof without loosing
the completeness. Then we describe a technique to bound branching on the formulas
which only contain conjunctions and disjunctions. Finally we present a technique to
deduce the satisfiability of a set of formulas S, when the satisfiability of a set S ! and
a permutation τ such that S = τ (S ! ) are known. Such a technique allows us to bound
backtracking. Our technique to bound backtracking is different from the semantical
technique provided in [Wei98].
Besides the strategy and its completeness, in the final part of the paper we present
some experimental results on the implementation PITP. PITP is written in C++ and
it is tested on the propositional part of ILTP v1.1.1 benchmark library ([ROK06]). Of
274 propositional benchmarks contained in ILTP v1.1.1, PITP decides 215 formulas
including 13 previously unsolved problems within the time limit of ten minutes. To
give the reader more elements to evaluate PITP strategies, comparisons with different
versions of PITP are provided.
2 Notation and Preliminaries
We consider the propositional language L based on a denumerable set of propositional
variables or atoms PV and the logical connectives ¬, ∧, ∨, →. (Propositional) Kripke
models are the main tool to semantically characterize (propositional) intuitionistic logic
Int (see [CZ97] and [Fit69] for the details). A Kripke model for L is a structure K =
$P, ≤, ρ, !&, where $P, ≤, ρ& is a poset with minimum ρ and ! is the forcing relation, a
binary relation between elements α of P and p of PV such that α ! p and α ≤ β imply
that β ! p. The forcing relation is extended in a standard way to arbitrary formulas of
L as follows:
1. α ! A ∧ B iff α ! A and α ! B;
2. α ! A ∨ B iff α ! A or α ! B;
3. α ! A → B iff, for every β ∈ P such that α ≤ β, β ! A implies β ! B;
4. α ! ¬A iff for every β ∈ P such that α ≤ β, β ! A does not hold.
We write α ! A when α ! A does not hold.
It is easy to prove that for every formula A, if α ! A and α ≤ β, then β ! A. A
formula A is valid in a Kripke model K = $P,≤,ρ,!& if and only if ρ ! A. It is well
known that Int coincides with the set of formulas valid in all Kripke models.
If we consider Kripke models K = $P,≤,ρ,!& such that |P | = 1 we get classical mod-
els for (propositional) classical logic Cl. Classical models are usually seen as functions
σ from PV to {true, f alse}. Given a formula A and a model σ, we use σ |= A with
the usual meaning of satisfiability. Finally, given a set S, the set PV(S) denotes the
elements of PV occurring in S.
In the following presentation, we give a brief overview of the tableau calculus Tab of
[AFM04] which is implemented by our decision procedure. The rules of the calculus are
given in Table 1. The calculus works on signed well formed formulas (swff for short),
where a swff is a (propositional) formula prefixed with a sign T, F or Fc . Given a
Kripke model K = $P,≤,ρ,!&, a world α ∈ P , a formula A and a set of swffs S, the
meaning of the signs is as follows:
• α ! TA (α realizes TA) iff α ! A;
• α ! FA iff α ! A;
• α ! Fc A iff α ! ¬A;
• α ! S iff α realizes every swff in S.
• K ! S iff ρ ! S.
A proof table (or proof tree) for S is a tree, rooted with S and obtained by the subsequent
application of the rules of the calculus. As an example, let Γ = {T(A ∧ B), T(B ∧
C), F(A ∨ B)}. With “ rule T∧ applies to Γ taking H ≡ T(A ∧ B) as main swff” we
mean that T∧ applies to Γ as Γ\{T(A∧B)},TA,TB
Γ
T∧. If no confusion arises we say that
a rule applies to Γ or equivalently a rule applies to H. Finally with Rule(H) we mean
the rule related to H (in our example Rule(T(A ∧ B)) is T∧).
For every proof table for S, the depth and the number of symbols occurring in the
nodes is linearly bounded in the number of symbols occurring in S (see [AFM04] for
further details). This is the key feature to implement a depth-first decision procedure
whose space complexity is O(n lg n) (as a matter of fact, it is well known that to generate
all the proof tables in the search space and to visit them with a depth-first strategy, it
is sufficient to have a stack containing, for every node of the visited branch, the index
of the main swff and a bit to store if the leftmost branch has been visited [Hud93]).
We emphasize that the sign Fc is introduced to give a specialized treatment of the
negated formulas. In this sense the rules for the formulas signed with Fc could be
rewritten replacing in the Fc -rules every occurrence of the sign Fc with T¬.
Given a set of swffs S, the signed atoms of S are the elements of the set δS =
{H|H ∈ S and H is a signed atom}. We say that S contains a complementary pair iff
{TA, FA} ⊆ S or {TA, Fc A} ⊆ S. Given δS , we denote with σδS the (classical) model
defined as follows: if Tp ∈ δS , then σδS (p) = true, σδS (p) = f alse otherwise.
Given a classical model σ, (i) σ !TH iff σ |= H; (ii) σ !FH and σ !Fc H iff σ *|= H.
Given a set of swffs S, a swff H (respectively a set of swffs S ! ) and the set of signed
atoms δS defined as above, we say that δS r ealizes H (respectively δS realizes S ! ), and
we write δS ! H (respectively δS ! S ! ), iff there exists a classical model σ fulfilling the
following conditions:
(i) σ ! H (respectively σ ! H ! for every H ! ∈ S ! ).
(ii) if Tp ∈ δS , then σ(p) = true;
(iii) if Fp ∈ δS or Fc p ∈ δS , then σ(p) = f alse
In other words, the relation ! between δS and a signed formula H holds if there exists
a classical model σ both realizing δS and H. If {Tp, Fc p, Fp} ∩ S = ∅ then there is no
condition on the truth value that σ gives to p.
S, T(A ∧ B) S, F(A ∧ B) S, Fc (A ∧ B)
T∧ F∧ Fc ∧
S, TA, TB S, FA|S, FB Sc , Fc A|Sc , Fc B
S, T(A ∨ B) S, F(A ∨ B) S, Fc (A ∨ B)
T∨ F∨ Fc ∨
S, TA|S, TB S, FA, FB S, Fc A, Fc B
S, TA, T(A → B)
T → Atom, with A an atom
S, TA, TB
S, F(A → B) S, Fc (A → B)
F→ Fc →
Sc , TA, FB Sc , TA, Fc B
S, T(¬A) S, F(¬A) S, Fc (¬A)
T¬ F¬ Fc ¬
S, Fc A Sc , TA Sc , TA
S, T((A ∧ B) → C) S, T(¬A → B)
T→∧ T→¬
S, T(A → (B → C)) Sc , TA|S, TB
S, T((A ∨ B) → C)
T→∨
S, T(A → p), T(B → p), T(p → C)
S, T((A → B) → C)
T →→
Sc , TA, Fp, T(p → C), T(B → p)|S, TC
where Sc = {TA|TA ∈ S} ∪ {Fc A|Fc A ∈ S} and
p is a new atom
Table 1: the Tab calculus
We say that a wff or a swff is classically evaluable (cle-wff and cle-swff for short) iff
conjunctions and disjunctions are the only connectives occurring in it. Finally, a set S
of swffs is contradictory if at least one of the following conditions holds:
1. S contains a complementary pair;
2. S contains a cle-swff H such that δS " H;
3. δS " S and for every propositional variable p occurring in S, Tp ∈ S or Fc p ∈ S.
Proposition 2.1 If a set of swffs S is contradictory, then for every Kripke model K =
$P,≤,ρ,!&, ρ " S.
Proof: If S is contradictory because the first condition holds, then for some formula
A, {TA, FA} ⊆ S or {TA, Fc A} ⊆ S holds. By the meaning of the signs and the
definition of the forcing relation in Kripke models, the claim immediately follows. If
S is contradictory because the second condition holds, then δS " H. Thus, there is
no classical model realizing both the signed atoms of S (that is δS ) and H. Since H
is a cle-swff, its classical and intuitionistic realizability coincide, thus no Kripke model
realizes S. If S is contradictory because the third condition holds, then let us suppose
there exists a Kripke model K = $P,≤,ρ,!& such that ρ ! S. Then for every p ∈ PV(S),
ρ ! p or ρ ! ¬p and this means that every world in K forces the same propositional
variables occurring in S, that is for every α, β ∈ P and for every p ∈ PV(S), α ! p
iff β ! p. Let φ ∈ P be a maximal state in the poset $P, ≤, ρ&. Since φ behaves as a
classical model, by hypothesis, φ " S. Then, since every world of K forces the same
propositional variables of S we deduce that ρ " S. /
.
A closed proof table is a proof table whose leaves are all contradictory sets. A closed
proof table is a proof of the calculus: a formula A is provable if there exists a closed
proof table for {FA}. For every rule of the calculus it is easy to prove that if there
exists a Kripke model K = $P,≤,ρ,!& and α ∈ P such that α realizes the premise of
the rule, then there exists (a possibly different) Kripke model K ! = $P ! , ≤! , ρ! , !! & and
β ∈ P ! such that β realizes the conclusion. This is the main step to prove the soundness
of the calculus:
Theorem 2.2 (Soundness) Let A be a wff. If there exists a closed proof table starting
from {FA}, then A is valid.
3 The optimizations and the proof search algorithm
Below we describe a recursive procedure Tab(S) which given a set S of swffs, returns
either a closed proof table for S or NULL (if there exists a Kripke model realizing S).
To describe Tab we use the following notation. Let S be a set of swffs, let H ∈ S
and let S1 or S1 | S2 be the nodes of the proof tree obtained by applying to S the rule
Rule(H) corresponding to H. If T ab1 and T ab2 are closed proof tables for S1 and S2
S S
respectively, then Rule(H) or Rule(H) denote the closed proof table for
T ab1 T ab1 | T ab2
S defined in the obvious way. Moreover, Ri (H) (i = 1, 2) denotes the set containing the
swffs of Si which replaces H. For instance:
R1 (T(A ∧ B)) = { TA, TB },
R1 (T(A ∨ B)) = {TA}, R2 (T(A ∨ B)) = {TB},
R1 (T((A → B) → C)) = { TA, Fp, T(B → p), T(p → C) },
R2 (T((A → B) → C)) = {TC}.
As stated in the introduction, Tab uses substitutions. For our purposes, the only
substitutions we are interested in are permutations from PV to PV. Given a substitution
τ and a swff H (respectively, a set of swffs S and tableau T ) τ (H) (respectively, τ (S)
and τ (T )) means the swff (respectively, the set of swffs and the tableau) obtained by
applying the substitution in the obvious way.
The procedure Tab divides the formulas in six groups according to their behavior
with respect to branching and backtracking:
C1 = {T(A ∧ B), F(A ∨ B), Fc (A ∨ B), T(¬A), T(p → A) with p an atom, T((A ∧ B) →
C), T((A ∨ B) → C)};
C2 = {T(A ∨ B), F(A ∧ B);
C3 = {F(¬A), F(A → B)};
C4 = {T((A → B) → C), T(¬A → B)};
C5 = {Fc (A → B), Fc (¬A)};
C6 = {Fc (A ∧ B)}.
We call Ci -swffs (i = 1, . . . , 6), respectively Ci -rules, the swffs of the group Ci , respectively
the rules related to Ci -swffs.
The intuition behind these groups can be explained as follows. It is well known that
in classical logic the order in which the rules are applied does not affect the completeness
of the decision procedure: if a proof exists it is found independently of the order in
which the rules are applied. Thus the search space consists of a single proof tree whose
branches have to be visited by the decision procedure. The rules having two conclusions
give rise to branches. Rules of this kind are T∨ and F∧. In intuitionistic logic the
order in which the rules are applied is relevant and affect the completeness. Given a
set Γ, there are many ways to go on with the proof (that is many swffs can be chosen
as main swff). Since the order is relevant, if the choice of a swff as main swff does not
give a closed proof table, we have to backtrack and try with another swff as main swff.
This means that in intuitionistic logic there is a space of proof tables to be visited by
backtracking. Rules requiring backtracking are, i.e., F →, T →→. In order to bound
time consumption, Tab applies the rules not requiring branching and backtracking first,
then the rules not requiring backtracking, finally the rules requiring backtracking. In the
Completeness Lemma (Lemma 4.1, page 11) we prove that we do not lose completeness
if C5 and C6 -rules are applied only when no other rule applies. Thus the application of
C5 and C6 -rules is invertible and no backtracking is required. On the other hand, to get
completeness, backtracking is unavoidable when C3 and C4 -rules are applied.
Now we come to the optimizations. First we discuss two checks that allow us to
bound the depth of the proofs. Let S be a set such that σδS ! S. Thus the Kripke
model coinciding with the classical model σδS realizes S and we do not need to go on
with the proof. The second check is related to Point 3 in the definition of contradictory
set. If δS " S and every propositional variable occurring in S occurs in S as swff signed
T or Fc , then there is no Kripke model realizing S and we do not need to proceed
with the proof. Although these checks could be performed after every rule application,
our strategy performs it when neither a C1 nor a C2 -rule applies to S (in Section 5 this
optimization is referred as opt1).
In order to bound branching, Tab treats in a particular way the cle-swffs in S, that
is the swffs in which only ∧ and ∨ occur (in other words swffs whose intuitionistic truth
coincides with classical truth). When Tab treats C2 -swffs (Point 3 of the algorithm
given below), first of all Tab checks if in S there exists a cle-swff H such that δS " H.
If S fulfills this condition, then S is not realizable, as we pointed out in Proposition 2.1.
Otherwise, if in S a cle-swff H occurs, such that σδS does not satisfy H, the splitting
rule Rule(H) is applied (we recall that σδS is the classical model defined from S by
taking as true the atoms p such that Tp ∈ S). Thus the cle-swffs of S, satisfying
the underlying model, are never applied. Despite this, from the realizability of one
among (S \ {H}) ∪ R1 (H) and (S \ {H}) ∪ R2 (H) we have enough information to prove
the realizability of S. In other words, we consider only the cle-swffs of C2 that are
not realized by the model underlying S (see Point 3 and Completeness Lemma for the
details). As an example consider
S = { F(P 0 ∧ P 2), F(P 0 ∧ P 4), F(P 2 ∧ P 4), F(P 1 ∧ P 3), F(P 1 ∧ P 5),
F(P 3 ∧ P 5), T(P 0 ∨ P 1), T(P 2 ∨ P 3), T(P 4 ∨ P 5) }.
Since σδS realizes the F-swffs in S but σδS does not realize any of the T-swffs of S, then
Tab chooses one of them, let us suppose H = T(P 0 ∨ P 1). The rule T∨ is applied
to S and S1 = (S \ {H}) ∪ {TP 0} and S2 = (S \ {H}) ∪ {TP 1} are the subsequent
sets of S. Now consider S1 . Since σδS1 realizes TP 0 and all the F-swffs in S1 , but σδS1
realizes neither T(P 2 ∨ P 3) nor T(P 4 ∨ P 5), Tab chooses one of them, let us suppose
H = T(P 2 ∨ P 3). The rule T∨ is applied to S1 and S3 = (S1 \ {H}) ∪ {TP 2} and
S4 = (S1 \ {H}) ∪ {TP 3} are the subsequent sets of S1 . Since δS3 does not realize
F(P 0 ∧ P 2) we deduce that S3 is contradictory. Similarly for the other sets. We
emphasize that at every step, the C2 -rules applicable to Si are only the ones where the
related swffs are not realized by σδSi . Without this strategy a huge closed proof table
could arise (in Section 5 this optimization is referred as opt2).
To bound the search space, [Wei98] describes a decision procedure in which back-
tracking is bounded by a semantical technique inspired by the completeness theorem.
The completeness theorem proves the satisfiability (realizability in our context) of a
set S under the hypothesis that S does not have any closed proof table. As an ex-
ample, let S = {F(A → B), T((A → B) → C), FC, TD}. From S we can de-
fine the Kripke model K(S) = $P,≤,ρ,!& such that P = {ρ} and ρ ! D. Note
that K(S) realizes TD but K(S) does not realize S. To prove the realizability of
S, the realizability of S1 = {TA, FB, T((A → B) → C), TD} and one between
S2 = {TA, Fp, T(B → p), T(p → C), TD} and S3 = {F(A → B), TC, FC, TD}
have to be proved. Since S3 is not realizable, the realizability of S1 and S2 must
be proved. From S1 we define the Kripke model K(S1 ) = ${α},≤,α,!&, where α ≤ α,
α ! D and α ! A such that K(S1 ) ! S1 . If we glue K(S1) above K(S) we get a
new Kripke model K = ${ρ, α},≤,ρ,!& where ρ ≤ ρ, ρ ≤ α, α ≤ α, ρ ! D,α ! D
and α ! A. Since K ! S, we do not need to apply T →→ to S in order to obtain
S2 = {TA, Fp, T(B → p), T(B → C), TD} (from S2 a Kripke model K(S2 ) is defin-
able; K(S2 ) glued above K(S) gives rise to a Kripke model realizing S). In this case the
work on S2 is spared. In the general case, see [Wei98], the information collected from
non closed proof tables built from a set S is used to build a Kripke model K. As a mat-
ter of fact, let S be a set such that no C1 or C2 -rule is applicable. Let {H1 , . . . , Hu } ⊆ S
the C3 and C4 -swffs of S. If there exists a Hj such that K " Hj , then Rule(Hj ) have
to be applied. If a closed proof table is found, then S is not realizable, otherwise the
Kripke model K can be extended in a new one, K j satisfying Hj . The procedure of
[Wei98] continues until a closed proof table or a Kripke model K i , 1 ≤ i ≤ u, such that
K i ! {H1 , . . . , Hu } is found. The procedure prunes the search space, since in S not all
the swffs requiring backtracking are considered, but only the swffs which, when checked,
are not realized from the Kripke model at hand.
Now, consider S = {F(A → B), F(C → D)}. From S we can define the Kripke model
K(S) = $P,≤,ρ,!& such that P = {ρ} and ! is the empty set. K(S) does not realize
S. By applying F → to S with F(A → B) as the main formula we get S1 = {TA, FB}.
The underlying model is K(S1 ) = ${α},≤,α,!& with α ! A. K(S1 ) glued above K(S)
gives rise to a model that does not realize F(C → D). Thus we must backtrack. We
apply F → to S with F(C → D) as the main formula. We get S2 = {TC, FD}. The
underlying model is K(S2 ) = ${β},≤,β,!& such that β ≤ β and β ! C realizes S2 . By
gluing K(S1 ) and K(S2 ) above K(S) the resulting model K = ${ρ, α, β},≤,ρ,!& such
that
ρ ≤ α, ρ ≤ β, ρ ≤ ρ, α ≤ α, β ≤ β, α ! A and β ! C
realizes S. But by a permutation τ : PV → PV such that τ (C) = A and τ (D) = B,
τ (S2 ) = S1 and we can build K(S2 ) = $P, ≤, !! , ρ, & from K(S1 ) as follows: K(S2 ) has
the same poset as K(S1 ) and !! is: for every α ∈ P and for every p ∈ PV, α !! p iff
α ! τ (p). In other words, K(S1 ) can be translated into K(S2 ) via τ and we can avoid
backtracking on S. As another example consider
S = { T(((P 0 → (P 1 ∨ P 2)) → (P 1 ∨ P 2))),
T(((P 2 → (P 1 ∨ P 0)) → (P 1 ∨ P 0))),
T(((P 1 → (P 2 ∨ P 0)) → (P 2 ∨ P 0))), F((P 1 ∨ (P 2 ∨ P 0))) },
where only a few"steps are needed to obtain $S starting from {FH}, where H is the
! # # #
axiom schema 2i=0 (Pi → j#=i Pj ) → j#=i Pj → 2i=0 Pi characterizing the logic of
binary trees (a logic in the family of k-ary trees logics, [CZ97], also known as Gabbay-de
Jongh logics). From S we can define the model K(S) = $P,≤,ρ,!& such that P = {ρ}
and ! is the empty set. K(S) does not realize S. By applying T →→ to S with
H = T(((P 0 → (P 1 ∨ P 2)) → (P 1 ∨ P 2))) we get S1 = (S \ {H}) ∪ R2 (H) and
S2 = (S \ {H})c ∪ R1 (H). Since S1 is not realizable, to prove the realizability of S we
have to prove the realizability of S2 . S2 defines the Kripke model K(S2 ) = ${α},≤,α,!&,
where α ≤ α and α ! P 0. Thus K(S2 ) ! S2 holds. Now, if we glue K(S2 ) above K(S)
we get a new model K ! (S) = ${ρ, α},≤,ρ,!&, where ρ ≤ ρ, ρ ≤ α, α ≤ α and α ! P 0.
K ! (S) does not realize S. Thus we must backtrack twice:
(i) by applying T →→ to S with H = T(((P 2 → (P 1 ∨ P 0)) → (P 1 ∨ P 0))) we get,
S3 = (S \ {H})c ∪ R1 and S4 = (S \ {H}) ∪ R2 (H);
(ii) by applying T →→ to S with H = T(((P 1 → (P 2 ∨ P 0)) → (P 2 ∨ P 0))) we get
S5 = (S \ {H}) ∪ R2 (H) and S6 = (S \ {H})c ∪ R1 (H).
In a few steps we find that S4 and S6 are not realizable. From S3 we define the Kripke
model K(S3 ) = ${β},≤,β,!& where β ≤ β and β ! P 2. K(S3 ) ! S3 . From S5 we define
the Kripke model K(S5 ) = ${γ},≤,γ,!& where γ ≤ γ and γ ! P 1. K(S5 ) ! S5 . Thus
by gluing K(S2 ), K(S3 ) and K(S5 ) above K(S) we get a model K realizing S. Since we
can define the permutations τ1 and τ2 such that τ1 (S3 ) = S2 and τ2 (S5 ) = S2 we can
avoid backtracking. Thus no proof of realizability of S3 or S5 is needed and the Kripke
models realizing S3 and S5 can be obtained by applying the permutations on the forcing
relation of the Kripke model for S2 .
Thus to avoid backtracking Tab builds a permutation τ between sets of swffs. Let
H be C3 -swff. Before applying Rule(H) we check if there exists a permutation τ from
PV(S) to PV(S) such that τ ((S \ {H})c ∪ R1 (H)) = (S \ {H ! })c ∪ R1 (H ! ). We already
know that the set (S \ {H ! })c ∪ R1 (H ! ) obtained treating H ! is realizable by a Kripke
model K ! . Since we have a permutation τ , then the set (S \{H})c ∪R1 (H) is realized by
the Kripke model K having the same poset as K ! and such that for every world α and
every propositional variable p, α !K ! p iff α !K τ (p). This means that the permutation
τ allows us to go from K ! to K (and the permutation τ −1 allows us to go from K to K ! ).
In particular, τ and τ −1 translate the forcing relation between the models. Analogously
if H is a C4 -swff. We emphasize that given a Kripke model K, a permutation τ and a
swff H, K ! H does not imply K ! τ (H). Thus we have taken a different route with
respect to [Wei98], where the realizability of τ (H) is checked on K that realizes H and
the two methods work in different situations. We emphasize that both methods imply a
certain computational cost. The method of [Wei98] implies checking the realizability on
a Kripke model, which is time consuming for swffs of the kind T(A → B). Our method
can be time consuming if we perform a search of a permutation among the P v(S)!
possible permutations. However, as we describe in Section 5, the procedure searches in
a small subset of all possible permutations (in Section 5, this optimization is referred as
opt3).
Finally, we could also define a permutation to prove that a set is not realizable. As a
matter of fact, if S is not realizable and there exists a permutation τ such that τ (S) = S ! ,
then S ! is not realizable. Thus, given a set S and a C2 or C6 -swff H ∈ S, if (S \ {H}) ∪
R1 (H) is closed and there exists a permutation τ such that τ ((S \ {H}) ∪ R1 (H)) =
(S \ {H}) ∪ R2 (H) then (S \ {H}) ∪ R2 (H) is not realizable and the tableau proof for
(S \ {H}) ∪ R1 (H) can be translated via τ in a tableau proof for (S \ {H}) ∪ R2 (H)
(see Points 3 and 6 of Tab). As a trivial application, consider a valid wff H(p), where
p = {p1 , . . . , pn } are all the propositional variables occurring in H. To prove that
{F(H(p) ∧ H(q))} is closed, it is sufficient to prove, by an application of F∧, that
{FH(p)} is closed and there exists a permutation such that {FH(p)} = τ ({FH(q)}).
To save work space, we describe Tab in natural language. The algorithm is divided
in seven main points. We recall that the input of Tab is a set S of swffs. If S is
realizable, then Tab returns NULL, otherwise Tab returns a closed proof table for S. In
the following description, given a set V of swffs, Tab (V) is the recursive call to Tab
with actual parameter V . Some instructions ’return NULL’ are labeled with r1,. . . , r6.
In the Completeness Lemma we refer to such instructions by means of these labels.
Function Tab (S)
1. If S contains a complementary pair, then Tab returns the proof S;
2. If a C1 -rule applies to S, then let H be a C1 -swff. If Tab((S \ {H}) ∪ R1 (H)) returns
S
a proof π, then Tab returns the proof Rule(H), otherwise Tab returns NULL (r1);
π
3. If a C2 -rule applies to S, then if there exists a C2 -swff H such that H is a cle-swff
and δS " H, then Tab returns (the proof) S. Otherwise, let H be a cle-swff such that
σδS " H, if there is any, otherwise let H be a C2 -swff. Let π1 = Tab(S \ {H} ∪ R1 (H)).
If π1 is NULL, then Tab returns NULL. If there exists a permutation τ such that (S \
S
{H}) ∪ R1 (H) = τ (S \ {H}) ∪ R2 (H)), then Tab returns the proof Rule(H).
π1 | τ −1 (π1 )
If such a permutation does not exist, then let π2 = Tab(S \ {H} ∪ R2 (H)). If π2 is a
S
proof, then Tab returns the proof Rule(H), otherwise (π2 is NULL) Tab returns
π1 | π 2
NULL;
4. If a C3 or C4 -rule applies to S, then Tab proceeds as follows: if σδS ! S, then Tab
returns NULL (r2). If for every p ∈ PV(S), Tp ∈ S or Fc p ∈ S, then Tab returns S.
If the previous points do not apply, then Tab carries out the following Points 4.1 and
4.2:
4.1 Let {H1 , . . . Hn } be all the C3 -swffs in S. For i = 1, . . . , n, the following instructions
are iterated: if there is no swff Hj (j ∈ {1, . . . , i − 1}) and a permutation τ such that
(S \{Hj })c ∪R1 (Hj ) = τ ((S \{Hi })c ∪R1 (Hi )), then let π = Tab((S \{Hi })c ∪R1 (Hi )).
S
If π is a proof, then Tab returns the proof Rule(Hi );
π
4.2 Let {H1 , . . . Hn } be all the C4 -swffs in S. For i = 1, . . . , n, the following Points (4.2.1)
and (4.2.2) are iterated.
(4.2.1) If there is neither swff Hj (j ∈ {1, . . . , i − 1}) nor a permutation τ such that
(S\{Hj })∪R2 (Hj ) = τ ((S\{Hi })∪R2 (Hi )), then let π2,i = Tab((S\{Hi })∪R2 (Hi )). If
π2,i is NULL, then Tab returns NULL (r3). If there is neither swff Hj , with j ∈ {1, . . . , i −
1}, nor a permutation τ such that (S \ {Hj })c ∪ R1 (Hj ) = τ ((S \ {Hi })c ∪ R1 (Hi )), then
S
if Tab((S \ {Hi })c ∪ R1 (Hi )) returns a proof π1 , Tab returns the proof Rule(Hi ).
π1 | π2,i
(4.2.2) If Point (4.2.1) does not hold, then there exists a permutation τ and a swff Hj
(j ∈ {1, . . . , i−1}) such that (S \{Hj })∪R2 (Hj ) = τ ((S \{Hi })∪R2 (Hi )). If there is no
swff Hu , with u ∈ {1, . . . , i − 1}, and a permutation τ such that (S \ {Hu })c ∪ R1 (Hu ) =
τ ((S \ {Hi })c ∪ R1 (Hi )), then if Tab((S \ {Hi })c ∪ R1 (Hi )) returns a proof π1 , Tab
S
returns the proof Rule(Hi ).
π1 | τ (π2,j )
−1
If in Points (4.1) and (4.2) Tab does not find any closed proof table, then Tab returns
NULL (r4).
5. If a C5 -rule applies to S, then let H be a C5 -swff. If Tab((S \ {H})c ∪ R1 (H)) returns
S
a proof π, then Tab returns the proof Rule(H), otherwise Tab returns NULL;
π
6. If a C6 -rule applies to S, then let H be a C6 -swff. Let π1 = Tab((S \ {H})c ∪ R1 (H)).
If π1 is NULL, then Tab returns NULL. If there exists a permutation τ such that (S \
S
{H})c ∪R1 (H) = τ ((S\{H})c ∪R2 (H)), then Tab returns the proof Rule(H).
π1 | τ −1 (π1 )
If such a permutation does not exist, then let π2 = Tab((S \ {H})c ∪ R2 (H)). If π2 is a
S
proof, then Tab returns Rule(H), otherwise (π2 is NULL) Tab returns NULL (r5);
π1 | π 2
7. If none of the previous points apply, then Tab returns NULL (r6).
end function Tab.
Point 4 deserves some comments. If the classical model σδS realizes S (condition
“σδS ! S”) then such a model is a Kripke model realizing S. If for every propositional
variable p ∈ P v(S), Tp ∈ S or Fc p ∈ S holds, then the subsequent sets of S do not
contain more information than S and from σδS " S we deduce δS " S. Since δS " S,
then S is not realizable (see Proposition 2.1). The iteration in Points 4.1 and 4.2 can
be summarized as follows: a proof for S is searched: for every C3 or C4 -swff H in S,
Rule(H) is applied to S. If no proof is found, then S is realizable. Now consider C3 -swffs.
If for a previous iteration j the set obtained by applying Rule(Hj ) to S is realizable
and can be translated via a permutation τ in (S \ {Hi })c ∪ R(Hi ), then Tab does not
apply Rule(Hi ) to S. The permutation τ and the realizability of (S \ {Hj })c ∪ R(Hj )
imply the realizability of (S \ {Hi })c ∪ R(Hi ) (see Case 4 in Completeness Lemma).
Tab applies the same idea in Point 4.2 to C4 -swffs of S. This point is more complex
because C4 -rules have two conclusions.
4 Completeness
In order to prove the completeness of Tab, we prove that given a set of swffs S, if the
call Tab(S) returns NULL, then we have enough information to build a countermodel
K = $P,≤,ρ,!& such that ρ ! S. To prove the proposition we need to introduce the
function deg defined as follows:
• if p is an atom, then deg(p) = 0;
• deg(A ∧ B) = deg(A) + deg(B) + 2;
• deg(A ∨ B) = deg(A) + deg(B) + 3;
• deg(A → B) = deg(A) + deg(B)+ (number of implications occurring in A) + 1;
• deg(¬A) = deg(A) + 1;
%
• deg(S) = H∈S deg(H).
It is easy to show that if S ! is obtained from a set of swffs S by an application of a rule
of Tab, then deg(S ! ) < deg(S).
Lemma 4.1 (Completeness) Let S be a set of swffs and suppose that Tab(S) returns
the NULL value. Then, there is a Kripke model K = $P,≤,ρ,!& such that ρ ! S.
Proof: The proof goes by induction on the complexity of S, measured with respect to
the function deg(S).
Basis: if deg(S) = 0, then S contains atomic swffs only. Tab(S) carries out the in-
struction labeled (r6). Moreover, S does not contain sets of the kind {Tp, Fp} and
{Tp, Fc p}. Let K = $P,≤,ρ,!& be the Kripke model such that P = {ρ} and ρ ! p iff
Tp ∈ S. It is easy to show that ρ ! S.
Step: Let us assume by induction hypothesis that the proposition holds for all sets S !
such that deg(S ! ) < deg(S). We prove that the proposition holds for S by inspecting
all the possible cases where the procedure returns the NULL value.
Case 1: the instruction labeled r1 has been performed. By induction hypothesis there
exists a Kripke model K = $P,≤,ρ,!& such that ρ!(S \{H})∪R1 (H), with H ∈ C1 . We
prove ρ ! H by proceeding according to the cases of H. If H is of the kind T(A ∧ B),
then by induction hypothesis ρ ! {TA, TB}, thus ρ ! A and ρ ! B, and therefore
ρ ! A ∧ B. This implies ρ ! T(A ∧ B). The other cases for H ∈ C1 are similar.
Case 2: the instruction labeled r2 has been performed. Thus σδS ! S holds. We use σδS
to define a Kripke model K with a single world ρ such that ρ ! p iff σ(p) = true. Since
ρ behaves as a classical model, ρ ! S holds.
Case 3: the instruction labeled r3 has been performed. By induction hypothesis there
exists a model K such that ρ ! (S \ {Hi }) ∪ R2 (Hi ), where Hi ∈ C4 . Let us suppose that
H is of the kind T((A → B) → C), thus ρ ! TC and this implies ρ ! Hi . The proof
goes similarly if Hi is of the kind T(¬A → B).
Case 4: the instruction labeled r4 has been performed. This implies that: (i) for ev-
ery H ∈ S ∩ C3 , we have two cases: (ia) Tab((S \ {H})c ∪ R1 (H)) = NULL, thus
by induction hypothesis there exists a Kripke model K H = $PH , ≤H , ρH , !H & such
that ρH ! (S \ {H})c ∪ R1 (H); (ib) there exists a permutation τ from PV(S) to
PV(S) and a swff H ! ∈ S ∩ C3 such that Tab((S \ {H ! })c ∪ R1 (H ! )) = NULL and
(S \{H ! })c ∪R1 (H ! ) = τ ((S \{H})c ∪R1 (H)). Thus by Point (a) applied to H ! , there ex-
ists a Kripke model K H ! = $PH ! , ≤H ! , ρH ! , !H ! & such that ρH ! !(S \{H ! })c ∪R1 (H ! ). By
using τ we can translate K H ! into a model K H = $PH , ≤H , ρH , !H &, where PH = PH ! ,
≤H =≤H ! , ρH = ρH ! and for every world α ∈ PH , if p ∈ PV(S), then α !H τ (p)
iff α !H ! p. By definition of K H , it follows K H ! (S \ {H})c ∪ R1 (H)); (ii) for ev-
ery H ∈ S ∩ C4 , we have two cases: (iia)Tab((S \ {H})c ∪ R1 (H)) = NULL, thus
by induction hypothesis there exists a Kripke model K H = $PH , ≤H , ρH , !H & such
that ρH ! (S \ {H})c ∪ R1 (H). (iib) there exist a permutation τ from PV(S) to
PV(S) and a swff H ! ∈ S ∩ C4 such that Tab((S \ {H ! })c ∪ R1 (H ! )) = NULL and
(S \{H ! })c ∪R1 (H ! ) = τ ((S \{H})c ∪R1 (H)). Thus by Point (a) applied to H ! , there ex-
ists a Kripke model K H ! = $PH ! , ≤H ! , ρH ! , !H ! & such that ρH ! !(S \{H ! })c ∪R1 (H ! ). By
using τ we can translate K H ! into a model K H = $PH , ≤H , ρH , !H &, where PH = PH ! ,
≤H =≤H ! , ρH = ρH ! and for every world α ∈ PH , if p ∈ PV(S), then α !H τ (p) iff
α !H ! p. By definition of K H , it follows K H !(S \{H})c ∪R1 (H)). Let K = $P, ≤, ρ, !&
be a Kripke model defined as follows:
&
P = H∈S∩(C3 S C4 ) PH ∪ {ρ};
& S
≤= H∈S∩(C3 C4 ) ≤H ∪{(ρ, α)|α ∈ P };
&
! = H∈S∩(C3
S
C4 ) !H ∪{(ρ, p)|Tp ∈ S}.
By construction of K, ρ ! S
Case 5: the instruction labeled r5 has been performed. We point out that S ∩ C1 =
S ∩ C2 = S ∩ C3 = S ∩ C4 = S ∩ C5 = ∅. By induction hypothesis there exists a model
K H = $PH , ≤H , ρH , !H & such that ρH ! (S \ {H})c ∪ R2 (H), where H ∈ C6 . Let K =
$P, ≤, ρ, !& be a Kripke defined as follows: P = PH ∪ {ρ}, ≤ = ≤H ∪{(ρ, α)|α ∈ P },
! = !H ∪{(ρ, p)|Tp ∈ S}. By the construction of K, ρ ! S, in particular, by induction
hypothesis ρH ! ¬B and therefore ρH ! ¬(A ∧ B). This implies ρ ! Fc (A ∧ B).
Case 6: the instruction r6 has been carried out. In this case S contains atomic swffs
and swffs of the kind T(p → A) and with Tp ∈ / S. Let K = $P,≤,ρ,!& be the Kripke
model such that P = {ρ} and ρ ! p iff Tp ∈ S. It is easy to show that ρ ! S. As a
matter of fact, if T(p → A) ∈ S, since Tp ∈ / S, ρ ! p therefore ρ ! p → A. /
.
By Lemma 4.1 we immediately get the completeness of Tab.
Theorem 4.2 (Completeness) If A ∈ Int, then Tab({FA}) returns a closed proof
table starting from FA.
5 Implementation and Results
We have implemented Tab as an iterative procedure in C++ language. At present
there are some features that are missing. First, there is no any kind of lexical nor-
malization. This feature, together with backjumping ([Bak95]) and BCP ([Fre95]),
only to give a partial list of the possible optimization techniques, is typical in the-
orem provers and will be one of the changes in the new version of the implementa-
tion. Moreover, when PITP applies C3 and C4 -rules, the search for a permutation pro-
ceeds as follows: let S be a set of swffs and let H and H ! be C3 -swffs in S. PITP
does not perform a full search among the P v(S)! possible permutations. PITP tries
to build a permutation τ such that H = τ (H ! ) and τ = τ −1 . If such a τ fulfills
(S \ {H})c ∪ R1 (H) = τ ((S \ {H ! })c ∪ R1 (H ! )), then τ is used. Otherwise PITP con-
siders that no permutation exists and solves (S \ {H ! })c ∪ R1 (H ! ). Analogously for
C4 -swffs. Since our search is narrow, many permutations are disregarded. This problem
is made worse by the fact that conjunctions and disjunctions are not implemented as
lists of formulas. Thus at present this optimization is applied only to two families of
formulas of ILTP v1.1.1 library. Finally PITP does not implement the search for a
permutation in Points 3 and 6 of Tab. Despite the fact that some optimizations are
ft Prolog ft C LJT STRIP PITP
solved 188 199 175 202 215
(%) 68.6 72.6 63.9 73.7 78.5
proved 104 106 108 119 128
refuted 84 93 67 83 87
solved after:
0-1s 173 185 166 178 190
1-10s 5 6 4 11 10
10-100s 6 7 2 11 9
100-600s 4 1 3 2 6
(>600s) 86 75 47 43 58
errors 0 0 52 29 1
Table 2: ft Prolog, ft C, LJT, STRIP and PITP on ILTP v1.1.1 formulas
SYJ202+1 SYJ205+1 SYJ206+1 SYJ207+1 SYJ208+1 SYJ209+1 SYJ211+1 SYJ212+1
provable provable provable refutable refutable refutable refutable refutable
ft Prolog 07 (516.55) 08 (60.26) 10 (144.5) 07 (358.05) 08 (65.41) 10 (543.09) 04 (66.62) 20 (0.01)
ft C 07 (76.3) 09 (85.84) 11 (481.98) 07 (51.13) 17 (81.41) 10 (96.99) 04 (17.25) 20 (0.01)
LJT 02 (0.09) 20 (0.01) 05 (0.01) 03 (2.64) 08 (0.18) 10 (461.27) 08 (546.46) 07 (204.98)
STRIP 06 (11.28) 14 (267.39) 20 (37.64) 04 (9.3) 06 (0.24) 10 (132.55) 09 (97.63) 20 (36.79)
PITP 09 (595.79) 20 (0.01) 20 (4.07) 04 (11.11) 08 (83.66) 10 (280.47) 20 (526.16) 11 (528.08)
Table 3: ILTP v1.1.1 formulas solved by classes
missing, results in Table 2 (this table is taken from http://www.iltp.de/download/-
ILTP-v1.1.1-prop-comparison.txt) shows that PITP outperforms the known theo-
rem provers on ILTP v1.1.1 library. Within 10 minutes PITP decides 215 out of 274
formulas of ILTP v1.1.1 The library divides the formulas in several families. Every
family contains formulas sharing the same pattern of increasing complexity. In Table 3
SYJ201+1 SYJ202+1 SYJ207+1 SYJ208+1 SYJ209+1 SYJ211+1 SYJ212+1
PITP none 20 (1.29) 03 (0.01) 04 (43.77) 04 (2.50) 10 (596.55) 20 (526.94) 11 (527.72)
PITP -opt1 20 (0.03) 08 (44.59) 04 (44.76) 08 (93.60) 10 (325.93) 20 (558.11) 11 (548.01)
PITP -opt2 20 (1.67) 03 (0.01) 04 (12.18) 04 (2.37) 10 (311.37) 19 (293.34) 10 (88.92)
PITP -opt3 20 (0.03) 08 (44.21) 04 (11.36) 08 (94.30) 10 (591.68) 19 (291.18) 10 (92.05)
PITP ALL 20 (0.03) 08 (45.30) 04 (12.74) 08 (90.11) 10 (297.83) 19 (313.11) 10 (93.18)
Table 4: Comparison between PITP optimizations
(this table is taken from http://www.iltp.de/) for every family (some families of ILTP
v1.1.1 are missing because they are decided within 1s by all provers) we report the index
of the largest formula which every prover is able to decide within 600s CPU time and in
parenthesis the CPU time necessary to solve such a formula. PITP solves all the formu-
las in three families and it is the best prover in three families (SYJ202+1, SYJ206+1,
SYJ211+1), ft-C solves all the formulas of SYJ212+1 and it is the best prover in four
families (SYJ207+1, SYJ208+1, SYJ210+1, SYJ212+1), finally STRIP solves all the
formulas in two families but in no class is it the best prover. Finally we run PITP on our
Xeon 3.2GHz machine to evaluate the effect of using the optimizations described above.
It is well known to people working in ATP that an optimization can be effective for
one class of formulas and be negative for other classes. In Table 4 we compare different
optimizations and give the results of their use on some classes of ILTP v1.1.1 formulas.
First, PITP without optimizations outperforms the other versions of PITP on the fam-
ilies SYJ211+1 and SYJ212+1. To give an idea of the overhead of the optimizations on
formulas where such optimizations do not apply, PITP without optimizations solves the
19th formula of SYJ211+1 in 247.19 seconds and the 10th formula of SYJ212+1 in 76.55
seconds. Among the optimizations the most important seems opt2. When opt2 is not
active the performances decrease. Thus even if this optimization can be used only on
particular classes of formulas, it dramatically influences the performances (in our opin-
ion this gives an idea of the great importance of bounding branching in propositional
intuitionistic logic). With regard to the other optimizations, there are some advantages
in some classes and disadvantages in others. In table 5 we provide the results of the
comparison between PITP and STRIP on twelve thousand random formulas with three
hundred connectives (since the performance of ft-C was worse than STRIP and PITP,
table 5 lacks of ft-C). Given the time limit of five minutes, STRIP does not decide 780
formulas, PITP does not decide 16 formulas.
References
[AFF+ 06] A. Avellone, M. Ferrari, C. Fiorentini, G. Fiorino, and U. Moscato. Esbc: an
application for computing stabilization bounds. ENTCS, 153(1):23–33, 2006.
[AFM04] A. Avellone, G. Fiorino, and U. Moscato. A new O(n lg n)-space deci-
sion procedure for propositional intuitionistic logic. In Andrei Voronkov
Matthias Baaz, Johann Makowsky, editor, LPAR 2002: Short Contributions,
CSL 2003: Extended Posters, volume VIII of Kurt Gödel Society, Collegium
Logicum, 2004.
[Bak95] A. B. Baker. Intelligent Backtracking on Constraint Satisfaction Problems:
Experimental and Theoretical Results. PhD thesis, University of Oregon,
1995.
[BC04] Yves Bertot and P. (Pierre) Castéran. Interactive theorem proving and pro-
gram development: Coq’Art: the calculus of inductive constructions. Texts
in theoretical computer science. Springer-Verlag, pub-SV:adr, 2004.
[Con86] R. Constable. Implementing Mathematics with the Nuprl Proof Development
System. Prentice–Hall, Englewood Cliffs, New Jersey, 1986.
[CZ97] A. Chagrov and M. Zakharyaschev. Modal Logic. Oxford University Press,
1997.
[Dyc92] R. Dyckhoff. Contraction-free sequent calculi for intuitionistic logic. Journal
of Symbolic Logic, 57(3):795–807, 1992.
[ES99] Uwe Egly and Stephan Schmitt. On intuitionistic proof transformations,
their complexity, and application to constructive program synthesis. Fundam.
Inform., 39(1-2):59–83, 1999.
[FFO02] M. Ferrari, C. Fiorentini, and M. Ornaghi. Extracting exact time bounds
from logical proofs. In A. Pettorossi, editor, Logic Based Program Synthesis
and Transformation, 11th International Workshop, LOPSTR 2001, Selected
Papers, volume 2372 of Lecture Notes in Computer Science, pages 245–265.
Springer-Verlag, 2002.
[Fit69] M.C. Fitting. Intuitionistic Logic, Model Theory and Forcing. North-Holland,
1969.
[Fre95] Jon William Freeman. Improvements to propositional satisfiability search
algorithms. PhD thesis, University of Pennsylvania, 1995.
[Hud93] J. Hudelmaier. An O(n log n)-space decision procedure for intuitionistic
propositional logic. Journal of Logic and Computation, 3(1):63–75, 1993.
[Men00] M. Mendler. Timing analysis of combinational circuits in intuitionistic propo-
sitional logic. Formal Methods in System Design, 17(1):5–37, 2000.
[ML84] P. Martin-Löf. Intuitionistic Type Theory. Studies in Proof Theory. Bib-
liopolis, Napoli, 1984.
[MMO97] P. Miglioli, U. Moscato, and M. Ornaghi. Avoiding duplications in tableau
systems for intuitionistic logic and Kuroda logic. Logic Journal of the IGPL,
5(1):145–167, 1997.
[ROK06] Thomas Raths, Jens Otten, and Christoph Kreitz. The ILTP problem library
for intuitionistic logic. release v1.1. To appear in Journal of Automated Rea-
soning, 2006.
provable
0-1s 1-10s 10-200s 200-300s
STRIP 200 19 15 0
PITP 192 36 11 2
unprovable
0-1s 1-10s 10-200s 200-300s
STRIP 10139 404 394 49
PITP 11663 49 27 4
> 300s
STRIP 780
PITP 16
Table 5: PITP and STRIP on random generated formulas
[Sta79] R. Statman. Intuitionistic logic is polynomial-space complete. Theoretical
Computer Science, 9(1):67–72, 1979.
[Wei98] Klaus Weich. Decision procedures for intuitionistic propositional logic by
program extraction. In TABLEAUX, pages 292–306, 1998.