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 GIUSEPPE
Ultimo
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.
paper
Tableaux, Propositional Linear Temporal Logic, Automated Deduction
English
Italian Conference on Computational Logic
2015
Ancona, D; Maratea, M; Mascardi, V
Proceedings of the 30th Italian Conference on Computational Logic, Genova, Italy, July 1-3, 2015
2015
1459
117
121
http://ceur-ws.org/Vol-1459/paper13.pdf
reserved
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.
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.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/10281/157775
Citazioni
  • Scopus 0
  • ???jsp.display-item.citation.isi??? ND
Social impact