Towards a tableau-based procedure for PLTL based on a multi-conclusion rule and logical optimizations
Mauro Ferrari, Camillo Fiorentini, Guido Fiorino · BOA (University of Milano-Bicocca) · 2015
We present an ongoing work on a proof-search procedure for Propositional Linear Temporal Logic (PLTL) based on a one-pass tableau calculus with a multiple-conclusion rule. The procedure exploits logical optimization rules to reduce the proof-search space. We also discuss the performances of a Prolog prototype of our procedure.