Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

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]]
  
 
sav08/simple_qe_for_dense_linear_orders.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice