1465
|
1 |
(* Title: HOL/ex/unsolved
|
969
|
2 |
ID: $Id$
|
1465
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
969
|
4 |
Copyright 1992 University of Cambridge
|
|
5 |
|
|
6 |
Problems that currently defeat the MESON procedure as well as best_tac
|
|
7 |
*)
|
|
8 |
|
1586
|
9 |
(*from Vladimir Lifschitz, What Is the Inverse Method?, JAR 5 1989. 1--23*)
|
2031
|
10 |
(*27 clauses; 81 Horn clauses*)
|
1586
|
11 |
goal HOL.thy "? x x'. ! y. ? z z'. (~P y y | P x x | ~S z x) & \
|
|
12 |
\ (S x y | ~S y z | Q z' z') & \
|
|
13 |
\ (Q x' y | ~Q y z' | S x' x')";
|
969
|
14 |
|
|
15 |
|
|
16 |
|
|
17 |
writeln"Problem 55";
|
|
18 |
|
1586
|
19 |
(*Original, equational version by Len Schubert [via Pelletier] *)
|
969
|
20 |
goal HOL.thy
|
1586
|
21 |
"(? x. lives x & killed x agatha) & \
|
|
22 |
\ lives agatha & lives butler & lives charles & \
|
|
23 |
\ (! x. lives x --> x=agatha | x=butler | x=charles) & \
|
|
24 |
\ (! x y. killed x y --> hates x y) & \
|
|
25 |
\ (! x y. killed x y --> ~richer x y) & \
|
|
26 |
\ (! x. hates agatha x --> ~hates charles x) & \
|
|
27 |
\ (! x. ~ x=butler --> hates agatha x) & \
|
|
28 |
\ (! x. ~richer x agatha --> hates butler x) & \
|
|
29 |
\ (! x. hates agatha x --> hates butler x) & \
|
|
30 |
\ (! x. ? y. ~hates x y) & \
|
969
|
31 |
\ ~ agatha=butler --> \
|
1586
|
32 |
\ killed agatha agatha";
|
969
|
33 |
|
1586
|
34 |
(*Halting problem: Formulation of Li Dafa (AAR Newsletter 27, Oct 1994.)
|
2031
|
35 |
author U. Egly; 46 clauses; 264 Horn clauses*)
|
1586
|
36 |
goal HOL.thy
|
|
37 |
"((EX X. (a X) & (ALL Y. (c Y) --> (ALL Z. (d X Y Z)))) --> \
|
|
38 |
\ (EX W. (c W) & (ALL Y. (c Y) --> (ALL Z. (d W Y Z))))) \
|
|
39 |
\ & \
|
|
40 |
\ (ALL W. (c W) & (ALL U. (c U) --> (ALL V. (d W U V))) --> \
|
|
41 |
\ (ALL Y Z. \
|
|
42 |
\ ((c Y) & (h2 Y Z) --> (h3 W Y Z) & (oo W g)) & \
|
|
43 |
\ ((c Y) & ~(h2 Y Z) --> (h3 W Y Z) & (oo W b)))) \
|
|
44 |
\ & \
|
|
45 |
\ (ALL W. (c W) & \
|
|
46 |
\ (ALL Y Z. \
|
|
47 |
\ ((c Y) & (h2 Y Z) --> (h3 W Y Z) & (oo W g)) & \
|
|
48 |
\ ((c Y) & ~(h2 Y Z) --> (h3 W Y Z) & (oo W b))) --> \
|
|
49 |
\ (EX V. (c V) & \
|
|
50 |
\ (ALL Y. (((c Y) & (h3 W Y Y)) & (oo W g) --> ~(h2 V Y)) & \
|
|
51 |
\ (((c Y) & (h3 W Y Y)) & (oo W b) --> (h2 V Y) & (oo V b))))) \
|
|
52 |
\ --> \
|
|
53 |
\ ~ (EX X. (a X) & (ALL Y. (c Y) --> (ALL Z. (d X Y Z))))";
|
969
|
54 |
|