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:propositional_logic_semantics [2008/03/11 14:51]
vkuncak
sav08:propositional_logic_semantics [2015/04/21 17:30] (current)
Line 8: Line 8:
  
 We next define evaluation function: We next define evaluation function:
-\[+\begin{equation*}
     e : F \to (I \to {\cal B})     e : F \to (I \to {\cal B})
-\]+\end{equation*}
 ++++by recursion on formula syntax tree:| ++++by recursion on formula syntax tree:|
-\[\begin{array}{l}+\begin{equation*}\begin{array}{l}
   e(p)(I) = I(p), \mbox{ for } p \in V \\   e(p)(I) = I(p), \mbox{ for } p \in V \\
-  e({"\lnot "}\> F)(I) = \lnot (e(F)(I)) \\ +  e({'\lnot '}\> F)(I) = \lnot (e(F)(I)) \\ 
-  e(F_1\> {"\land "}\> F_2)(I) = e(F_1)(I) \land e(F_2)(I) \\ +  e(F_1\> {'\land '}\> F_2)(I) = e(F_1)(I) \land e(F_2)(I) \\ 
-  e(F_1\> {"\lor "}\> F_2)(I) = e(F_1)(I) \lor e(F_2)(I) \\ +  e(F_1\> {'\lor '}\> F_2)(I) = e(F_1)(I) \lor e(F_2)(I) \\ 
-  e(F_1\> {"\rightarrow ​"}\> F_2)(I) = (e(F_1)(I) \rightarrow e(F_2)(I)) \\ +  e(F_1\> {'\rightarrow ​'}\> F_2)(I) = (e(F_1)(I) \rightarrow e(F_2)(I)) \\ 
-  e(F_1\> {"\leftrightarrow ​"}\> F_2)(I) = (e(F_1)(I) \leftrightarrow e(F_2)(I))+  e(F_1\> {'\leftrightarrow ​'}\> F_2)(I) = (e(F_1)(I) \leftrightarrow e(F_2)(I))
 \end{array} \end{array}
-\]+\end{equation*}
  
-We wrote symbols like $" ​\land "$ on left in quotes to emphasize that those are syntactic entities, in contrast to symbols like $\land$ on right-hand side that denote propositional operations given by truth tables (stated in [[Propositional Logic Informally]]).+We wrote symbols like $'\land '$ on left in quotes to emphasize that those are syntactic entities, in contrast to symbols like $\land$ on right-hand side that denote propositional operations given by truth tables (stated in [[Propositional Logic Informally]]).
 ++++ ++++
  
Line 29: Line 29:
  
 We denote $e(F)(I) = {\it true}$ by We denote $e(F)(I) = {\it true}$ by
-\[+\begin{equation*}
     I \models F     I \models F
-\]+\end{equation*}
 and denote $e(F)(I) = {\it false}$ by and denote $e(F)(I) = {\it false}$ by
-\[+\begin{equation*}
    I \not\models F    I \not\models F
-\]+\end{equation*}
  
 ===== Validity and Satisfiability ===== ===== Validity and Satisfiability =====
  
 Formula is valid iff $\forall I. I \models F$.  We write this simply Formula is valid iff $\forall I. I \models F$.  We write this simply
-\[+\begin{equation*}
    ​\models F    ​\models F
-\]+\end{equation*}
  
 Formula is satisfiable iff $\exists I. I \models F$ Formula is satisfiable iff $\exists I. I \models F$
 
sav08/propositional_logic_semantics.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice