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.
Citazione: | 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. | |
Tipo: | paper | |
Carattere della pubblicazione: | Scientifica | |
Presenza di un coautore afferente ad Istituzioni straniere: | No | |
Titolo: | Towards a tableau-based procedure for PLTL based on a multi-conclusion rule and logical optimizations | |
Autori: | Ferrari, M; Fiorentini, C; Fiorino, G | |
Autori: | FIORINO, GUIDO GIUSEPPE (Ultimo) | |
Data di pubblicazione: | 2015 | |
Lingua: | English | |
Nome del convegno: | Italian Conference on Computational Logic | |
Serie: | CEUR WORKSHOP PROCEEDINGS | |
Appare nelle tipologie: | 02 - Intervento a convegno |
File in questo prodotto:
File | Descrizione | Tipologia | Licenza | |
---|---|---|---|---|
paper13.pdf | Publisher's version | Administrator Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.