Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
|
complexity [2007/10/05 01:00] philippe.suter |
complexity [2007/10/05 01:03] philippe.suter |
||
|---|---|---|---|
| Line 40: | Line 40: | ||
| * $\forall x . S_1(x) \vee \ldots \vee S_n(x) \Leftrightarrow T(x)$ | * $\forall x . S_1(x) \vee \ldots \vee S_n(x) \Leftrightarrow T(x)$ | ||
| * and $\forall x . \neg (E(x) \wedge F(x))$ respectively. | * and $\forall x . \neg (E(x) \wedge F(x))$ respectively. | ||
| + | |||
| + | |||
| ==== Verifying disjunction ==== | ==== Verifying disjunction ==== | ||
| Line 56: | Line 58: | ||
| Note that checking the satifiability should be doable in polynomial time, as all needs to be done is find one pair of sets among a finite list which are disjoint (and this information can only come from the assumptions/axioms, which are themselves in a finite number. (FIXME : I know this doesn't sound convincing.. let's do better). | Note that checking the satifiability should be doable in polynomial time, as all needs to be done is find one pair of sets among a finite list which are disjoint (and this information can only come from the assumptions/axioms, which are themselves in a finite number. (FIXME : I know this doesn't sound convincing.. let's do better). | ||
| + | |||
| + | We can also rely on the fact that we introduced only one quantifier and that the size of the generated formula is linear in terms of the size of the original one. This formula is hence in $[\exists^{*} \forall^{1}]_{=}$ and checking its validity can hence be done in NP time. | ||
| ==== Verifying completeness/reachability ==== | ==== Verifying completeness/reachability ==== | ||