NONCLAUSAL RESOLUTION SYSTEM FOR BRANCHING TEMPORAL LOGIC

Jūratė Sakalauskaitė

Institute of Mathematics and Informatics Akademijos 4, 2600 Vilnius, Lithuania e-mail: jurate.sakalauskaite @mlats.mii.lt

Abstract. We present a proof system for branching propositional temporal logic. The system is based on nonclausal resolution. The system is proved to be complete. The proof of completeness uses tableau construction for the logic.

1. Introduction

Temporal logic is an appropriate formalism to reason about concurrent systems. We consider here the branching propositional temporal logic BPTL, i.e. in underlying model of the logic any instant of time may split into different possible futures. Branching time logic allows to reason about different possible futures. BPTL is a subsystem of branching time logic introduced in [BPM]. The language of BPTL contains the usual propositional connectives (say ∧, ∨, ℸ, ⊃) and temporal modalities. Time is assumed discrete and branching. In BPTL if u and v range over formulas then

• ◯ u means ”u is true in each next state”;

• ⊚ u means ”u is true in some next state; in other words ⊚u ≡ ℸ◯ℸu;

• □ u means ”u is always true (from now on )”;

• ♢ u means ”u is eventually true”; in other words ♢u ≡ ℸ□ℸu.

For BPTL a Hilbert style proof system can be obtained as a subsystem of Hilbert style proof system presented in [BPM].

In this paper we present nonclausal resolution proof system for BPTL. Nonclausal resolution has the advantage over the classical clausal resolution of not requiring formulas to be in clause form. The proof of completeness uses tableau construction for BPTL extracted from [BPM]. The idea to use tableau construction to prove completeness of nonclausal resolution proof system is adopted from [AM].

In section 2 we present syntax and semantics of BPTL. In section 3 we introduce a nonclausal resolution system ℝ and explore soundness issues. In section 4 we present the proof of completeness of ℝ. Section 5 contains some concluding remarks.

2. Syntax and semantics of BPTL

Formulas are defined as usual with the help of propositional connectives ∧, ∨, ⊃ and temporal modalities ◯, ⊚, □, ♢.

A model for BPTL is a triple (S, P, R), where S is a set of states, P is an assignment of propositional letters to states and R is a binary relation on states such that for each s ∈ S there is t ∈ S (s, t) ∈ R. For a propositional letter a and a state s ∈ S, a ∈ P (s) iff a is true in s. We extend the interpretation over the model to all formulas in BPTL as follows, where b = (s = s_{0}, s_{1}, …, s_{i}, …) is an infinite path through the model such that s_{i}Rs_{i+1}.

1. s ⊧ a iff a ∈ P (s) for a atomic;

2. s ⊧ ℸp iff s ⊭ p;

3. s ⊧ p ∨ q iff s ⊧ p or s ⊧ q;

4. s ⊧ □p iff ∀b ∀t (t ∈ b implies t ⊧ p);

5. s ⊧ ◯p iff ∀t (sRt implies t ⊧ p);

6. s ⊧ ♢p iff ∃b ∃t (t ∈ b implies t ⊧ p);

7. s ⊧ ⊚p iff ∃t (sRt implies t ⊧ p).

p is satisfiable iff s ⊧ p for some model M and some state s in M. p is valid iff s ⊧ p for each model M and each state s in M.

3. The resolution system for BPTL

In this section we describe a nonclausal resolution proof system ℝ for BPTL.

3.1 Preliminaries

The sequence of formulas S_{0}, …, S_{n} is a derivation of S_{n} from S_{0} if, for all i, S_{i+1} is obtained from S_{i} by rules of the system. We refer to the S_{i} as a derivation step. In the special case, where S_{n} = false, the sequence S_{0}, …, S_{n} is a refutation of S_{0}. A proof of the formula w is a refutation of ℸw. We write ⊢ w to denote that formula w has a proof within ℝ.

The resolution system in this paper consists of simplification rules and deduction rules. We also use the recursive-call mechanism which enables to apply rules to subformulas of a proof step.

We define the set of conjuncts of a formula u as follows: u is a conjunct of u, and if u is of the form u_{1} ∧ u_{2}, then conjuncts of u_{1} and the conjuncts of u_{2} are conjuncts of u.

• Simplification rules

These rules simplify formulas, or put them in forms where the other rules can be applied. They are all of the form

u_{1}, …, u_{m} ⇒ v.

The rule u_{1}, …, u_{m} ⇒ v can be applied to a formula S_{i}, if the formulas u_{1}, …, u_{m} occur as conjuncts in S_{i}. Then in order to obtain corresponding derivation step we delete one occurrence of each u_{i} and add the derived formula v to the conjunction.

• Deduction rules.

The deduction rules have a form

u_{1}, …, u_{m} ⟼ D.

The rule u_{1}, …, u_{m} ⟼ v can be applied to a formula S_{i}, if the formulas u_{1}, …, u_{m} occur as conjuncts in S_{i}. Then, in order to obtain corresponding derivation step, add the derived formula v to the conjunction.

•Polarity.

An occurrence of a subformula has positive polarity in a formula if it is embedded in the scope of an even number of explicit or implicit ℸ′s.

•The recursive-call mechanism.

The recursive-call mechanism for BPTL is: if there is a derivation of v from u then we may take S_{i+1} to be S_{i}, with a positive occurrence of u replaced with v.

Usually, we do not mention the recursive-call mechanism in our proofs. Instead we mention the simplification and deduction rules that enables us to apply.

3.2 Soundness For our proof notion to be meaningful we require that rules be sound, i.e., that they maintain satisfiability: if S_{0} is satisfiable, then S_{n} is satisfiable.

The following lemma is helpful in proving soundness of the system.

Lemma 3.1. If u ⊃ v is valid and w_{1} is the result of replacing in w one positive occurrence of u with v, then w ⊃ w_{1} is valid.

Proof. By induction on complexity of w. Each of simplification rules and deduction rules of ℝ has the property

that

(u_{1} ∧ … ∧ u_{m}) ⊃ v

is valid.

This guarantees the soundness of ℝ:

Theorem 3.2(soundness) Assume that (u_{1} ∧ … ∧ u_{m}) ⊃ v is valid for all simplification rules and all deduction rules. If there is a derivation of S_{n} from S_{0} and S_{0} is satisfiable, then S_{n} is satisfiable.

Proof. By induction on the depth of recursive calls in the derivation.

3.3 rules of the system ℝ

3.3.1 Simplification rules

• True-false reduction rules

These rules include

□ true ⇒ true ♢ true ⇒ true □ false ⇒ false ♢ false ⇒ false ◯ true ⇒ true ⊚ true ⇒ true ◯ false ⇒ false ⊚ false ⇒ false

and the regular true-false reduction rules in propositional logic such as false ∧u ⇒false, etc. .

• Weakening rules

u, v ⇒ u, u, v ⇒ v.

• Negation rules

\begin{matrix}ℸ□u ⇒ ♢ℸu,  ℸ♢u ⇒ □ℸu, \\ ℸ◯u ⇒ ⊚ℸu,  ℸ ⊚ u ⇒ ◯ℸu. \end{matrix}

\begin{aligned}ℸ(u ∨ v) & ⇒ (ℸu ∧ ℸv), \\ ℸ(u ∧ v) & ⇒ (ℸu ∨ ℸv), \\ ℸℸu & ⇒ u. \end{aligned}

Similar rules are added for the other connectives.

3.3.2 Deduction rules

•Resolution rule

To state this rule , we introduce some substitution notation. We write u < v > to indicate that the formula v occurs in u, and then u < w > denotes the result of replacing exactly one occurrence of v with w in u. We write u < v_{1}, …, v_{n} > to indicate that each of v_{1}, …, v_{n} occurs in u ,and then u < w > denotes the result of sequentially replacing exactly one occurrence of each of v_{1}, …, v_{n} with w in u.

The nonclausal resolution rule for propositional logic is

A < u >, B < u >⟼ A < true > ∨B < false > .

That is, if the formulas A < u, …, u > and B < u, …, u > have a common subformula u, then we can derive the resolvent A < true > ∨B < false >. This is obtained by replacing certain occurrences of u in A < u, …, u > with true and certain occurrences of u in B < u, …, u > with false, and taking the disjunction of the results. (Here ”certain occurrences” means ”one or more occurrences”).

As noted in [AM] this rule does not carry over to linear propositional temporal logic .It does not carry to branching propositional temporal logic as well. The reason is that while u occurs in both A and B, it need not denote the same truth value in all its occurrences; intuitively, each occurrence of u may refer to different instants of time.

The resolution rule is sound in ℝ under the following restriction: the occurrences of u in A or B that are substituted by true or false, respectively, are all in the scope of the same number of ◯’s and ⊚’s and not in the scope of any □ or ♢ in A or B; and all these occurrences of u may be except one are in the scope of only ◯’s, each of which occurs with positive polarity.

For example, consider the formulas

\begin{matrix}A : ◯ ⊚ □p ∧ ♢□p and \\ B : ◯◯□p ∧ ⊚◯□p. \end{matrix}

Taking u to be □p the rule allows us to derive the resolvent

(◯ ⊚ true ∧ ♢□p) ∨ (◯◯false ∧ ⊚◯□p).

We only substituted true or false for those occurrences in the scope of ◯⊚ and ◯◯. We cannot substitute the other occurrence of □p in A, since it is in the scope of ♢. Also, we cannot substitute the other occurrence of □p in B, since we substituted □p in ◯ ⊚ □p in A, which is in the scope of ◯⊚, but not in the scope of ◯◯.

• Modality rules

These are rules to handle formulas in the scope of □, ♢, ◯, ⊚.

• □ rule: □u ⟼ u ∧ ◯□u;

• ♢ rule: ♢u ⟼ u ∨ ⊚♢u;

• ◯◯ rule: ◯u, ◯v ⟼ ◯(u ∧ v);

• ⊚◯ rule: ⊚u, ◯v ⟼ ⊚(u ∧ v). •Induction rule

if ⊢ ℸ(w ∧ u), then

w, ♢u ⟼ ♢(ℸu ∧ ⊚(u ∧ ℸw)).

• Distribution rule

u, v_{1} ∨ … ∨ v_{n} ⟼ (u ∧ v_{1}) ∨ … ∨ (u ∧ v_{n}).

One can write similar rules for the other propositional connectives, e.g. ⊃.

3.4 An example. Let us prove the validity of the formula

(p ∧ □(p ⊃ ◯p)) ⊃ □p.

In other words , we refute

ℸ(ℸ(p ∧ □(p ⊃ ◯p)) ∨ □p.

The negation rules yield

(p ∧ □(p ⊃ ◯p)) ∧ ♢ℸp.

Since ⊢ ℸ(p ∧ ℸp), we apply the induction rule and weakening to derive

♢(p ∧ ⊚ℸp) ∧ □(p ⊃ ◯p).

Since ⊢ ℸ(□(p ⊃ ◯p) ∧ (p ∧ ⊚ℸp)) (as we check later), as above we derive

♢(ℸ(p ∧ ⊚ℸp) ∧ ⊚((p ∧ ⊚ℸp) ∧ ℸ□(p ⊃ ◯p)) ∧ □(p ⊃ ◯p).

By weakening this yields

♢ ⊚ (ℸ□(p ⊃ ◯p)) ∧ □(p ⊃ ◯p).

Since ⊢ ℸ(⊚(ℸ□(p ⊃ ◯p)) ∧ □(p ⊃ ◯p)) (as we check later), as above we derive

♢(ℸ(⊚(ℸ□(p ⊃ ◯p))) ∧ ⊚ ⊚ ℸ□(p ⊃ ◯p)).

By □ rule and weakening this yields

♢(ℸ(⊚(ℸ◯□(p ⊃ ◯p))) ∧ ⊚ ⊚ ℸ□(p ⊃ ◯p)).

By negation rule and weakening this yields

♢(◯◯□(p ⊃ ◯p) ∧ ⊚ ⊚ ℸ□(p ⊃ ◯p)).

We apply the resolution rule (taking A = ◯◯□(p ⊃ ◯p))), B = ⊚⊚ℸ□(p ⊃ ◯p) and u = □(p ⊃ ◯p) to derive

♢◯◯false ∨ ⊚ ⊚ ℸtrue,

and then by simplification and weakening

♢false.

And then

false.

We still have to show a) ⊢ □(p ⊃ ◯p) ∧ (p ∧ ⊚ℸp) and b) ⊢ ℸ(⊚(ℸ□(p ⊃ ◯p)) ∧ □(p ⊃ ◯p)) to justify the application of the induction rule in this proof. We show a). b) is left to the reader. We apply □ rule and weakening to derive

(p ⊃ ◯p) ∧ (p ∧ ⊚ℸp).

By distribution rule and weakening this yields

(ℸp ∧ p ∧ ⊚ℸp) ∨ (◯p ∧ p ∧ ⊚ℸp).

We apply twice the resolution rule to derive

ℸtrue ∨ (false ∧ ⊚ℸp) ∨ (◯false ∨ (p ∧ ⊚ℸtrue)).

Negation rules and simplifications yield

false.

4.Completeness of ℝ

In this section we prove that the resolution system R is complete.

Theorem 4.1(completeness) Every valid BPTL formula is provable in the resolution system ℝ.

Proof. Our strategy as in [AM] is to show that any tableau proof can be transformed into a resolution proof. In other words, if the tableau decision procedure finds ℸu of BPTL unsatisfiable, then ℸu has a refutation. If n is a node of the tableau then U_{n} denotes the set of formulas at n. We prove a more general fact:

for every node n in the tableau for u ,if n is eliminated, then ∧U_{n} has the refutation.

The proof is by complete induction on the stage at which nodes are eliminated by the tableau decision procedure.(In other words ,the rank of a node is the stage at which it is deleted).

We recall the definition of a tableau construction for u and the tableau decision procedure ([BPM]). Formulas are classified as α-formulas and β -formulas

α  α_{1}  α_{2}
p∧q  p  q
□p  p  ◯□p
β  β_{1}  β_{2}
p∨q  p  q
♢p  p  ⊚♢p.

Tableau construction and decision procedure. Let u be BPTL formula. Let n_{0} be

the root of T and let U_{n_{0}} = {ℸu, □ ⊚ true}. T, the tableau for ℸu, is constructed inductively by applying the following rules to nodes which are leaves of T.

R_{α}: if α ∈ U_{n}, then create a son n_{1} of n and define
U_{n_{1}} = U_{n} ∪ {α_{1}, α_{2}}.
R_{β}: if β ∈ U_{n}, then create two sons n_{1}, n_{2} of n and define
U_{n_{i}} = U_{n} ∪ {β_{i}}, i = 1, 2.

R_{⊚} : let V_{n} = {⊚p_{1}, …, ⊚p_{k}, ◯q_{1}, … ◯q_{m}} be the set of next time formulas in parent n. Create k sons n_{i}, i = 1, …, k of n and define

U_{n_{i}} = {p_{i}, q_{1}, …, q_{m}}.

Notation. If the R_{α}/R_{β}/R_{⊚}-rule was applied at node n, the n is called α/β/⊚- node. Root and sons of ⊚-node are called pre-states. ⊚-node is called a state.

The construction of T is made finite by introducing the following two termination rules:

1. if p ∈ U_{n} and ℸp ∈ U_{n}, then this node is called closed and is not expanded further.

2. if a node m is about to be created as a son of an ⊚-node n and there is an ancestor n′ of n such that n′ is an immediate descendant of a ⊚-node and U_{n′} = U_{m}, then do not create m but instead connect n to n′ with ”feedback” edge.

A node of T is eliminated in the following three cases:

1) it contains a proposition and its negation;

2) it is α- or β-node and all of its descendants have been eliminated; it is ⊚-node and one of its descendants have been eliminated;

3) if the node is a pre-state and contains ♢v and on no path from the node do v occurs. ℸu is found unsatisfiable if and only if all nodes of the tableau have been eliminated. Consider a node n. Assume that if the node m has already been eliminated

then ∧U_{m} has a refutation, and suppose that n is eliminated. To prove completeness we show that U_{n} is refuted in R. We analyse three cases; they correspond to the three possible reasons why n can be eliminated.

Lemma 4.1. 1) If U_{n} contains p and ℸp then ∧U_{n} can be refuted in R;

2) if n is α/β/⊚-node and ∧U_{n_{1}} is refuted in ℝ/ ∧ U_{n_{1}} and ∧U_{n_{2}} are refuted in ℝ/ ∧ U_{n_{i}} for some i is refuted in ℝ then ∧U_{n} can be refuted in ℝ.

Proof. In case 1) ∧U_{n} = p ∧ ℸp ∧ ϕ for some formula ϕ. We derive false by resolution on p and simplifications.

We consider 2).

• Let U_{n_{1}} be created from U_{n} by α-rule. Then p ∧ q ∈ U_{n} and U_{n_{1}} = U_{n} ∪ {p, q} or □p ∈ U_{n} and U_{n_{1}} = U_{n} ∪ {p, ◯□p}. Assume, there is a refutation of ∧U_{n_{1}} to show that there is a refutation of ∧U_{n}. In both cases the refutation of ∧U_{n_{1}} can be extended to the refutation of U_{n}.

• Let U_{n_{1}} and U_{n_{2}} be obtained from U_{n} by β-rule. Then p ∨ q ∈ U_{n} or ♢p ∈ U_{n}. In the first case (∧U_{n_{1}})∨(∧U_{n_{2}}) is obtained from ∧U_{n} by the distribution rule . In the second case (∧U_{1}) ∨ (∧U_{n_{2}}) is obtained from ∧U_{n} by applying ♢-rule and next the distribution rule. Assume there is a refutation of ∧U_{n_{1}} and ∧U_{n_{2}}, to show there is a refutation of ∧U_{n}. In both cases the refutation of U_{n_{1}} and U_{n_{2}} can be extended to the refutation of U_{n}.

• Let U_{n_{i}} be created from U_{n} by ⊚-rule. Then ∧U_{n} = ⊚p_{1} ∧ … ∧ ⊚p_{k} ∧ ◯q_{1} ∧ … ∧ ◯q_{l} ∧v_{1} ∧…∧v_{m}, where v_{i}’s are not of the form ◯w or ⊚w and ∧U_{n_{i}} = p_{i} ∧q_{1} ∧…∧q_{l}. Assume there is a refutation of ∧U_{n_{i}} in ℝ. The following lines are refutation of

∧U_{n} in ℝ.

1. ⊚p_{1} ∧ … ⊚ p_{k} ∧ ◯q_{1} ∧ … ∧ ◯q_{l} ∧ v_{1} ∧ … ∧ v_{m} ∧U_{n}

2. ⊚p_{i} ∧ ◯q_{1} ∧ … ∧ ◯q_{l}  by weakening from 1.
3. ⊚p_{i} ∧ ◯(q_{1} ∧ … ∧ q_{l})  by ◯◯-rule and weakening from 2.
4. ⊚(p_{i} ∧ q_{1} ∧ … ∧ q_{l})  by ⊚◯-rule and weakening from 3.

⋮

S. ⊚ false  by assumption on

U_{n_{i}}.

S+1. false  by simplification

from S.

Lemma 4.2. If a node n is a prestate which contains ♢v and on no path from the node do v occurs, then ∧U_{n} can be refuted in R.

To prove lemma 4.2 we prove some auxiliary lemmas.

Let [n]^{∗} be the set of prestates accessible from n by choosing at ⊚-node the son corresponding to ⊚♢v. Then ♢v ∈ U_{n} and on no path from u ∈ [n]^{∗} do v occurs. Let Y_{u}, u ∈ n ∪ [n]^{∗}, denote a part of prestate u obtained by erasing ◯’s in a state preceding u. We call Y_{u} universal next time part of u. We will want to construct universal next time parts of prestates in [n]^{∗}. More precisely, we get w_{i}’s that say what universal next time parts of prestates at depth i counting from n will be true then. We call w_{i} the i-th fringe. For example, if U_{n} = {□(◯q ∨ ⊚q_{1}), ♢v},

then w_{1} = ◯(q ∧ □(◯q ∨ ⊚q_{1})) ∨ ◯□(◯q ∨ ⊚q_{1}), where (q ∧ □(◯q ∨ ⊚q_{1}), □(◯q ∨ ⊚q_{1}), are

universal next time parts of prestates at depth 1 in [n]^{∗}

Lemma 4.2.1. Given a prestate n ℝ can derive formulas w_{i} built from the universal next time parts p_{i}^{l} of prestates from [n]^{∗} at depth i from Y_{n} with ∨ and ◯. Furthermore, each p_{i}^{l} occurs in the scope of exactly i ◯’s.

Proof. Put w_{o} = ∧Y_{n}. We show how to obtain w_{i+1} from w_{i}. Let Y_{t} be a universal next time part of a prestate t ∈ [n]^{∗} in w_{i} at depth i. Then U_{t} = Y_{t} ∪ ♢v.

Let [t] be the states accessible from t by α, β nodes which include ⊚♢v. We will show that we derive ∨_{u∈[t]} ∧(U_{u} − {⊚♢v}) from Y_{t} = ∧(U_{t} − {♢v}) in ℝ. In fact

applying □−, ♢-rules and distribution rule we derive ∨_{u∈[t]^{+}}(∧U_{u}) from U_{t}, where

[t]^{+} is all states accessible from t by α, β nodes, i.e. [t]^{+} is obtained from [t] by adding states which include v. But these states are eliminated, so refuted by induction. Thus we derive ∨_{u∈[t]}(∧U_{u}) from ∧U_{t}. Hence we derive ∨_{u∈[t]}(U_{u} − {⊚♢v})

from ∧(U_{t} − ♢v). By weakening we drop from U_{u} all the formulas other than prefixed with ◯. So we derive ∨_{u∈[t]}( ∧_{p∈Y_{u}} ◯p). Apply ◯◯-rule to pull ◯’s out of

conjunction. We derive ∨_{u∈[t]}(◯ ∧_{p∈Y_{u}} p). Applying this procedure to all universal

next time parts at depth i from w_{i} we derive w_{i+1}.

Lemma 4.2.2. Given a prestate t ∈ n ∪ [n]^{∗} ∧Y_{t} ∧ v can be refuted in ℝ.

Proof. U_{t} = Y_{t} ∪ {♢v} as mentioned above. Without loss of generality we can assume that β rule was applied to ♢v at t to construct sons t_{1}, t_{2}. Then U_{t_{1}} = {U_{t} − {♢v}} ∪ {v} = Y_{t} ∪ {v}. But t_{1} have been eliminated; otherwise we have path with v from n. Thus U_{t_{1}} is refuted in ℝ by induction.

Lemma 4.2.3. For any i ⩾ 0 ⊢ ℸ(w_{i} ∧ ⊚^{i}v).

Proof. For i = 0 distribute v by the distribution rule and apply lemma 4.2.2. For i > 0 distribute ⊚^{i}v by the distribution rule. Next use ⊚◯- rule to push v inwards. Then we obtain conjunctions of universal next time parts of prestates in the depth i from n∪[n]^{∗} with v. Applying lemma 4.2.2 we obtain the refutation of this conjunctions. Then applying reduction rules false ∨A → A, ⊚ false → false we obtain refutation of w_{i} ∧ ⊚^{i}v.

The lemma 4.2.4 is the main lemma of completeness proof.

Lemma 4.2.4. If for all i ⊢ ℸ(w_{i} ∧ ⊚^{i}v), then ⊢ ℸ ∧ U_{n}.

Proof. ∧U_{n} = ∧Y_{n} ∧ ♢v by assumption. Assume ⊢ ℸ(w_{i} ∧ ⊚^{i}v), for alli. We put w_{0} = ∧Y_{n}. From w_{0} and ♢v, by the induction rule and weakening we derive

♢ ⊚ (v ∧ ℸw_{0})

since ⊢ ℸ(w_{0} ∧ v) by assumption. By lemma 4.2.1 we can derive w_{1}. Furthermore, ⊢ ℸ(w_{1} ∧ ⊚v) by assumption. Thus ⊢ ℸ(w_{1} ∧ ⊚(v ∧ ℸw_{0})). This by the induction rule yields

♢ ⊚ (⊚(v ∧ ℸw_{0}) ∧ ℸw_{1}).

In general, we can get all w_{i}’s and we have that ⊢ ℸ(w_{i} ∧ ⊚^{i}v), by assumption. Successive applications of the induction rule will give

♢ ⊚ (⊚(… ⊚ (v ∧ ℸw_{0}) ∧ …) ∧ ℸw_{m−1}) ∧ ℸw_{m})

for any m.

We weaken this to

♢ ⊚ (⊚(… ⊚ (ℸw_{0}) ∧ …) ∧ ℸw_{m−1}) ∧ ℸw_{m})

Call this formula Ψ_{m} and define also Ω_{m} by Ψ_{m} = ♢Ω_{m}.

The finite model property tells us that there are only finitely many universal next time parts generated from w_{0}. Thus for some s we have all universal next time parts generated from w_{0} in ℝ. We check that ⊢ ℸ(w_{0} ∧ Ω_{s}). Take s + 1-th fringe w_{s+1} of w_{0}. Each universal next time part Y in w_{s+1} is in the scope of s + 1 of ◯’s and it is denied in Ω_{s}. Furthermore ℸY is in the scope of s + 1 of ⊚’s in Ω_{s}. Applying the resolution rule we obtain false derived from w_{0} ∧ Ω_{s}, i.e. w_{o} ∧ Ω_{s} has the refutation in ℝ. Thus we can apply the induction rule (and weakening) once more and get

♢(ℸΩ_{s} ∧ ⊚Ω_{s}).

Call this formula ϕ. ϕ says that at each point in depth s + 1 we are in one of universal next time prestates reachable from w_{0} and that there are the next instant we are in none of them. Of course, this cannot be the case; in fact, we can refute ℸΩ_{s} ∧⊚Ω_{s} : we derive the first fringe of all universal next time parts of prestates in ℸΩ_{s} and check that universal next time parts of prestates in these fringes were already in Ω_{s}. Thus by the resolution rule we derive ♢ false and hence false.

Proof of lemma 4.2. From lemma 4.2.3 and lemma 4.2.4 we obtain that ∧U_{n} can be refuted in R.

5. Concluding remarks

We have presented a nonclausal resolution approach to theorem proving in BPTL with temporal modalities ◯, ⊚, □, ♢. We show that presented system is complete. We expect to generalize this approach to get nonclausal resolution system for branching temporal logic with modality Until.

References

[AM] (1990) Abadi M. and Z.Manna, Nonclausal deduction in first order temporal logic, Journal of ACM 37, 2, 279-317.

[BPM] (1983) Ben-Ari M., A.Pnueli and Z.Manna, The temporal logic of branching time, Acta Informatica 20, 207–226.