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.
Towards a tableau-based procedure for PLTL based on a multi-conclusion rule and logical optimizations / M. Ferrari, C. Fiorentini, G. Fiorino (CEUR WORKSHOP PROCEEDINGS). - In: Proceedings of the 30th Italian Conference on Computational Logic (CILC 2015), Genova, Italy, July 1-3, 2015. / [a cura di] D. Ancona, M. Maratea, V. Mascardi. - [s.l] : D. Ancona, M. Maratea, V. Mascardi, 2015 Sep 29. - pp. 117-121 (( Intervento presentato al 30. convegno CILC (Italian Conference on Computational Logic) tenutosi a Genova nel 2015.
Towards a tableau-based procedure for PLTL based on a multi-conclusion rule and logical optimizations
C. Fiorentini;
2015
Abstract
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.
| File | Dimensione | Formato | |
|---|---|---|---|
|
paper13.pdf
accesso aperto
Tipologia:
Publisher's version/PDF
Dimensione
241.71 kB
Formato
Adobe PDF
|
241.71 kB | Adobe PDF | Visualizza/Apri |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
