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_logic_syntax [2008/03/19 10:24]
vkuncak
sav08:first-order_logic_syntax [2015/04/21 17:30] (current)
Line 7: Line 7:
 The set $V$ denotes countably infinite set of first-order variables, which is independent of the language. The set $V$ denotes countably infinite set of first-order variables, which is independent of the language.
  
-\[+\begin{equation*}
 \begin{array}{rcl} \begin{array}{rcl}
     F &::​=&​ A \mid \lnot F \mid (F \land F) \mid (F \lor F) \mid (F \rightarrow F) \mid (F \leftrightarrow F) \\     F &::​=&​ A \mid \lnot F \mid (F \land F) \mid (F \lor F) \mid (F \rightarrow F) \mid (F \leftrightarrow F) \\
Line 14: Line 14:
     T & ::= & V \mid f(T,​\ldots,​T)  ​     T & ::= & V \mid f(T,​\ldots,​T)  ​
 \end{array} \end{array}
-\]+\end{equation*}
  
 Terminology summary: Terminology summary:
Line 31: Line 31:
  
 Example: Consider language ${\cal L} = \{ P, Q, R, f \}$ with $ar(P) = 1$, $ar(Q) = 1$, $ar(R) = 2$, $ar(f) = 2$. Then Example: Consider language ${\cal L} = \{ P, Q, R, f \}$ with $ar(P) = 1$, $ar(Q) = 1$, $ar(R) = 2$, $ar(f) = 2$. Then
-\[+\begin{equation*}
     \lnot \forall x.\, \forall y. R(x,y) \land Q(x) \rightarrow Q(f(y,x)) \lor P(x)     \lnot \forall x.\, \forall y. R(x,y) \land Q(x) \rightarrow Q(f(y,x)) \lor P(x)
-\]+\end{equation*}
 denotes denotes
-\[+\begin{equation*}
     \lnot (\forall x.\ (\forall y. ((R(x,y) \land Q(x)) \rightarrow (Q(f(y,x)) \lor P(x)))))     \lnot (\forall x.\ (\forall y. ((R(x,y) \land Q(x)) \rightarrow (Q(f(y,x)) \lor P(x)))))
-\]+\end{equation*}
  
 Often we use infix notation for relation and function symbols. ​ In the example above, if we write $R$ and $f$ in infix notation, the formula becomes Often we use infix notation for relation and function symbols. ​ In the example above, if we write $R$ and $f$ in infix notation, the formula becomes
-\[+\begin{equation*}
     \lnot \forall x.\, \forall y. x \mathop{R} y \land Q(x) \rightarrow Q(y \mathop{f} x) \lor P(x)     \lnot \forall x.\, \forall y. x \mathop{R} y \land Q(x) \rightarrow Q(y \mathop{f} x) \lor P(x)
-\]+\end{equation*}
  
 Notation: when we write $F_1 \equiv F_2$ this means that $F_1$ and $F_2$ are identical formulas (with identical syntax trees). ​ For example, $p \land q \equiv p \land q$, but it is not the case that $p \land q \equiv q \land p$. Notation: when we write $F_1 \equiv F_2$ this means that $F_1$ and $F_2$ are identical formulas (with identical syntax trees). ​ For example, $p \land q \equiv p \land q$, but it is not the case that $p \land q \equiv q \land p$.
  
 In [[Isabelle theorem prover]] we use this ++++ASCII notation for First-Order Logic| In [[Isabelle theorem prover]] we use this ++++ASCII notation for First-Order Logic|
-\[+\begin{equation*}
 \begin{array}{c|c} ​ \begin{array}{c|c} ​
 \mbox{math} & \mbox{Isabelle} \\ \hline \mbox{math} & \mbox{Isabelle} \\ \hline
Line 60: Line 60:
 \exists ​ & \verb!EX! \exists ​ & \verb!EX!
 \end{array} \end{array}
-\]+\end{equation*}
 Rendering and input in math notation is also possible using [[http://​proofgeneral.inf.ed.ac.uk/​|ProofGeneral]]. Note: the equality symbol (even if used on '​bool'​ types) binds more strongly than propositional operators, unlike the usual equivalence. Rendering and input in math notation is also possible using [[http://​proofgeneral.inf.ed.ac.uk/​|ProofGeneral]]. Note: the equality symbol (even if used on '​bool'​ types) binds more strongly than propositional operators, unlike the usual equivalence.
  
Line 69: Line 69:
  
 $FV$ denotes the set of free variables in the given propositional formula and can be defined recursively as follows: $FV$ denotes the set of free variables in the given propositional formula and can be defined recursively as follows:
-\[\begin{array}{rcl}+\begin{equation*}\begin{array}{rcl}
   FV(x) &=& \{ x \}, \mbox{ for } x \in V \\   FV(x) &=& \{ x \}, \mbox{ for } x \in V \\
-  FV(f(t_1,​\ldots,​t_n) &=& F(t_1) \cup \ldots \cup F(t_n) \\ +  FV(f(t_1,​\ldots,​t_n)) &=& F(t_1) \cup \ldots \cup F(t_n) \\ 
-  FV(R(t_1,​\ldots,​t_n) &=& F(t_1) \cup \ldots \cup F(t_n) \\+  FV(R(t_1,​\ldots,​t_n)) &=& F(t_1) \cup \ldots \cup F(t_n) \\
   FV(t_1 = t_2) &=& F(t_1) \cup F(t_2) \\   FV(t_1 = t_2) &=& F(t_1) \cup F(t_2) \\
   FV(\lnot F) &=& FV(F) \\   FV(\lnot F) &=& FV(F) \\
Line 81: Line 81:
   FV(\forall x.F) &=& FV(F) \setminus \{x\} \\   FV(\forall x.F) &=& FV(F) \setminus \{x\} \\
   FV(\exists x.F) &=& FV(F) \setminus \{x\}    FV(\exists x.F) &=& FV(F) \setminus \{x\} 
-\end{array}\]+\end{array}\end{equation*}
  
 If $FV(F) = \emptyset$, we call $F$ a //closed first-order logic formula//, or //​sentence//​. If $FV(F) = \emptyset$, we call $F$ a //closed first-order logic formula//, or //​sentence//​.
  
 
sav08/first-order_logic_syntax.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice