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:

    e : F \to (I \to {\cal B})

by recursion on formula syntax tree:

This definition follows one in the formula evaluator in homework01.

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

    I \models F

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

   I \not\models F

Validity and Satisfiability

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

   \models F

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