Name
Abstract | ||
|---|---|---|
We first show that infinite satisfiability can be reduced to finite satisfiability for all prenex formulas of Separation Logic with $k\geq1$ selector fields ($\seplogk{k}$). Second, we show that this entails the decidability of the finite and infinite satisfiability problem for the class of prenex formulas of $\seplogk{1}$, by reduction to the first-order theory of one unary function symbol and unary predicate symbols. We also prove that the complexity is not elementary, by reduction from the first-order theory of one unary function symbol. Finally, we prove that the Bernays-Sch\"onfinkel-Ramsey fragment of prenex $\seplogk{1}$ formulae with quantifier prefix in the language $\exists^*\forall^*$ is \pspace-complete. The definition of a complete (hierarchical) classification of the complexity of prenex $\seplogk{1}$, according to the quantifier alternation depth is left as an open problem. |
Year | DOI | Venue |
|---|---|---|
2018 | 10.29007/74ll | arXiv: Logic in Computer Science |
Field | DocType | Volume |
Discrete mathematics,Separation logic,Open problem,Unary operation,Satisfiability,Boolean satisfiability problem,Decidability,Unary function,Mathematics,Alternation (linguistics) | Journal | abs/1804.03556 |
Citations | PageRank | References |
0 | 0.34 | 0 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Mnacho Echenim | 1 | 95 | 15.75 |
| Radu Iosif | 2 | 483 | 42.44 |
| Nicolas Peltier | 3 | 50 | 11.84 |