科研之友
微信
新浪微博
Facebook
分享链接
摘要
We consider the Sigma(1)(0)-fragment of second-order logic over the vocabulary %26lt;+, x, 0, 1, %26lt;, S-1,..., S-k %26gt;, interpreted over the reals, where the predicate symbols S-i are interpreted as semi-algebraic sets. We show that, in this context, satisfiability of formulas is decidable for the first-order there exists*-quantifier fragment and undecidable for the there exists*for all- and for all*-fragments. We also show that for these three fragments the same (un)decidability results hold for containment and equivalence of formulas.
- 出版日期2014
