Lab for Automated Reasoning and Analysis LARA

Propositional Logic Semantics

Recall homework01.

Let ${\cal B} = \{{\it true}, {\it false}\}$.

Interpretation for propositional logic is a function $I : V \to {\cal B}$.

We next define evaluation function:

\begin{equation*}
    e : F \to (I \to {\cal B})
\end{equation*}

by recursion on formula syntax tree:

This definition follows one in the formula evaluator in homework01.

We denote $e(F)(I) = {\it true}$ by

\begin{equation*}
    I \models F
\end{equation*}

and denote $e(F)(I) = {\it false}$ by

\begin{equation*}
   I \not\models F
\end{equation*}

Validity and Satisfiability

Formula is valid iff $\forall I. I \models F$. We write this simply

\begin{equation*}
   \models F
\end{equation*}

Formula is satisfiable iff $\exists I. I \models F$

Formula is contradictory iff $\forall I. I \not\models F$

Satisfiability of Sets of Formulas

 
sav08/propositional_logic_semantics.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice