Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/Sources/formale Sprachen/Isabelle/Sequents/LK/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 11 kB

Quelle Hard_Quantifiers.thy Sprache: Isabelle

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

Hard examples with quantifiers.  Can be read to test the LK system.
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.

Uses pc_tac rather than fast_tac when the former is significantly faster.
*)

theory Hard_Quantifiers
imports "../LK"
begin

lemma "\ (\x. P(x) \ Q(x)) \ (\x. P(x)) \ (\x. Q(x))"
  by fast

lemma "\ (\x. P \ Q(x)) \ (P \ (\x. Q(x)))"
  by fast

lemma "\ (\x. P(x) \ Q) \ (\x. P(x)) \ Q"
  by fast

lemma "\ (\x. P(x)) \ Q \ (\x. P(x) \ Q)"
  by fast

text "Problems requiring quantifier duplication"

(*Not provable by fast: needs multiple instantiation of \<forall>*)
lemma "\ (\x. P(x) \ P(f(x))) \ P(d) \ P(f(f(f(d))))"
  by best_dup

(*Needs double instantiation of the quantifier*)
lemma "\ \x. P(x) \ P(a) \ P(b)"
  by fast_dup

lemma "\ \z. P(z) \ (\x. P(x))"
  by best_dup

text "Hard examples with quantifiers"

text "Problem 18"
lemma "\ \y. \x. P(y)\P(x)"
  by best_dup

text "Problem 19"
lemma "\ \x. \y z. (P(y)\Q(z)) \ (P(x)\Q(x))"
  by best_dup

text "Problem 20"
lemma "\ (\x y. \z. \w. (P(x) \ Q(y)\R(z) \ S(w)))
    \<longrightarrow> (\<exists>x y. P(x) \<and> Q(y)) \<longrightarrow> (\<exists>z. R(z))"
  by fast

text "Problem 21"
lemma "\ (\x. P \ Q(x)) \ (\x. Q(x) \ P) \ (\x. P \ Q(x))"
  by best_dup

text "Problem 22"
lemma "\ (\x. P \ Q(x)) \ (P \ (\x. Q(x)))"
  by fast

text "Problem 23"
lemma "\ (\x. P \ Q(x)) \ (P \ (\x. Q(x)))"
  by best

text "Problem 24"
lemma "\ \ (\x. S(x) \ Q(x)) \ (\x. P(x) \ Q(x) \ R(x)) \
     \<not> (\<exists>x. P(x)) \<longrightarrow> (\<exists>x. Q(x)) \<and> (\<forall>x. Q(x) \<or> R(x) \<longrightarrow> S(x))
    \<longrightarrow> (\<exists>x. P(x) \<and> R(x))"
  by pc

text "Problem 25"
lemma "\ (\x. P(x)) \
        (\<forall>x. L(x) \<longrightarrow> \<not> (M(x) \<and> R(x))) \<and>
        (\<forall>x. P(x) \<longrightarrow> (M(x) \<and> L(x))) \<and>
        ((\<forall>x. P(x)\<longrightarrow>Q(x)) \<or> (\<exists>x. P(x) \<and> R(x)))
    \<longrightarrow> (\<exists>x. Q(x) \<and> P(x))"
  by best

text "Problem 26"
lemma "\ ((\x. p(x)) \ (\x. q(x))) \
      (\<forall>x. \<forall>y. p(x) \<and> q(y) \<longrightarrow> (r(x) \<longleftrightarrow> s(y)))
  \<longrightarrow> ((\<forall>x. p(x)\<longrightarrow>r(x)) \<longleftrightarrow> (\<forall>x. q(x)\<longrightarrow>s(x)))"
  by pc

text "Problem 27"
lemma "\ (\x. P(x) \ \ Q(x)) \
              (\<forall>x. P(x) \<longrightarrow> R(x)) \<and>
              (\<forall>x. M(x) \<and> L(x) \<longrightarrow> P(x)) \<and>
              ((\<exists>x. R(x) \<and> \<not> Q(x)) \<longrightarrow> (\<forall>x. L(x) \<longrightarrow> \<not> R(x)))
          \<longrightarrow> (\<forall>x. M(x) \<longrightarrow> \<not> L(x))"
  by pc

text "Problem 28. AMENDED"
lemma "\ (\x. P(x) \ (\x. Q(x))) \
        ((\<forall>x. Q(x) \<or> R(x)) \<longrightarrow> (\<exists>x. Q(x) \<and> S(x))) \<and>
        ((\<exists>x. S(x)) \<longrightarrow> (\<forall>x. L(x) \<longrightarrow> M(x)))
    \<longrightarrow> (\<forall>x. P(x) \<and> L(x) \<longrightarrow> M(x))"
  by pc

text "Problem 29. Essentially the same as Principia Mathematica *11.71"
lemma "\ (\x. P(x)) \ (\y. Q(y))
    \<longrightarrow> ((\<forall>x. P(x) \<longrightarrow> R(x)) \<and> (\<forall>y. Q(y) \<longrightarrow> S(y)) \<longleftrightarrow>
         (\<forall>x y. P(x) \<and> Q(y) \<longrightarrow> R(x) \<and> S(y)))"
  by pc

text "Problem 30"
lemma "\ (\x. P(x) \ Q(x) \ \ R(x)) \
        (\<forall>x. (Q(x) \<longrightarrow> \<not> S(x)) \<longrightarrow> P(x) \<and> R(x))
    \<longrightarrow> (\<forall>x. S(x))"
  by fast

text "Problem 31"
lemma "\ \ (\x. P(x) \ (Q(x) \ R(x))) \
        (\<exists>x. L(x) \<and> P(x)) \<and>
        (\<forall>x. \<not> R(x) \<longrightarrow> M(x))
    \<longrightarrow> (\<exists>x. L(x) \<and> M(x))"
  by fast

text "Problem 32"
lemma "\ (\x. P(x) \ (Q(x) \ R(x)) \ S(x)) \
        (\<forall>x. S(x) \<and> R(x) \<longrightarrow> L(x)) \<and>
        (\<forall>x. M(x) \<longrightarrow> R(x))
    \<longrightarrow> (\<forall>x. P(x) \<and> M(x) \<longrightarrow> L(x))"
  by best

text "Problem 33"
lemma "\ (\x. P(a) \ (P(x) \ P(b)) \ P(c)) \
     (\<forall>x. (\<not> P(a) \<or> P(x) \<or> P(c)) \<and> (\<not> P(a) \<or> \<not> P(b) \<or> P(c)))"
  by fast

text "Problem 34 AMENDED (TWICE!!)"
(*Andrews's challenge*)
lemma "\ ((\x. \y. p(x) \ p(y)) \
               ((\<exists>x. q(x)) \<longleftrightarrow> (\<forall>y. p(y))))     \<longleftrightarrow>
              ((\<exists>x. \<forall>y. q(x) \<longleftrightarrow> q(y))  \<longleftrightarrow>
               ((\<exists>x. p(x)) \<longleftrightarrow> (\<forall>y. q(y))))"
  by best_dup

text "Problem 35"
lemma "\ \x y. P(x,y) \ (\u v. P(u,v))"
  by best_dup

text "Problem 36"
lemma "\ (\x. \y. J(x,y)) \
         (\<forall>x. \<exists>y. G(x,y)) \<and>
         (\<forall>x y. J(x,y) \<or> G(x,y) \<longrightarrow>
         (\<forall>z. J(y,z) \<or> G(y,z) \<longrightarrow> H(x,z)))
         \<longrightarrow> (\<forall>x. \<exists>y. H(x,y))"
  by fast

text "Problem 37"
lemma "\ (\z. \w. \x. \y.
           (P(x,z)\<longrightarrow>P(y,w)) \<and> P(y,z) \<and> (P(y,w) \<longrightarrow> (\<exists>u. Q(u,w)))) \<and>
        (\<forall>x z. \<not> P(x,z) \<longrightarrow> (\<exists>y. Q(y,z))) \<and>
        ((\<exists>x y. Q(x,y)) \<longrightarrow> (\<forall>x. R(x,x)))
    \<longrightarrow> (\<forall>x. \<exists>y. R(x,y))"
  by pc

text "Problem 38"
lemma "\ (\x. p(a) \ (p(x) \ (\y. p(y) \ r(x,y))) \
                 (\<exists>z. \<exists>w. p(z) \<and> r(x,w) \<and> r(w,z)))  \<longleftrightarrow>
         (\<forall>x. (\<not> p(a) \<or> p(x) \<or> (\<exists>z. \<exists>w. p(z) \<and> r(x,w) \<and> r(w,z))) \<and>
                 (\<not> p(a) \<or> \<not> (\<exists>y. p(y) \<and> r(x,y)) \<or>
                 (\<exists>z. \<exists>w. p(z) \<and> r(x,w) \<and> r(w,z))))"
  by pc

text "Problem 39"
lemma "\ \ (\x. \y. F(y,x) \ \ F(y,y))"
  by fast

text "Problem 40. AMENDED"
lemma "\ (\y. \x. F(x,y) \ F(x,x)) \
         \<not> (\<forall>x. \<exists>y. \<forall>z. F(z,y) \<longleftrightarrow> \<not> F(z,x))"
  by fast

text "Problem 41"
lemma "\ (\z. \y. \x. f(x,y) \ f(x,z) \ \ f(x,x))
         \<longrightarrow> \<not> (\<exists>z. \<forall>x. f(x,z))"
  by fast

text "Problem 42"
lemma "\ \ (\y. \x. p(x,y) \ \ (\z. p(x,z) \ p(z,x)))"
  oops

text "Problem 43"
lemma "\ (\x. \y. q(x,y) \ (\z. p(z,x) \ p(z,y)))
          \<longrightarrow> (\<forall>x. (\<forall>y. q(x,y) \<longleftrightarrow> q(y,x)))"
  oops

text "Problem 44"
lemma "\ (\x. f(x) \
                 (\<exists>y. g(y) \<and> h(x,y) \<and> (\<exists>y. g(y) \<and> \<not> h(x,y)))) \<and>
         (\<exists>x. j(x) \<and> (\<forall>y. g(y) \<longrightarrow> h(x,y)))
         \<longrightarrow> (\<exists>x. j(x) \<and> \<not> f(x))"
  by fast

text "Problem 45"
lemma "\ (\x. f(x) \ (\y. g(y) \ h(x,y) \ j(x,y))
                      \<longrightarrow> (\<forall>y. g(y) \<and> h(x,y) \<longrightarrow> k(y))) \<and>
      \<not> (\<exists>y. l(y) \<and> k(y)) \<and>
      (\<exists>x. f(x) \<and> (\<forall>y. h(x,y) \<longrightarrow> l(y))
                   \<and> (\<forall>y. g(y) \<and> h(x,y) \<longrightarrow> j(x,y)))
      \<longrightarrow> (\<exists>x. f(x) \<and> \<not> (\<exists>y. g(y) \<and> h(x,y)))"
  by best

text "Problems (mainly) involving equality or functions"

text "Problem 48"
lemma "\ (a = b \ c = d) \ (a = c \ b = d) \ a = d \ b = c"
  by (fast add!: subst)

text "Problem 50"
lemma "\ (\x. P(a,x) \ (\y. P(x,y))) \ (\x. \y. P(x,y))"
  by best_dup

text "Problem 51"
lemma "\ (\z w. \x y. P(x,y) \ (x = z \ y = w)) \
         (\<exists>z. \<forall>x. \<exists>w. (\<forall>y. P(x,y) \<longleftrightarrow> y = w) \<longleftrightarrow> x = z)"
  by (fast add!: subst)

text "Problem 52"  (*Almost the same as 51. *)
lemma "\ (\z w. \x y. P(x,y) \ (x = z \ y = w)) \
         (\<exists>w. \<forall>y. \<exists>z. (\<forall>x. P(x,y) \<longleftrightarrow> x = z) \<longleftrightarrow> y = w)"
  by (fast add!: subst)

text "Problem 56"
lemma "\ (\x.(\y. P(y) \ x = f(y)) \ P(x)) \ (\x. P(x) \ P(f(x)))"
  by (best add: symL subst)
  (*requires tricker to orient the equality properly*)

text "Problem 57"
lemma "\ P(f(a,b), f(b,c)) \ P(f(b,c), f(a,c)) \
         (\<forall>x y z. P(x,y) \<and> P(y,z) \<longrightarrow> P(x,z)) \<longrightarrow> P(f(a,b), f(a,c))"
  by fast

text "Problem 58!"
lemma "\ (\x y. f(x) = g(y)) \ (\x y. f(f(x)) = f(g(y)))"
  by (fast add!: subst)

text "Problem 59"
(*Unification works poorly here -- the abstraction %sobj prevents efficient
  operation of the occurs check*)
lemma "\ (\x. P(x) \ \ P(f(x))) \ (\x. P(x) \ \ P(f(x)))"
  using [[unify_trace_bound = 50]]
  by best_dup

text "Problem 60"
lemma "\ \x. P(x,f(x)) \ (\y. (\z. P(z,y) \ P(z,f(x))) \ P(x,y))"
  by fast

text "Problem 62 as corrected in JAR 18 (1997), page 135"
lemma "\ (\x. p(a) \ (p(x) \ p(f(x))) \ p(f(f(x)))) \
      (\<forall>x. (\<not> p(a) \<or> p(x) \<or> p(f(f(x)))) \<and>
              (\<not> p(a) \<or> \<not> p(f(x)) \<or> p(f(f(x)))))"
  by fast

(*18 June 92: loaded in 372 secs*)
(*19 June 92: loaded in 166 secs except #34, using repeat_goal_tac*)
(*29 June 92: loaded in 370 secs*)
(*18 September 2005: loaded in 1.809 secs*)

end

quality100%

¤ Dauer der Verarbeitung: 0.15 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.