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:deciding_quantifier-free_fol [2008/04/23 06:49]
vkuncak
sav08:deciding_quantifier-free_fol [2015/04/21 17:30] (current)
Line 8: Line 8:
  
 Example: is the following formula satisfiable:​ Example: is the following formula satisfiable:​
-\[+\begin{equation*}
   a=f(a) \land a \neq b   a=f(a) \land a \neq b
-\]+\end{equation*}
 is the following is the following
-\[ +\begin{equation*} 
-   ​(f(a)=b \lor (f(f(f(a))) = a \land f(a) \neq f(b))) \land f(f(f(f(a)) \neq b \land b=f(b) +   ​(f(a)=b \lor (f(f(f(a))) = a \land f(a) f(b))) \land f(f(f(f(a)) \neq b \land b=f(b) 
-\]+\end{equation*}
  
 
sav08/deciding_quantifier-free_fol.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice