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.
Ferrari, M., Fiorentini, C., Fiorino, G. (2015). Towards a tableau-based procedure for PLTL based on a multi-conclusion rule and logical optimizations. In Proceedings of the 30th Italian Conference on Computational Logic, Genova, Italy, July 1-3, 2015 (pp.117-121). CEUR-WS.
Towards a tableau-based procedure for PLTL based on a multi-conclusion rule and logical optimizations
FIORINO, GUIDO GIUSEPPEUltimo
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 in questo prodotto:
| File | Dimensione | Formato | |
|---|---|---|---|
|
paper13.pdf
Solo gestori archivio
Tipologia di allegato:
Publisher’s Version (Version of Record, VoR)
Dimensione
241.71 kB
Formato
Adobe PDF
|
241.71 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
