The inverse method is a saturation based theorem proving technique; it relies on a forward proof-search strategy and can be applied to cut-free calculi enjoying the subformula property. Here we apply this method to derive the unprovability of a formula in the modal logic K. To this aim, we design a forward calculus to check the K-satis ability of a set of modal formulas. From a derivation of , we can extract a Kripke model of .
? This work has been partially funded by INdAM-GNCS (Italy). an RK( )-derivation is a set containing formulas constructed using the ones in . Axioms of RK( ) are maximal consistent sets of the set of literals determined by . Rules of RK( ) are inspired by semantics, so that proof-search for a derivation of mirrors the construction of a model of . A remarkable result is that the models extracted from RK( )-derivations are in general \small". This is mainly due to the fact that in forward derivations we can re-use the same premise many times, without duplicating it, and this reduces the generation of redundant worlds. Actually, for every satis able set , we can build a derivation of in RK( ) such that the height of the extracted model is minimal. 2
We consider the language L built from a denumerable set V of propositional variables and the connectives ^, : and . We denote formulas by , , . . . and set of formulas by , , . . . ; is the set f j 2 g. By LCL we denote the set of classical formulas of L, namely the formulas not containing ; with H, X , . . . sets of classical formulas, we call cl-sets. A literal is a formula of the kind p or :p, with p 2 V. A set of literals X is lit-consistent i there is no p 2 V such that fp; :pg X . The set Sf+( ) is the smallest set of formulas such that
Sf+( ) and: { ^ { :( {
2 Sf+( ) implies f ; g Sf+( ); :: 2 Sf+( ) implies ^ ) 2 Sf+( ) implies f: ; : g Sf+( ); 2 Sf+( ) implies 2 Sf+( ); : 2 Sf+( ) implies : 2 Sf+( ); 2 Sf+( ).
Let W be a non-empty nite set of worlds and R be an intransitive successor relation on W (i.e., 8x; y; z(xRy ^ yRz ! :xRz); note that R is irre exive as well). An intransitive tree with root is a triple (W; R; ) such that the re exive and transitive closure of R is a tree partial order on W with root [1]. A model for L is a structure M = hW; R; ; V i, where (W; R; ) is an intransitive tree with root and V , the evaluation function, maps each p 2 V to a subset of W (the set of worlds where p is true). A (classical) interpretation is a subset of V; for w 2 W , by I(w) we denote the interpretation de ned by the propositional variables true at w (i.e., p 2 I(w) i w 2 V (p)). The relation (M; w) j= (the formula is valid in M at world w) is de ned as usual by induction on (see e.g. [1]): { (M; w) j= p, with p 2 V, i w 2 V (p); { (M; w) j= i , for every v 2 W , wRv implies (M; v) j= .
The interpretation of : and ^ is classical. Note that the validity of a classical formula at a world w only depends on I(w). Expressions of the kind ; and ; denote the sets [ f g and [ respectively. By (M; w) j= we mean that, for every 2 , (M; w) j= . A set is (K-)satis able i there exists a model M and a world w of M such that (M; w) j= . It is well-known that the modal logic K is the set of formulas of L such that, for every model M and every world w of M, (M; w) j= (see [1]); accordingly, is valid in K i
Lit
^ 1 J (Tin=1 i) ; f : f j
; ; ; :: ::
; : k ; : k; :( 1 ^ 2) :^
n H j : 2 Sin=1 i g K; H
H 2 Sf+( )g; H no0 9 > > > = > > > ; no n
1 Cl-rules Applied only if the formula introduced in the conclusion belongs to Sf+( ) 9 > > > = > > > ;
Join rules J K = \ Sf+( ) X is a maximal lit-consistent subset of Sf+( ) the set f: g is not satis able. In this paper we present a forward calculus to constructively prove the satis ability of a set of formulas.
The calculus RK( ) is a forward refutation calculus to prove that a nite nonempty set of formulas of L is satis able, meaning that the formula :(V ) is not valid in K. In forward calculi proof-search starts from axioms and rules are applied from premises to the conclusion (forward direction). The rules are displayed in Fig. 1. Axioms of RK( ), introduced by the axiom rule Lit, are the cl-sets X such that X is a maximal lit-consistent subset of Sf +( ), namely: there is no lit-consistent set Y such that X Y Sf+( ). Cl-rules are standard refutation rules for classical connectives; they introduce a formula of the kind generating f^orm)ualansdin::Sf +. (To):gtehtistemrmotinivaattieosn,thweesiodnelycoanddmitiitonruolen athpeplaicpaptliiocnas^ , :( tion of cl-rules. Join rules on and on0 allow one to introduce formulas of the kind and : . The rule on has n + 1 2 premises, where at least one premise H is a cl-set. Rule on0 is the degenerated instance of on only having the premise H. In both cases, the formulas introduced by the rule applications must belong to Sf+( ) (see the de nition of the J : K operator). An RK( )-derivation of is a derivation in RK( ) with the set as root. A set is provable in RK( ) i there exists an RK( )-derivation of such that ; we also say that is proved by .
Given an RK( )-derivation of , we can build a K-model satisfying ; this proves the soundness RK( ). The height of , denoted h( ), is the maximum distance from the root of and an axiom sequent of . We de ne the structure Mod( ) inductively on the height of . { If h( ) = 0, then only consists of an application of Lit and is a maximal lit-consistent subset of Sf +( ). We set Mod( ) = hf g; ;; ; V i, where ; is the empty successor relation and V (p) = f g if p 2 and V (p) = ; otherwise. { If h( ) > 0, let R be the rule applied at the root of .
(
Then Mod( ) = Mod( 0). Note that, if is a derivation of a cl-set H,
only consists of one instance of Lit followed by instances of cl-rules,
accordingly Mod( ) consists of a single world.
(
n+1 W = [ Wi; i=1 n+1 [ Vi; i=1 V =
R = n [ ( Ri [ f ( ; i) g ) i=1 It is easy to check that Mod( ) is a well-de ned model. Moreover, proceeding by induction on the height of one can prove: Theorem 1 (Soundness of RK( )). Let be the root of Mod( ). Then (Mod( ); ) j= be an RK( )-derivation of .
and
We prove that the calculus RK( ) is complete, namely: if is a nite satis able set, then is provable in RK( ). We give a constructive proof by exhibiting how to build an RK( )-derivation of starting from a model M = hW; R; ; V i of . The height of a world w0 2 W , denoted by h(w0), is the maximal length of an R-chain w0Rw1Rw2 : : : ; since hW; R; i is a nite tree, the de nition is well-found. The height of M, denoted by h(M), coincides with h( ). We show that h(Mod( )) h(M); accordingly, we can use RK( ) to generate \small" models of . To formalize this, we introduce the following de nitions: { { If is h-satis able i there is a model M of such that h(M) h.
is satis able, h( ) is the minimum h such that is h-satis able.
The rank Rn( ) of an RK( )-derivation is the maximum number of
applications of rule on along a branch of . Formally, let r be the root rule of and let
1; : : : ; n be the immediate subderivations of . Then:
Rn( ) =
(0 if r is the axiom rule Lit
c + maxf Rn(
c = (1 if r =on 0 otherw.
Note that h(Mod( )) = Rn( ). In the proof of next lemma we show how to build a derivation of a satis able set. Note that Theorem 2 immediately follows from Lemma 1. By j j we denote the number of symbols occurring in . Lemma 1. Let be a nite set of formulas and let satis able set. Then, there exists an RK( )-derivation and Rn( ) h. Moreover, LCL implies LCL. of
Sf+( ) be a hsuch that Proof. We prove the assertion by induction hypothesis (IH) on j j. Since is h-satis able, there exists a model M = hW; R; ; V i and w 2 W such that (M; w) j= and h(w) h. We proceed through a case analysis, only detailing some representative cases.
Case 1: only contains literals.
Let X be the set of literals l 2 Sf+( ) such that (M; w) j= l. Then, X is a maximal lit-consistent subset of Sf +( ), hence X is an axiom of RK( ). Since
X LCL, the assertion holds.
Case 2: = :( 1 ^ 2); 0, with :( 1 ^ 2) 62 0.
Since (M; w) j= :( 1 ^ 2), there exists k 2 f1; 2g such that (M; w) j= : k. Let k = 0 [ f: kg; note that (M; w) j= k, hence k is h-satis able. Since j kj < j j and k Sf+( ), by (IH) there exists an RK( )-derivation k of k such that k k and Rn( k) h. Let be: . . .
k : k; 0;
k = :( 1 ^ 2); 0; Since and Rn( ) = Rn( k) LCL, by (IH) we get k LCL, hence
h, the assertion holds. Moreover, if Case 3: = ; : 1; : : : ; : n; H, with n 1.
Let j 2 f1; : : : ; ng and j = [ f: j g. Since (M; w) j= : j , there exists wj 2 W such that wRwj and (M; wj ) j= : j . We also have (M; wj ) j= , hence j is h(wj )-satis able. Since j j j < j j and j Sf+( ), by (IH) there exists an RK( )-derivation j of j such that j j and Rn( j ) h(wj ), hence Rn( j ) < h. Since H is h-satis able (indeed, (M; w) j= H) and H LCL and jHj < j j, by (IH) there exists an RK( )-derivation c of G such that H G LCL. We can de ne as follows: ... where we leave understood the formulas in the (possibly empty) set . We have . Note that c cannot contain applications of rule on, hence Rn( c) = 0. This implies that Rn( ) = m + 1, where m is the maximum Rn( j ). Since m < h, we get Rn( ) h, and this concludes the proof of this case. tu
As a consequence of the previous lemma we get: Theorem 2 (Completeness of RK( )). Let formulas. Then, there exists an RK( )-derivation that h(Mod( )) h( ). be a of nite set of satis able
such that such k :^
LCL.
k =
k n k
Lit
Lit
no (
Derivation 1
Let = p ^ : p. Note that corresponds to the negation of the transitivity
axiom (
A more signi cant example is given in Fig. 3, where we show an RK(
We have presented the naive forward proof-search strategy; we leave as future
work the investigation of clever strategies (e.g., the use of subsumption to reduce
redundancies) and the implementation of the calculus exploiting the full- edged
Java Framework JTabWb [5]. In this paper we only focus on K; we plan to
extend the techniques here introduced to other modal logics.
(A ^
(
(B ^ (A ^ D)); ::(B ^ (A ^ >>>> B ^ (A ^ D); (C ^ (A ^ E)); > >>: ::(C ^ (A ^ E)); C ^ (A ^ E);
D; :: E 9
D); >>>>
E); >=>> D)); > > > > > > > ; w1: w9: w10: w90: w16: