LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
sav08:simple_qe_for_dense_linear_orders [2009/04/21 19:34]
vkuncak
sav08:simple_qe_for_dense_linear_orders [2015/04/21 17:30] (current)
Line 11: Line 11:
  
 Formulas $T$ are the formulas that are closed formulas that are true in the structure $(\mathbb{Q},<​)$ or rational numbers. Formulas $T$ are the formulas that are closed formulas that are true in the structure $(\mathbb{Q},<​)$ or rational numbers.
 +
 +**Example:​** The '​successor'​ formula:
 +\begin{equation*}
 +   ​\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?
  
 ===== Normal form of Formulas ===== ===== Normal form of Formulas =====
Line 33: Line 39:
 Quantifier elimination from more general formulas: Quantifier elimination from more general formulas:
  
-  ​* [[http://​www4.informatik.tu-muenchen.de/​~nipkow/​pubs/​lqe.pdf|Linear Quantifier Elimination]]+**Example:​** Use quantifier elimination to compute the truth value in dense linear orders for the example '​successor'​ formula above. 
 + 
 + 
 +===== References ===== 
 + 
 +  ​* [[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]]