Quelle Propositional.thy Sprache: Isabelle

(*  Title:      Sequents/LK/Propositional.thy
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1992  University of Cambridge
*)

section \<open>Classical sequent calculus: examples with propositional connectives\<close>

theory Propositional
imports "../LK"
begin

text "absorptive laws of \ and \"

lemma "\ P \ P \ P"
  by fast_prop

lemma "\ P \ P \ P"
  by fast_prop

text "commutative laws of \ and \"

lemma "\ P \ Q \ Q \ P"
  by fast_prop

lemma "\ P \ Q \ Q \ P"
  by fast_prop

text "associative laws of \ and \"

lemma "\ (P \ Q) \ R \ P \ (Q \ R)"
  by fast_prop

lemma "\ (P \ Q) \ R \ P \ (Q \ R)"
  by fast_prop

text "distributive laws of \ and \"

lemma "\ (P \ Q) \ R \ (P \ R) \ (Q \ R)"
  by fast_prop

lemma "\ (P \ Q) \ R \ (P \ R) \ (Q \ R)"
  by fast_prop

text "Laws involving implication"

lemma "\ (P \ Q \ R) \ (P \ R) \ (Q \ R)"
  by fast_prop

lemma "\ (P \ Q \ R) \ (P \ (Q \ R))"
  by fast_prop

lemma "\ (P \ Q \ R) \ (P \ Q) \ (P \ R)"
  by fast_prop

text "Classical theorems"

lemma "\ P \ Q \ P \ \ P \ Q"
  by fast_prop

lemma "\ (P \ Q) \ (\ P \ R) \ (P \ Q \ R)"
  by fast_prop

lemma "\ P \ Q \ \ P \ R \ (P \ Q) \ (\ P \ R)"
  by fast_prop

lemma "\ (P \ Q) \ (P \ R) \ (P \ Q \ R)"
  by fast_prop

(*If and only if*)

lemma "\ (P \ Q) \ (Q \ P)"
  by fast_prop

lemma "\ \ (P \ \ P)"
  by fast_prop

(*Sample problems from
  F. J. Pelletier,
  Seventy-Five Problems for Testing Automatic Theorem Provers,
  J. Automated Reasoning 2 (1986), 191-216.
  Errata, JAR 4 (1988), 236-236.
*)

(*1*)
lemma "\ (P \ Q) \ (\ Q \ \ P)"
  by fast_prop

(*2*)
lemma "\ \ \ P \ P"
  by fast_prop

(*3*)
lemma "\ \ (P \ Q) \ (Q \ P)"
  by fast_prop

(*4*)
lemma "\ (\ P \ Q) \ (\ Q \ P)"
  by fast_prop

(*5*)
lemma "\ ((P \ Q) \ (P \ R)) \ (P \ (Q \ R))"
  by fast_prop

(*6*)
lemma "\ P \ \ P"
  by fast_prop

(*7*)
lemma "\ P \ \ \ \ P"
  by fast_prop

(*8.  Peirce's law*)
lemma "\ ((P \ Q) \ P) \ P"
  by fast_prop

(*9*)
lemma "\ ((P \ Q) \ (\ P \ Q) \ (P \ \ Q)) \ \ (\ P \ \ Q)"
  by fast_prop

(*10*)
lemma "Q \ R, R \ P \ Q, P \ (Q \ R) \ P \ Q"
  by fast_prop

(*11.  Proved in each direction (incorrectly, says Pelletier!!)  *)
lemma "\ P \ P"
  by fast_prop

(*12.  "Dijkstra's law"*)
lemma "\ ((P \ Q) \ R) \ (P \ (Q \ R))"
  by fast_prop

(*13.  Distributive law*)
lemma "\ P \ (Q \ R) \ (P \ Q) \ (P \ R)"
  by fast_prop

(*14*)
lemma "\ (P \ Q) \ ((Q \ \ P) \ (\ Q \ P))"
  by fast_prop

(*15*)
lemma "\ (P \ Q) \ (\ P \ Q)"
  by fast_prop

(*16*)
lemma "\ (P \ Q) \ (Q \ P)"
  by fast_prop

(*17*)
lemma "\ ((P \ (Q \ R)) \ S) \ ((\ P \ Q \ S) \ (\ P \ \ R \ S))"
  by fast_prop

end

quality100%

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.