# zbMATH — the first resource for mathematics

A resolution method for temporal logic. (English) Zbl 0745.68091
Artificial intelligence, IJCAI-91, Proc. 12th Int. Conf., Sydney/Australia 1991, 99-104 (1991).
[For the entire collection see Zbl 0741.68016.]
The paper describes a resolution procedure for discrete, linear, propositional temporal logic. The logic incorporates both past-time and future-time temporal operators, and its models consist of sequence of states, each sequence having finite past and infinite future. The approach is to rewrite arbitrary temporal formulae, incorporating both past-time and future-time temporal operators, into Separated Normal Forms (SNF) formulae. An SNF temporal formula has the form $$\square\bigwedge_{i=1,\dots,n}(P_ i\Rightarrow F_ i)$$, where $$P_ i$$ is a strict (the current index is not included) past-time temporal formula, and each $$F_ i$$ is a (non-strict) future-time formula. A further restriction on literals is imposed. Any arbitrary temporal formula is rewritten as an equivalent formula in SNF, on which both non- temporal and temporal resolution rules are applied. The non-temporal resolution rule is, essentially, the classical resolution rule and is only applied to $$\square$$-rules (‘always in the future’-rules). $$\lozenge$$-rules (‘sometime in the future’-rules) are processed using the temporal resolution procedure. The temporal resolution rule applies to one $$\lozenge$$-rule, of the form $$P\Rightarrow\lozenge\lnot L$$, and a set of global $$\square$$-rules. A set of rules that, together, imply that the literal $$L$$ is always true, is called a loop in $$L$$. For the implementation efficiency, the author applies a graph-theoretic approach for finding loops: the set of rules belonging to a loop is represented directly as an AND/OR graph, with each rule representing a set of edges, or as a standard state-graph. In either case, the loops in $$L$$ correspond to terminal strongly connected components of the graph structure, which is calculated with a suitable version of R. E. Tarjan’s algorithm. These operations are based on soundness, completeness, and termination of the proposed temporal resolution procedure.
Reviewer: N.Curteanu (Iaşi)

##### MSC:
 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010) 03B35 Mechanization of proofs and logical operations 03B45 Modal logic (including the logic of norms) 68T27 Logic in artificial intelligence
##### Keywords:
resolution procedure; propositional temporal logic