Home // COMPUTATION TOOLS 2015, The Sixth International Conference on Computational Logics, Algebras, Programming, Tools, and Benchmarking // View article

A New Refutation Calculus With Logical Optimizations for PLTL

Authors:
Mauro Ferrari
Camillo Fiorentini
Guido Fiorino

Keywords: Propositional Linear Temporal Logic; Tableaux; Satisfiability checking.

Abstract:
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.

Pages: 31 to 33

Copyright: Copyright (c) IARIA, 2015

Publication date: March 22, 2015

Published in: conference

ISSN: 2308-4170

ISBN: 978-1-61208-394-0

Location: Nice, France

Dates: from March 22, 2015 to March 27, 2015