- English only

# Lab for Automated Reasoning and Analysis LARA

# Differences

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

sav08:proof_theory_for_propositional_logic [2008/03/09 19:43] vkuncak |
sav08:proof_theory_for_propositional_logic [2015/04/21 17:30] (current) |
||
---|---|---|---|

Line 15: | Line 15: | ||

System $S$ is sound if for every formula $F$, | System $S$ is sound if for every formula $F$, | ||

- | \[ | + | \begin{equation*} |

(\vdash_S F) \rightarrow (\models F) | (\vdash_S F) \rightarrow (\models F) | ||

- | \] | + | \end{equation*} |

We can only prove true formulas. | We can only prove true formulas. | ||

Line 23: | Line 23: | ||

System $S$ is complete if for every formula $F$, | System $S$ is complete if for every formula $F$, | ||

- | \[ | + | \begin{equation*} |

(\models F) \rightarrow (\vdash F) | (\models F) \rightarrow (\vdash F) | ||

- | \] | + | \end{equation*} |

We can prove all valid formulas. | We can prove all valid formulas. | ||

- | ===== Case analysis proof system ===== | + | ===== Some Example Proof Systems ===== |

- | A sound and complete proof system. | + | === Case analysis proof system === |

- | Case analysis rule: | + | A simple A sound and complete proof system. |

- | \[ | + | |

+ | **Rule 1:** Case analysis rule: | ||

+ | \begin{equation*} | ||

\frac{P\{p \mapsto {\it true}\}\ ;\ P\{p \mapsto {\it false}\}} | \frac{P\{p \mapsto {\it true}\}\ ;\ P\{p \mapsto {\it false}\}} | ||

{P} | {P} | ||

- | \] | + | \end{equation*} |

- | Evaluation rule: derive $P$ if $P$ has no variables and it evaluates to //true//. | + | **Rule 2:** Evaluation rule: derive $P$ if $P$ has no variables and it evaluates to //true//. |

- | Adding simplification rules. Adding sound rules preserves soundness and completeness. | + | We can also add simplification rules. Adding sound rules preserves soundness and completeness. |

- | ===== Gentzen proof system ===== | + | === Gentzen proof system === |

Recall Gentzen's proof system from [[proofs and induction]] part of [[lecture02]], ignoring rules for predicates and induction. | Recall Gentzen's proof system from [[proofs and induction]] part of [[lecture02]], ignoring rules for predicates and induction. | ||

- | ===== Resolution ===== | + | === Resolution === |

- | | + | |

- | Definition and soundness. Completeness in next lecture. | + | |

+ | [[Definition of Propositional Resolution]] | ||