Since 2014
First-Order Logic with Two Variables and Unary Temporal Logic
BRICS Report Series
View Archive Info| Field | Value | |
| Title |
First-Order Logic with Two Variables and Unary Temporal Logic
|
|
| Creator |
Etessami, Kousha
Vardi, Moshe Y. Wilke, Thomas |
|
| Description |
We investigate the power of first-order logic with only two variables overomega-words and finite words, a logic denoted by FO2. We prove that FO2 canexpress precisely the same properties as linear temporal logic with only the unary temporal operators: “next”, “previously”, “sometime in the future”, and “sometime in the past”, a logic we denote by unary-TL. Moreover, our translation from FO2 to unary-TL converts every FO2 formula to an equivalent unary-TL formula that is at most exponentially larger, and whose operator depth is at most twice the quantifier depth of the first-order formula. We show that this translation is optimal.While satisfiability for full linear temporal logic, as well as forunary-TL, is known to be PSPACE-complete, we prove that satisfiabilityfor FO2 is NEXP-complete, in sharp contrast to the fact that satisfiabilityfor FO3 has non-elementary computational complexity. Our NEXP timeupper bound for FO2 satisfiability has the advantage of being in terms ofthe quantifier depth of the input formula. It is obtained using a small model property for FO2 of independent interest, namely: a satisfiable FO2 formula has a model whose “size” is at most exponential in the quantifier depth of the formula. Using our translation from FO2 to unary-TL we derive this small model property from a corresponding small model property for unary-TL. Our proof of the small model property for unary-TL is based on an analysis of unary-TL types.
|
|
| Publisher |
Aarhus University
|
|
| Date |
1997-01-05
|
|
| Type |
info:eu-repo/semantics/article
info:eu-repo/semantics/publishedVersion |
|
| Format |
application/pdf
|
|
| Identifier |
https://tidsskrift.dk/brics/article/view/18784
10.7146/brics.v4i5.18784 |
|
| Source |
BRICS Report Series; No 5 (1997): RS-05 First-Order Logic with Two Variables and Unary Temporal Logic
BRICS Report Series; Nr. 5 (1997): RS-05 First-Order Logic with Two Variables and Unary Temporal Logic 1601-5355 0909-0878 |
|
| Language |
eng
|
|
| Relation |
https://tidsskrift.dk/brics/article/view/18784/16431
|
|