Name
Title | ||
|---|---|---|
Towards a tableau-based procedure for PLTL based on a multi-conclusion rule and logical optimizations. |
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. |
Year | Venue | Field |
|---|---|---|
2015 | CILC | Programming language,Computer science,Automated theorem proving,Linear temporal logic,Prolog,Rule of inference,Propositional variable,Method of analytic tableaux |
DocType | Citations | PageRank |
Conference | 0 | 0.34 |
References | Authors | |
9 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Mauro Ferrari | 1 | 93 | 16.05 |
| Camillo Fiorentini | 2 | 121 | 21.00 |
| Guido Fiorino | 3 | 97 | 12.71 |