Differences

This shows you the differences between two versions of the page.

--- sav08:propositional_logic_informally [2010/02/22 13:59]
vkuncak
+++ sav08:propositional_logic_informally [2015/04/21 17:30]
@@ Line 1: / Line 1: @@
-====== 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
-  * 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 =====
-  * Many search problems can be encoded using propositional formulas
-  * Checking equivalence of logical combinatorial circuits in hardware directly reduces to SAT
-  * Can encode integer arithmetic with fixed bitwidth (e.g. operations on 16-bit integers)
-  * An important class of logics can be obtained by giving meaning to propositional variables
-===== Propositional Formulas =====
-Propositional logic studies propositional formulas.
-//Propositional formulas// are expressions built from
-  * constants //true// and //false//
-  * propositional variables, such as $p$, $q$, $p_1$, $q_1$, ...
-  * logical operators ($\land, \lor, \lnot, \rightarrow, \leftrightarrow$) that combine propositional formulas into larger propositional formulas (we define their meaning below)
-**Analogy with mathematical expressions:** Just like a mathematical expression such as $2 \cdot x + 3 \cdot y$ specifies a binary function from values of $x$ and $y$ to the value $2x+3y$, a propositional formula such as $p \land (\lnot q)$ specifies a function from the values of $p$ and $q$ to the value $p \land (\lnot q)$.
-===== Definitions of Logical Operations (Logical Connectives) =====
-We specify a binary  logical operation by a truth table: for each combination of arguments we indicate the result of the operation.  For binary operation, the rows indicate the first argument, the columns indicate the second argument.
-=== Negation (logical 'not') ===
-\[\begin{array}{c|c}
-p & \lnot p \\\hline
-{\sl false} & {\sl true} \\ \hline
-{\sl true} & {\sl false}
-\end{array}
-\]
-=== Conjunction (logical 'and') ===
-\[\begin{array}{c|cc}
-\land & {\sl false} & {\sl true} \\ \hline
-{\sl false} & {\sl false} & {\sl false} \\ \hline
-{\sl true} & {\sl false} & {\sl true}
-\end{array}
-\]
-=== Disjunction (logical 'or') ===
-\[\begin{array}{c|cc}
-\lor & {\sl false} & {\sl true} \\ \hline
-{\sl false} & {\sl false} & {\sl true} \\ \hline
-{\sl true} & {\sl true} & {\sl true}
-\end{array}
-\]
-=== Implication ('if') ===
-\[\begin{array}{c|cc}
-\rightarrow & {\sl false} & {\sl true} \\ \hline
-{\sl false} & {\sl true} & {\sl true} \\ \hline
-{\sl true} & {\sl false} & {\sl true}
-\end{array}
-\]
-Check validity of these implications:
-  * $(1=2)\ \rightarrow\ (7 \mbox{ is an even number})$
-  * $(1=1)\ \rightarrow\ (7 \mbox{ is an even number})$
-  * $(1=2)\ \rightarrow\ (\sqrt{2} \mbox{ is a rational number})$
-=== Logical Eqivalence ('if and only if') ===
-\[\begin{array}{c|cc}
-\leftrightarrow & {\sl false} & {\sl true} \\ \hline
-{\sl false} & {\sl true} & {\sl false} \\ \hline
-{\sl true} & {\sl false} & {\sl true}
-\end{array}
-\]
-===== Evaluating Propositional Formulas =====
-If we know values of variables in the formula, we can compute its value.
-Let us evaluate formula
-\[
-    ((p \rightarrow q) \land\ ((\lnot p) \rightarrow r)) \leftrightarrow ((p \land q)\ \lor\ ((\lnot p) \land r))
-\]
-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.
-===== Validity, Satisfiability of Logical Formulas =====
-Formula is //valid// if it evaluates to //true// for //all// values of its variables (all columns for formula say //true//).
-Formula is //satisfiable// if it evaluates to //true// for //some// values of its variables (//true// appears in at least one column).
-Formula is //unsatisfiable// if it evaluates to //false// for //all// values of its variables (all columns for formula say //false//).
-**Observations**
-  * $F$ is unsatisfiable if and only if $F$ is not satisfiable
-  * $F$ is valid if and only if $\lnot F$ is unsatisfiable
-**SAT** problem: given a propositional formula $F$, check whether $F$ is satisfiable.
-**SAT** is a well-known NP-complete problem.
-===== Propositional Tautologies =====
-Valid propositional formula is called //propositional tautology//, or //tautology// for short.  Tautologies are basic principles of logical reasoning.  They are true regardless of how complex the intended meaning of propositions is, as long as we are sure that each proposition evaluates to //true// or //false//.
-Here is a small list of tautologies.
-\[\begin{array}{l}
-  (p \rightarrow q) \leftrightarrow ((\lnot p) \lor q) \\
-  (p \leftrightarrow q) \leftrightarrow ((p \rightarrow q) \land (q \rightarrow p)) \\
-  (p \land q) \leftrightarrow (q \land p) \\
-  (p \land (q \land r)) \leftrightarrow ((p \land q) \land r)) \\
-  (p \lor q) \leftrightarrow (q \lor p) \\
-  (p \lor (q \lor r)) \leftrightarrow ((p \lor q) \lor r)) \\
-  (p \land (q \lor r)) \leftrightarrow ((p \land q) \lor (p \land r)) \\
-  (p \lor (q \land r)) \leftrightarrow ((p \lor q) \land (p \lor r)) \\
-  \lnot (\lnot p) \leftrightarrow p \\
-  p \lor (\lnot p) \\
-  \lnot (p \land q) \leftrightarrow (\lnot p) \lor (\lnot q) \\
-  \lnot (p \lor q) \leftrightarrow (\lnot p) \land (\lnot q) \\
-  (p \rightarrow (q \rightarrow r)) \leftrightarrow ((p \land q) \rightarrow r) \\
-  (p \rightarrow (q \land r)) \leftrightarrow ((p \rightarrow q) \land (p \rightarrow r)) \\
-  ((p \lor q) \rightarrow r) \leftrightarrow ((p \rightarrow r) \land (q \rightarrow r)) \\
-  ((p \rightarrow {\sl false}) \leftrightarrow (\lnot p)
-\end{array}\]
-Suggest another tautology.
-===== More information =====
-  * [[Calculus of Computation Textbook]], Chapter 1 (for now especially Sections 1.1, 1.2, 1.3)
-  * [[:Gallier Logic Book]], Sections 3.1, 3.2, 3.3