×

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
PDF BibTeX XML Cite