Lab for Automated Reasoning and Analysis 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:first-order_theories [2008/04/15 13:45]
vkuncak
sav08:first-order_theories [2015/04/21 17:30] (current)
Line 3: Line 3:
 (Building on [[First-Order Logic Semantics]].) (Building on [[First-Order Logic Semantics]].)
  
-**Definition:​** A //​first-order theory// is a set $T$ of [[First-Order Logic Syntax|first-order logic formulas]].+**Definition:​** A //​first-order theory// is a set $T$ of [[First-Order Logic Syntax|first-order logic sentences]].
  
 **Definition:​** A theory $T$ is //​consistent//​ if it is satisfiable. **Definition:​** A theory $T$ is //​consistent//​ if it is satisfiable.
Line 22: Line 22:
  
 Consider the language ${\cal L} = \{ \le \}$ where $\le$ is a binary relation. ​ Consider the following three sentences: Consider the language ${\cal L} = \{ \le \}$ where $\le$ is a binary relation. ​ Consider the following three sentences:
-\[\begin{array}{rcl}+\begin{equation*}\begin{array}{rcl}
   Ref & \equiv & \forall x. x \le x \\   Ref & \equiv & \forall x. x \le x \\
   Sym & \equiv & \forall x.\ x \le y \land y \le x \rightarrow x=y \\   Sym & \equiv & \forall x.\ x \le y \land y \le x \rightarrow x=y \\
   Tra & \equiv & \forall x. \forall y.\ \forall z. x \le y \land y \le z \rightarrow x \le z   Tra & \equiv & \forall x. \forall y.\ \forall z. x \le y \land y \le z \rightarrow x \le z
 \end{array} \end{array}
-\]+\end{equation*}
 Let $T = Conseq(\{Ref,​Sym,​Tra\})$. ​ Let us answer the following: Let $T = Conseq(\{Ref,​Sym,​Tra\})$. ​ Let us answer the following:
   * Is $T$ ++consistent?​|Yes,​ take, for example, ordering on integers.++   * Is $T$ ++consistent?​|Yes,​ take, for example, ordering on integers.++
   * Is $T$ ++complete?​|No,​ take, for example, $\exists x. \forall y. x \le y$. It is true with the ordering on $\mathbb{N}$,​ but false with the ordering on $\mathbb{Z}$.++   * Is $T$ ++complete?​|No,​ take, for example, $\exists x. \forall y. x \le y$. It is true with the ordering on $\mathbb{N}$,​ but false with the ordering on $\mathbb{Z}$.++
 
sav08/first-order_theories.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice