TY - JOUR
TI - Some Fragments of Second-Order Logic Over the Reals for Which Satisfiability and Equivalence Are (Un)Decidable
AU - Grimson, Rafael
AU - Kuijpers, Bart
TI - Some Fragments of Second-Order Logic Over the Reals for Which Satisfiability and Equivalence Are (Un)Decidable
AB - 
 We consider the Σ1-fragment of second-order logic over the vocabulary (+, ×, 0, 1, <, S1, ..., Sk), interpreted over the reals, where the predicate symbols Si are interpreted as semi- algebraic sets. We show that, in this context, satisfiability of formulas is decidable for the first-order ∃∗-quantifier fragment and undecidable for the ∃∗∀- and ∀∗-fragments. We also show that for these three fragments the same (un)decidability results hold for containment and equivalence of formulas.

VL - 2014
IS - Number 49
PY - 2014
SN - 0137-2904
C1 - 2084-2589
SP - 23
EP - 34
DO - 10.4467/20842589RM.14.002.2272
UR - https://ejournals.eu/en/journal/reports-on-mathematical-logic/article/some-fragments-of-second-order-logic-over-the-reals-for-which-satisfiability-and-equivalence-are-un-decidable