Lab for Automated Reasoning and Analysis LARA

Semantic Argument Method

Suppose we want to prove the validity of a propositional logic formula $F$. Several methods to do this exists, one of which is called the semantic argument method.

We start the proof by assuming that a falsifying interpretation exists:

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

and try to show that this leads to a contradiction by applying semantic definitions of the logical connectives.

Thus, we obtain a set of proof rules:

\begin{equation*}
  \frac{I \models \neg F}{I \not\models F}  \text{    and    } \frac{I \not\models \neg F}{I \models F}
\end{equation*}

\begin{equation*}
    \frac{I \models F \wedge G}{\parbox{2cm}{$I \models F$ \\ $I \models G$}}  \text{ and }
    \frac{I \not\models F \wedge G}{I \not\models F \mid I \not\models G}}
\end{equation*}

\begin{equation*}
    \frac{I \models F \vee G}{I \models F \mid I \models G}}  \text{ and }
 \frac{I \not\models F \vee G}{\parbox{2cm}{$I \not\models F$ \\ $I \not\models G$}} 
\end{equation*}

\begin{equation*}
    \frac{I \models F \to G}{I \not\models F \mid I \models G}}  \text{ and }
 \frac{I \not\models F \to G}{\parbox{2cm}{$I \models F$ \\ $I \not\models G$}} 
\end{equation*}

\begin{equation*}
    \frac{I \models F \leftrightarrow G}{I \models F \wedge G \mid I \not\models F \vee G}}  \text{ and }
 \frac{I \not\models F \leftrightarrow G}{I \models F \wedge \neg G \mid I \models \neg F \wedge G}} 
\end{equation*}

\begin{equation*}
    \frac{\parbox{2cm}{$I \models F$ \\ $I \not\models F$}}{I \models \bot}
\end{equation*}

Extension to First-order logic

The proof rules above apply in addition to the following proof rules for the quantifiers:

\begin{equation*}
  \frac{I \models \forall x. F}{I \vartriangleleft \{ x \mapsto v \} \models F}
\end{equation*}

for any $v$ in the domain of the interpretation.

\begin{equation*}
  \frac{I \not\models \exists x. F}{I \vartriangleleft \{ x \mapsto v \} \not\models F}
\end{equation*}

for any $v$ in the domain of the interpretation.

\begin{equation*}
  \frac{I \models \exists x. F}{I \vartriangleleft \{ x \mapsto v \} \models F}
\end{equation*}

for a fresh $v$ in the domain of the interpretation.

\begin{equation*}
  \frac{I \not\models \forall x. F}{I \vartriangleleft \{ x \mapsto v \} \not\models F}
\end{equation*}

for a fresh $v$ in the domain of the interpretation.

 
sav13/semantic_argument_method.txt · Last modified: 2015/04/21 17:33 (external edit)
 
© EPFL 2018 - Legal notice