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.

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)