We consider the $\Sigma_0^1$-fragment of second-order logic over the vocabulary $\langle+, \times, 0, 1, <, S_1, ..., S_k \rangle$, interpreted over the reals, where the predicate symbols $S_i$ are interpreted as semialgebraic sets. We show that, in this context, satisability of formulas is decidable for the first-order $\exists$*-quantifier fragment and undecidable for the $\exists$*$\forall$- and $\forall$*-fragments. We also show that for these three fragments the same (un)decidability results hold for containment and equivalence of formulas.
Ta witryna wykorzystuje pliki cookies do przechowywania informacji na Twoim komputerze. Pliki cookies stosujemy w celu świadczenia usług na najwyższym poziomie, w tym w sposób dostosowany do indywidualnych potrzeb. Korzystanie z witryny bez zmiany ustawień dotyczących cookies oznacza, że będą one zamieszczane w Twoim komputerze. W każdym momencie możesz dokonać zmiany ustawień dotyczących cookies
Informacja
SZANOWNI CZYTELNICY!
UPRZEJMIE INFORMUJEMY, ŻE BIBLIOTEKA FUNKCJONUJE W NASTĘPUJĄCYCH GODZINACH:
Wypożyczalnia i Czytelnia Główna: poniedziałek – piątek od 9.00 do 19.00