Symbolic WS1S
Keyword(s):
Blow Up
◽
We extend weak monadic second-order logic of one successor (WS1S) to symbolic alphabets byallowing character predicates to range over decidable first order theories and not just finite alphabets.We call this extension symbolic WS1S (s-WS1S). We then propose two decision procedures for such alogic: 1) we use symbolic automata to extend the classic reduction from WS1S to finite automata toour symbolic logic setting; 2) we show that every s-WS1S formula can be reduced to a WS1S formulathat preserves satisfiability, at the price of an exponential blow-up.
Keyword(s):
2016 ◽
Vol 17
(4)
◽
pp. 1-18
◽
Keyword(s):
Keyword(s):
1999 ◽
Vol Vol. 3 no. 3
◽
Keyword(s):
2004 ◽
Vol 130
(1-3)
◽
pp. 3-31
◽
Keyword(s):