Automated Natural Deduction for Propositional Linear-time Temporal

Automated Natural Deduction for Propositional Linear-time Temporal Logic∗ Alexander Bolotov Harrow School of Computer Science University of Westminster Watford Road, Harrow HA1 3TP, UK. A.Bolotov@wmin.ac.uk Oleg Grigoriev, Vasilyi Shangin Department of Logic, Faculty of Philosophy Moscow State University, Moscow, 119899, Russia. {shangin,grig}@philos.msu.ru Abstract We present a proof searching technique for the natural deduction calculus for the propositional linear-time tempo- ral logic and prove its correctness. This opens the prospect to apply our technique as an automated reasoning tool in a number of emerging computer science applications and in a deliberative decision making framework across various AI applications. 1 Introduction In this paper we present a proof searching technique for the natural deduction proof system for the proposi- tional linear-time temporal logic PLTL [9] and establish its correctness. The particular approach to build a natural deduction calculus we are interested in is a modification of Quine’s representation of subordinate proof [15] devel- oped for classical propositional and first-order logic. Recall that natural deduction calculi (abbreviated in this paper by ‘ND’) of this type were originally developed by Jaskowski [11], improved by Fitch [8] and simplified by Quine [15]. The ND technique initially defined for classical proposi- tional logic was extended to first-order logic [3, 4] and sub- sequently to the non-classical framework of propositional intuitionistic logic [13]. In [2] it was further extended to capture propositional linear-time temporal logic PLTL and in [5] the ND system was proposed for the computation tree logic CTL. The computer science community has recently become more interested in ND systems [1, 14] mostly due to its potential to represent the goal-directed nature of the proof. This makes the ND method applicable in many AI areas, most notably, in agent engineering [18]. Among other in- teresting and even surprising applications of ND systems is for example their use in the verification of security proto- cols [6]. Obviously, the extension of ND to the temporal ∗This research was partially supported by Russian Foundation for Hu- manities, grant No 06-03-00020a. framework, widely used in agent engineering and verifica- tion, opens broader prospectives for research in ND con- structions. However, from the practical point of view, its success depends on the automation of the proof searching procedure. The latter is the subject of the current paper. We are extending the proof searching technique which was initially developed for the classical case [3, 4], and also extended to intuitionistic logic [13]. We are not aware of any other proof search algorithm for temporal ND systems. For example, the only other ND constructions for linear- time logic [10] and branching-time logic [16] which we are aware of have not been followed by any presentation of the relevant proof searching techniques. Note that while working on the mechanisation of the ND system for PLTL, known as PLTLND, and its correctness we also found a simpler formulation of the underlying ND system. The paper is organized as follows. In §2 we describe PLTLND reviewing the PLTL syntax and semantics in §2.1 and formulating the natural deduction calculus in §2.2. Sub- sequently, in §3, we introduce the main proof-searching pro- cedures (§3.1), the proof-searching algorithm (§3.2), give an example of the algorithmic construction of the proof (§3.3) and provide the correctness argument (§3.4). Finally, in §4, we provide concluding remarks and identify future work. 2 Natural Deduction System PLTLND In this section we review the logic PLTL and the calculus PLTLND. 2.1 Syntax and Semantics of PLTL In the syntax of PLTL we identify a set, Prop, of atomic propositions: p, q, r, . . . , p1, q1, r1, . . . , pn, qn, rn, . . .; classical operators: ¬,∧,⇒,∨, and temporal operators: (‘always in the future’),♦ (‘at sometime in the future’), g (‘at the next moment in time’), and U (‘until’). The set of well-formed formulae of PLTL, wffPLTL is defined as follows. Definition 1 (PLTL syntax) 1. All atomic propositions (members of Prop) are in wffPLTL. 2. If A and B are in wffPLTL, then so are A ∧ B, ¬A, A ∨B, and A⇒ B. 3. If A and B are in wffPLTL, then so are A, ♦A, gA, and AU B. For the semantics of PLTL we utilise the notation of [7]. A model for PLTL formulae, is a discrete, linear sequence of states σ = s0, s1, s2, . . . which is isomorphic to the nat- ural numbers, N , and where each state, si, 0 ≤ i, consists of the propositions that are true in it at the i-th moment of time. If a well-formed formula A is satisfied in the model σ at the moment i then we abbreviate it by 〈σ, i〉 |= A. Be- low, in Figure 1, we define the relation |=, where indices i, j, k ∈ N . 〈σ, i〉 |= p iff p ∈ si, for p ∈ Prop 〈σ, i〉 |= ¬A iff 〈σ, i〉 6|= A 〈σ, i〉 |= A ∧B iff 〈σ, i〉 |= A and 〈σ, i〉 |= B 〈σ, i〉 |= A ∨B iff 〈σ, i〉 |= A or 〈σ, i〉 |= B 〈σ, i〉 |= A⇒ B iff 〈σ, i〉 6|= A or 〈σ, i〉 |= B 〈σ, i〉 |= A iff for each j if i ≤ j then 〈σ, j〉 |= A 〈σ, i〉 |=♦A iff there exists j such that i ≤ j and 〈σ, j〉 |= A 〈σ, i〉 |= gA iff 〈σ, i + 1〉 |= A 〈σ, i〉 |= AU B iff there exists j such that i ≤ j and 〈σ, j〉 |= B and for each k, if i ≤ k < j then 〈σ, k〉 |= A Figure 1. Semantics for PLTL Definition 2 (PLTL Satisfiability) A well-formed for- mula, A, is satisfiable if, and only if, there exists a model σ such that 〈σ, 0〉 |= A. Definition 3 (PLTL Validity) A well-formed formula, A, is valid if, and only if, A is satisfied in every possible model, i.e. for each σ, 〈σ, 0〉 |= A. 2.2 The Calculus PLTLND Here we present the formulation of PLTLND with a slightly different set of rules in comparison with its original formulation in [2]. Namely, now we have two new rules, application of negation to U and ♦ operators, but fewer introduction rules for U (see details below). The core idea of a natural deduction proof technique for a logic L is to establish rules of the following two classes: elimination rules which decompose formulae and introduc- tion rules aimed at constructing formulae, introducing new logical constants. Given a task to prove some formula A of L, we aim at synthesising A. Every proof commences with an assumption and, in general, we are allowed to introduce assumptions at any step of the proof. In the type of natural deduction that we are interested in, assumptions have con- ditional interpretation. Namely, given that a formula A is preceded in a proof by assumptions C1, C2, . . . Cn we in- terpret this situation as follows: if C1, C2, . . . Cn are satis- fiable in L then A is satisfiable in L. Thus, if A is a theorem (a valid formula in L) and we want to obtain its proof then we must interpret A ‘unconditionally’, i.e. it should not de- pend on any assumptions. In our system, the corresponding process is called discarding of assumptions, which accom- panies the application of several introduction rules. As we will see below, in a proof of a theorem in our system the set of non-discarded assumptions should be empty. Another feature of our construction of PLTLND is the use of the labeling technique. In the language of PLTLND we use labeled PLTL formulae and a specific type of expres- sions that use labels themselves, called relational judge- ments. Thus, additionally to elimination and introduction rules, we also establish rules to manipulate with relational judgements. Extended PLTL Syntax and Semantics. We extend the PLTL language by introducing la- bels. Labels are terms, elements of the set, Lab = {x, y, z, x1, x2, x3, . . .}, where x, y, z . . . are variables. When constructing a PLTLND proof, we associate formu- lae appearing in the proof with a model σ described in §2.1 such that labels in the proof are interpreted over the states of σ. Since σ is isomorphic to natural numbers, we can in- troduce the operations on labels: ≃, which stands for the equality between labels, ¹ and ≺, which are syntactic ana- logues of the ≤ and < relation in σ. Thus, ¹ satisfies the following properties: (2.1) For any i ∈ Lab : i ¹ i (reflexivity), (2.2) For any i, j, k ∈ Lab if i ¹ j and j ¹ k then i ¹ k (transitivity). (2.3) For any i, j, k ∈ Lab if i ¹ j and i ¹ k then j ≺ k or k ≺ j or j ≃ k (linearity). (2.4) For any i ∈ Lab, there exists j ∈ Lab such that i ¹ j (seriality). Now, we define a relation Next ⊂ Lab2 : Next(x, y) ⇔ x ≺ y and there is no z ∈ Lab such that x ≺ z and z ≺ y. Next is the ‘predecessor-successor’ relation which sat- isfies the seriality property: for any i ∈ Lab, there exists j ∈ Lab such that Next(i, j). Let ′ abbreviate the operation which being applied to i ∈ Lab gives us i′ ∈ Lab such that Next(i, i′). As we have already mentioned above, now we are able to introduce the expressions representing the properties of re- lations ‘¹’, ‘≺’, ‘≃’ and ‘Next’, and the operation ′ which, following [17], we call relational judgements. Definition 4 (PLTLND Syntax) • If A is a PLTL formula and i ∈ Lab then i : A is a PLTLND formula. • Any relational judgement of the type Next(i, j), i ¹ j, i ≺ j and i ≃ j is a PLTLND formula. Some useful and rather straightforward properties relat- ing operations on labels are given below. (2.5) For any i, j ∈ Lab if Next(i, j) then i ¹ j. (2.6) For any i, j ∈ Lab if i ≺ j then i ¹ j. PLTLND Semantics. For the interpretation of PLTLND formulae we adapt the semantical constructions defined in §2.1 for the logic PLTL. In the rest of the paper we will use capital letters A,B,C,D, . . . as metasymbols for PLTL for- mulae, and calligraphic letters A,B, C,D . . . to abbreviate formulae of PLTLND, i.e. either labelled formulae or rela- tional judgements. The intuitive meaning of i :A is that A is satisfied at the world i. Let Γ be a set of PLTLND formulae, let DΓ = {x|x : A ∈ Γ}, let σ be a model as defined in §2.1 and let f be a function which maps elements of DΓ into N (recall that a PLTL model σ is isomorphic to natural numbers). Definition 5 (Realisation of PLTLND formulae in a model) Model σ realises a set, Γ, if there is a mapping, f , which satisfies the following conditions. (1) For any x ∈ DΓ, and for any A, if x : A ∈ Γ then 〈σ, f(x)〉 |= A, (2) For any x, y, if x ¹ y ∈ Γ, and f(x) = i, and f(y) = j then i ≤ j, (3) For any x, y, if Next(x, y) ∈ Γ, and f(x) = i, and f(y) = j then j = i + 1. The set Γ in this case is called realisable. Definition 6 (PLTLND Validity) A well-formed PLTLND formula,A = i :B, is valid (abbreviated as |=ND A) if, and only if, the set {A} is realisable in every possible model, for any function f . Rules of Natural Deduction System. In Figure 2 we define these sets of elimination and in- troduction rules, where prefixes ‘el’ and ‘in’ abbreviate an elimination and an introduction rule, respectively. Elimination Rules : ∧ el1 i :A ∧B i :A ∧ el2 i :A ∧B i :B ⇒ el i :A⇒ B, i :A i :B ¬ el i :¬¬A i :A ∨ el i :A ∨B, i :¬A i :B Introduction Rules : ∨ in1 i :A i :A ∨B ∨ in2 i :B i :A ∨B ∧ in i :A, i :B i :A ∧B ⇒ in [i :C], i :B i :C ⇒ B ¬ in [j :C], i :B, i :¬B j :¬C Figure 2. PLTLND-rules for Booleans • In the formulation of the rules ‘⇒ in’ and ‘¬ in’ for- mulae [i :C] and [j :C] respectively must be the most recent non discarded [4] assumption occurring in the proof. When we apply one of these rules on step n and discard an assumption on step m, we also discard all formulae from m to n− 1. We will write [m - (n−1)] to indicate this situation. Now, we add an additional rule which is deeply involved into our searching procedure. ¬∨ i :¬(A ∨B) i :¬A ∧ ¬B This rule simply represents one of De Morgan laws and is derivable from the set of classical rules mentioned above. Hence, it is a technical addition, connected with the search- ing procedure. We keep the notions of flagged and relatively flagged la- bel with the meaning similar to the notions of flagged and relatively flagged variable in first order logic [4]. By saying that the label, j, is flagged, abbreviated as 7→ j, we mean that it is bound to a state and, hence, cannot be rebound to some other state. By saying that a variable i is relatively flagged (bound) by j, abbreviated as j 7→ i we mean that a bounded variable, j, restricts the set of runs for i that is linked to it in the relational judgment, for example i ¹ j. Now in Figure 3 we introduce the following rules to ma- nipulate with relational judgements which correspond to the properties (2.1)-(2.6). reflexivity i ¹ i gseriality Next(i, i′) ≺ / ¹ i ≺ j i ¹ j g/ ¹ Next(i, i′) i ¹ i′ transitivity i ¹ j, j ¹ k i ¹ k ¹ linearity i ¹ j, i ¹ k (j ¹ k) ∨ (j ≃ k) ∨ (k ¹ j) Figure 3. PLTLND-rules for relational judge- ments The linearity rule needs some additional comments. Strictly speaking, in the PLTLND language, to avoid unnec- essary complications, we do not allow either Boolean com- bination of relational judgements or their negations. Ob- viously, the conclusion of the ¹ linearity rule violates this constraint. However, it expresses an obvious property of the linear time model structure and to make our presentation more transparent we explicitly formulate a corresponding rule. Our justification here is very simple: the only way in which the conclusion of this rule is involved into the con- struction of the proof is reasoning by cases - see more de- tails in the discussion of the relevant searching rule (5.2) in §3.1. Next, in Figures 4 and Figures 5 we define elimination and introduction rules for the temporal logic operators and the induction rule. ⋆ When applying gel the conclusion i′ : A becomes marked by M1. This affects other rules: - the condition ∀C(j : C 6∈ M1) in the rules ♦el, U el1 means that the label j should not occur in the proof in any formula, j :C, that is marked by M1, - the condition j :A 6∈M1 in the rule in means that j :A is not marked by M1. ⋆⋆ In U el2 the expression i[AB] is used with the follow- ing meaning: a variable i in the proof can be marked with [AB] if it has been introduced in the proof as a result of the application of the rule U el1 to i :AU B. ⋆ ⋆ ⋆ In in and the induction rules formula i ¹ j must be the most recent assumption and a variable j is new in a derivation; applying the rule on the step n of the proof, we discard i ¹ j and all subsequent formulae until the step n. Finally, we add two more rules which are also deeply involved into our searching procedure. el i : A, i ¹ j j :A ♦el i :♦A i ¹ j, j :A ∀C(j :C 6∈M1) 7→ j, j 7→ i gel⋆ i : gA i′ :A i′ :A ∈M1 U el1 i :AU B, i :¬B i :A, j :B, i ≺ j ∀C(j :C 6∈M1) 7→ j, j 7→ i U ⋆⋆el2 i[AB] ¹ j[AB], i[AB] ¹ k, k ≺ j[AB] k :A Figure 4. Elimination rules for temporal oper- ators in⋆⋆⋆ j :A, [i ¹ j] i : A j :A 6∈M1 7→ j, j 7→ i ♦in i :A i :♦A g in i′ :A, Next(i, i′) i : gA U in i :B i :AU B Induction ⋆⋆⋆ i :A [i ¹ j] j :A⇒ gA i : A j :A 6∈M1 7→ j, j 7→ i Figure 5. Introduction rules for temporal op- erators ¬U i : ¬(AU B) i : ¬B ∨ ¬B U (¬A ∧ ¬B) ¬♦ i : ¬♦A i : ¬A While the first rule, ¬U is not derivable from the set of rules for temporal operators given above, the second rule, ¬♦ can be easily derived from them. However, the addi- tion of these rules as part of the main rules of the system significantly simplifies our searching procedure. Note also that together with the use of fewer introduction rules for U , it also leads us to a new ND formulation of PLTL. Definition 7 (PLTLND proof) An ND proof of a PLTL formula B is a finite sequence of PLTLND formulae A1,A2, . . . ,An which satisfies the following conditions: • everyAi (1 ≤ i ≤ n) is either an assumption, in which case it should have been discarded, or the conclusion of one of the ND rules, applied to some foregoing for- mulae, • the last formula, An, is x :B, for some label x, • no variable - world label is flagged twice or relatively binds itself. When B has a PLTLND proof we will abbreviate it as ⊢ND B indicating that B is a theorem. Theorem 1 [PLTLND Soundness] PROOF: The new rule, ¬U , introduced into the system, is based on the similar equivalence, ¬AU B ≡ ¬B ∨ ¬B U (¬A∧¬B). Similarly, the second rule, ¬♦, is based on the following famous equivalence relating the and♦ operators ¬♦A ≡ ¬A. It is an easy exercise to show that both of these new rules preserve satisfiability. This, together with the soundness theorem of the original formu- lation of the ND system in [2], gives us the soundness of the new formulation. (END) Theorem 2 [PLTLND Completeness] PROOF: We can also show that with the addition of the new rules, ¬♦ and ¬U , we are able to prove all the theorems of the logic PLTL. This completeness proof would be very similar to that contained in [2] being different only in estab- lishing the fact that all the axioms of PLTL are derivable in a new system with these new rules. (END) 3 ND-proof Searching Technique The proof searching strategy is goal-directed. The core idea behind it is the creation of the two sequences of formu- lae: list proof and list goals. The first sequence represents formulae which form a proof. In the second sequence we keep track of the list of goals. Here, each goal is either a formula or two arbitrary contradictory formulae. We will abbreviate this designated type of goal by⊥. An algo-proof is a pair (list proof, list goals) whose construction is deter- mined by the searching procedure described below. At each step of constructing an algo-proof, a specific goal is cho- sen, which we aim to reach at the current stage. Thus, the appropriate name for such a goal would be a current goal. The first goal of list goals is extracted from the given task, we will refer to this goal as to the initial goal. Definition 8 (Reachability of a current goal) A cur- rent goal, Gn, 0 ≤ n, occurring in list goals= 〈G1, G2, . . . , Gn〉, is reached if the following condi- tions are satisfied: • If Gn 6= ⊥ then Gn is reached if there is a formula A in list proof such thatA is not discarded andA = Gn, else • Gn is ⊥ and it is reached if – there are two non-discarded contradictory for- mulae i :A and i :¬A (for some i) in list proof. – ⊥ is derived in each of three tasks following Pro- cedure (2.2.6), reasoning by cases (see §3.1). In general, when we construct a proof, we check whether the current goal has been reached. If it has been reached then we apply the appropriate introduction rule, and this is the only reason for the application of introduction rules. As we will see later, such an application of an introduction rule is absolutely determined by the structure of the previ- ous goal and by the formulation of introduction rules. Al- ternatively, (if the current goal has not been reached), we continue searching for a possible update of list proof and list goals. Note that the construction of these sequences is determined either by the structure of the current goal, or by the structure of complex formulae occurring within list proof. Additionally, we introduce a mechanism of mark- ing formulae within list proof and list goals to prevent an infinite application of searching rules. Now we describe a set of procedures which guide the construction of an algo-proof. 3.1 Proof-Searching Procedures Procedure 1. Here we update a sequence list proof by searching (in a breadth-first manner) for an applicable elim- ination rule, ¬♦, ¬U or ¬∨ rules. If we find a formula, or two formulae, which can serve as premises of one of these rules, the rule is enforced and the sequence list proof is up- dated by the conclusion of the rule. We apply these rules in the following order: rules to eliminate a Boolean operation, ¬♦, ¬U , ¬∨, U el,♦el, and, finally, el. Note that el applies to some formula i : A any time when the new label j appears in the list proof such that i ≤ j. Procedure 2. Here a new goal is synthesized in a backward chaining style following one of the subprocedures described below. They apply