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:propositional_logic_syntax [2009/04/08 18:34]
philippe.suter
sav08:propositional_logic_syntax [2015/04/21 17:30] (current)
Line 3: Line 3:
 Let $V$ be a [[countable set]] of //​propositional variables//,​ denoted by non-terminal //​V//​. ​ The context-free grammar of propositional logic formulas ${\cal F}$ is the following: Let $V$ be a [[countable set]] of //​propositional variables//,​ denoted by non-terminal //​V//​. ​ The context-free grammar of propositional logic formulas ${\cal F}$ is the following:
  
-\[+\begin{equation*}
    F ::= V \mid {\it false} \mid {\it true} \mid (F \land F) \mid (F \lor F) \mid (\lnot F) \mid (F \rightarrow F) \mid (F \leftrightarrow F)    F ::= V \mid {\it false} \mid {\it true} \mid (F \land F) \mid (F \lor F) \mid (\lnot F) \mid (F \rightarrow F) \mid (F \leftrightarrow F)
-\]+\end{equation*}
 We denote the set of all propositional formulas given by the above [[:Notes on Context-Free Grammars|context-free grammar]] by ${\cal F}$.  Each propositional formula is a finite sequence of symbols, given by the above context-free grammar. ​ The set ${\cal F}$ is a countable set: we can order all formulas in this set in a sequence (for example, by writing them down in binary alphabet and sorting the resulting strings alphabetically). We denote the set of all propositional formulas given by the above [[:Notes on Context-Free Grammars|context-free grammar]] by ${\cal F}$.  Each propositional formula is a finite sequence of symbols, given by the above context-free grammar. ​ The set ${\cal F}$ is a countable set: we can order all formulas in this set in a sequence (for example, by writing them down in binary alphabet and sorting the resulting strings alphabetically).
  
Line 11: Line 11:
   * $\land$, $\lor$ associative   * $\land$, $\lor$ associative
   * priorities, from strongest-binding:​ $(\lnot)\ ;\ (\land, \lor)\ ;\ (\rightarrow,​ \leftrightarrow)$   * priorities, from strongest-binding:​ $(\lnot)\ ;\ (\land, \lor)\ ;\ (\rightarrow,​ \leftrightarrow)$
-When in doubt, use parenthesis.+When in doubt, use parentheses.
  
 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 Propositional Logic| In [[Isabelle theorem prover]] we use this ++++ASCII notation for Propositional Logic|
-\[+\begin{equation*}
 \begin{array}{c|c} ​ \begin{array}{c|c} ​
 \mbox{math} & \mbox{Isabelle} \\ \hline \mbox{math} & \mbox{Isabelle} \\ \hline
Line 27: Line 27:
 {\it false} & \verb!False! \\ {\it false} & \verb!False! \\
 \end{array} \end{array}
-\]+\end{equation*}
 Rendering and input in math notation is also possible using ProofGeneral or Eclipse. Rendering and input in math notation is also possible using ProofGeneral or Eclipse.
  
Line 36: Line 36:
  
 $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}{l}+\begin{equation*}\begin{array}{l}
   FV(p) = \{ p \}, \mbox{ for } p \in V \\   FV(p) = \{ p \}, \mbox{ for } p \in V \\
   FV(\lnot F) = FV(F) \\   FV(\lnot F) = FV(F) \\
Line 43: Line 43:
   FV(F_1 \rightarrow F_2) = FV(F_1) \cup FV(F_2) \\   FV(F_1 \rightarrow F_2) = FV(F_1) \cup FV(F_2) \\
   FV(F_1 \leftrightarrow F_2) = FV(F_1) \cup FV(F_2) \\   FV(F_1 \leftrightarrow F_2) = FV(F_1) \cup FV(F_2) \\
-\end{array}\]+\end{array}\end{equation*}
  
 If $FV(F) = \emptyset$, we call $F$ a //ground formula//. If $FV(F) = \emptyset$, we call $F$ a //ground formula//.
 
sav08/propositional_logic_syntax.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice