products/sources/formale Sprachen/Java/openjdk-20-36_src/test/jdk/sun/nio/cs/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Propositional.thy   Sprache: Unknown

(*  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

[ Dauer der Verarbeitung: 0.15 Sekunden  (vorverarbeitet)  ]