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: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