• 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) Both sides previous revision Previous revision 2009/04/22 12:08 vkuncak 2009/04/22 00:02 vkuncak 2009/04/21 23:59 vkuncak 2009/04/21 19:34 vkuncak 2009/04/21 19:32 vkuncak 2009/04/21 19:31 vkuncak 2009/04/21 19:28 vkuncak 2008/04/22 16:33 piskac 2008/04/10 13:09 vkuncak 2008/04/10 13:08 vkuncak 2008/04/10 12:58 vkuncak 2008/04/09 21:39 vkuncak 2008/04/09 21:37 vkuncak created Next revision Previous revision 2009/04/22 12:08 vkuncak 2009/04/22 00:02 vkuncak 2009/04/21 23:59 vkuncak 2009/04/21 19:34 vkuncak 2009/04/21 19:32 vkuncak 2009/04/21 19:31 vkuncak 2009/04/21 19:28 vkuncak 2008/04/22 16:33 piskac 2008/04/10 13:09 vkuncak 2008/04/10 13:08 vkuncak 2008/04/10 12:58 vkuncak 2008/04/09 21:39 vkuncak 2008/04/09 21:37 vkuncak created 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