• English only

# Differences

This shows you the differences between two versions of the page.

sav08:simple_qe_for_dense_linear_orders [2009/04/22 00:02]
vkuncak
sav08:simple_qe_for_dense_linear_orders [2015/04/21 17:30] (current)
Line 13: Line 13:

**Example:​** The '​successor'​ formula: **Example:​** The '​successor'​ formula:
-$+\begin{equation*} ​\forall x. \exists y.\ x < y \ \land\ (\forall z. (x < z \rightarrow z=y \lor y < z) ​\forall x. \exists y.\ x < y \ \land\ (\forall z. (x < z \rightarrow z=y \lor y < z) -$+\end{equation*}
Is this formula true in dense linear orders? Is there a non-dense linear order where its truth value is different? Is this formula true in dense linear orders? Is there a non-dense linear order where its truth value is different?

Line 40: Line 40:

**Example:​** Use quantifier elimination to compute the truth value in dense linear orders for the example '​successor'​ formula above. **Example:​** Use quantifier elimination to compute the truth value in dense linear orders for the example '​successor'​ formula above.
+

===== References ===== ===== References =====

-  * [[http://​www4.informatik.tu-muenchen.de/​~nipkow/​pubs/​lqe.pdf|Linear Quantifier Elimination]]+  * [[http://​www4.informatik.tu-muenchen.de/​~nipkow/​pubs/​lqe.pdf|Linear Quantifier Elimination]] ​(Tobias Nipkow, IJCAR 2008)
* [[http://​citeseer.ist.psu.edu/​loos93applying.html|Applying Linear Quantifier Elimination]]   * [[http://​citeseer.ist.psu.edu/​loos93applying.html|Applying Linear Quantifier Elimination]]
* [[http://​citeseer.ist.psu.edu/​71579.html|Parallel Fourier-Motzkin Elimination]]   * [[http://​citeseer.ist.psu.edu/​71579.html|Parallel Fourier-Motzkin Elimination]]