非表示:
キーワード:
-
要旨:
This paper introduces a new decision procedure for PLTL based on labelled
superposition.
Its main idea is to treat temporal formulas as infinite sets of purely
propositional clauses over an extended signature. These infinite sets are then
represented by finite sets of labelled propositional clauses. The new
representation enables the replacement of the complex temporal resolution
rule, suggested by existing resolution calculi for PLTL, by a fine grained
repetition check of finitely saturated labelled clause sets followed by a
simple inference. The completeness argument is based on the standard model
building idea from superposition. It inherently justifies ordering
restrictions, redundancy elimination and effective partial model building. The
latter can be directly used to effectively generate counterexamples of
non-valid PLTL conjectures out of saturated labelled clause sets in a
straightforward way.
