A New Refutation Calculus With Logical Optimizations for PLTL

摘要

Propositional Linear Temporal Logic (PLTL) is a tool for reasoning about systems whose states change in time. We present an ongoing work on a new proof-search procedure for Propositional Linear Temporal Logic and its implementation. The proof-search procedure is based on a one-pass tableau calculus with a multiple-conclusion rule treating temporal-operators and on some logical optimization rules. These rules have been devised by applying techniques developed by the authors for logics with Kripke semantics and here applied to the Kripke-based semantics for Propositional Linear Temporal Logic.