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_informally [2010/02/22 13:59]
vkuncak
sav08:propositional_logic_informally [2015/04/21 17:30] (current)
Line 1: Line 1:
 ====== Propositional Logic ====== ====== Propositional Logic ======
  
-Propositional logic is the core part of most logical formalisms (such as first-order and higher-order logic). ​ It also describes well digital circuits that are the basis of most modern computing devices. ​ In this course we will +Propositional logic is the core part of most logical formalisms (such as first-order and higher-order logic). ​ It also describes well digital circuits that are the basis of most modern computing devices. ​
-  * review propositional logic informally to make sure everyone is comfortable with it (today) +
-  * define propositional logic formula syntax and semantics formally +
-  * learn how to write programs that build, transform, and prove validity of such formulas (SAT solvers) +
-  * use these techniques to build verification tools+
  
 ===== Importance of Propositional Logic ===== ===== Importance of Propositional Logic =====
Line 31: Line 27:
 === Negation (logical '​not'​) === === Negation (logical '​not'​) ===
  
-\[\begin{array}{c|c}+\begin{equation*}\begin{array}{c|c}
 p & \lnot p \\\hline p & \lnot p \\\hline
 {\sl false} & {\sl true} \\ \hline {\sl false} & {\sl true} \\ \hline
 {\sl true} & {\sl false} {\sl true} & {\sl false}
 \end{array} \end{array}
-\]+\end{equation*}
  
 === Conjunction (logical '​and'​) === === Conjunction (logical '​and'​) ===
  
-\[\begin{array}{c|cc}+\begin{equation*}\begin{array}{c|cc}
 \land & {\sl false} & {\sl true} \\ \hline \land & {\sl false} & {\sl true} \\ \hline
 {\sl false} & {\sl false} & {\sl false} \\ \hline {\sl false} & {\sl false} & {\sl false} \\ \hline
 {\sl true} & {\sl false} & {\sl true} {\sl true} & {\sl false} & {\sl true}
 \end{array} \end{array}
-\]+\end{equation*}
  
 === Disjunction (logical '​or'​) === === Disjunction (logical '​or'​) ===
  
  
-\[\begin{array}{c|cc}+\begin{equation*}\begin{array}{c|cc}
 \lor & {\sl false} & {\sl true} \\ \hline \lor & {\sl false} & {\sl true} \\ \hline
 {\sl false} & {\sl false} & {\sl true} \\ \hline {\sl false} & {\sl false} & {\sl true} \\ \hline
 {\sl true} & {\sl true} & {\sl true} {\sl true} & {\sl true} & {\sl true}
 \end{array} \end{array}
-\]+\end{equation*}
  
 === Implication ('​if'​) === === Implication ('​if'​) ===
  
-\[\begin{array}{c|cc}+\begin{equation*}\begin{array}{c|cc}
 \rightarrow & {\sl false} & {\sl true} \\ \hline \rightarrow & {\sl false} & {\sl true} \\ \hline
 {\sl false} & {\sl true} & {\sl true} \\ \hline {\sl false} & {\sl true} & {\sl true} \\ \hline
 {\sl true} & {\sl false} & {\sl true} {\sl true} & {\sl false} & {\sl true}
 \end{array} \end{array}
-\]+\end{equation*}
  
 Check validity of these implications:​ Check validity of these implications:​
Line 73: Line 69:
 === Logical Eqivalence ('if and only if') === === Logical Eqivalence ('if and only if') ===
  
-\[\begin{array}{c|cc}+\begin{equation*}\begin{array}{c|cc}
 \leftrightarrow & {\sl false} & {\sl true} \\ \hline \leftrightarrow & {\sl false} & {\sl true} \\ \hline
 {\sl false} & {\sl true} & {\sl false} \\ \hline {\sl false} & {\sl true} & {\sl false} \\ \hline
 {\sl true} & {\sl false} & {\sl true} {\sl true} & {\sl false} & {\sl true}
 \end{array} \end{array}
-\]+\end{equation*}
  
 ===== Evaluating Propositional Formulas ===== ===== Evaluating Propositional Formulas =====
Line 85: Line 81:
  
 Let us evaluate formula Let us evaluate formula
-\[+\begin{equation*}
     ((p \rightarrow q) \land\ ((\lnot p) \rightarrow r)) \leftrightarrow ((p \land q)\ \lor\ ((\lnot p) \land r))     ((p \rightarrow q) \land\ ((\lnot p) \rightarrow r)) \leftrightarrow ((p \land q)\ \lor\ ((\lnot p) \land r))
-\]+\end{equation*}
 for all values of its parameters. ​ Let us draw formula as a tree.  We introduce a column for each tree node.  We obtain the value of a tree node by looking at the value of its children and applying the truth table for the operation in the node.  The root gives the truth value of the formula. for all values of its parameters. ​ Let us draw formula as a tree.  We introduce a column for each tree node.  We obtain the value of a tree node by looking at the value of its children and applying the truth table for the operation in the node.  The root gives the truth value of the formula.
  
Line 113: Line 109:
 Here is a small list of tautologies. Here is a small list of tautologies.
  
-\[\begin{array}{l}+\begin{equation*}\begin{array}{l}
   (p \rightarrow q) \leftrightarrow ((\lnot p) \lor q) \\   (p \rightarrow q) \leftrightarrow ((\lnot p) \lor q) \\
   (p \leftrightarrow q) \leftrightarrow ((p \rightarrow q) \land (q \rightarrow p)) \\   (p \leftrightarrow q) \leftrightarrow ((p \rightarrow q) \land (q \rightarrow p)) \\
Line 130: Line 126:
   ((p \lor q) \rightarrow r) \leftrightarrow ((p \rightarrow r) \land (q \rightarrow r)) \\   ((p \lor q) \rightarrow r) \leftrightarrow ((p \rightarrow r) \land (q \rightarrow r)) \\
   ((p \rightarrow {\sl false}) \leftrightarrow (\lnot p)   ((p \rightarrow {\sl false}) \leftrightarrow (\lnot p)
-\end{array}\]+\end{array}\end{equation*}
  
 Suggest another tautology. Suggest another tautology.
 
sav08/propositional_logic_informally.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice