Name
Abstract | ||
|---|---|---|
This paper relates the well-known formalism of Linear Temporal Logic with the
logic of propositional schemata introduced by the authors. We prove that LTL is
equivalent to a particular class of schemata in the sense that polynomial-time
translation algorithms exist from one logic to the other. Not only does this
result shed new light on the expressive power of propositional schemata, but it
also entails the new result that the satisfiability of the considered class of
schemata is PSPACE-complete. We informally compare the resulting proof
procedures for each logic (opposing the direct approaches to the
translation-based ones). The encoding from schemata to LTL makes the Wolper
procedure for LTL very close to the standard tableaux procedure for schemata.
The reverse encoding surprisingly makes the latter procedure very close to the
one-pass Schwendimann algorithm for LTL. |
Year | Venue | Keywords |
|---|---|---|
2011 | Clinical Orthopaedics and Related Research | artificial intelligent,polynomial time,expressive power,linear temporal logic,satisfiability |
Field | DocType | Volume |
Discrete mathematics,Autoepistemic logic,Interval temporal logic,Algorithm,Zeroth-order logic,Linear temporal logic,Theoretical computer science,Many-valued logic,Intermediate logic,Propositional variable,Dynamic logic (modal logic),Mathematics | Journal | abs/1102.2 |
Citations | PageRank | References |
0 | 0.34 | 5 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Vincent Aravantinos | 1 | 86 | 10.29 |
| Ricardo Caferra | 2 | 303 | 29.85 |
| Nicolas Peltier | 3 | 50 | 11.84 |