| author | huffman |
| Sat, 16 Sep 2006 23:46:38 +0200 | |
| changeset 20557 | 81dd3679f92c |
| parent 19969 | c72e2110c026 |
| permissions | -rw-r--r-- |
|
19492
29c6cba140da
added some helper files for HOL goals/lemmas. Clauses have TPTP format.
mengj
parents:
diff
changeset
|
1 |
%ID: $Id$ |
|
29c6cba140da
added some helper files for HOL goals/lemmas. Clauses have TPTP format.
mengj
parents:
diff
changeset
|
2 |
%Author: Jia Meng, NICTA |
|
29c6cba140da
added some helper files for HOL goals/lemmas. Clauses have TPTP format.
mengj
parents:
diff
changeset
|
3 |
%typed combinator reduction for full-types (include S) |
|
29c6cba140da
added some helper files for HOL goals/lemmas. Clauses have TPTP format.
mengj
parents:
diff
changeset
|
4 |
|
|
29c6cba140da
added some helper files for HOL goals/lemmas. Clauses have TPTP format.
mengj
parents:
diff
changeset
|
5 |
%K P Q --> P |
|
29c6cba140da
added some helper files for HOL goals/lemmas. Clauses have TPTP format.
mengj
parents:
diff
changeset
|
6 |
input_clause(a1,axiom, |
|
29c6cba140da
added some helper files for HOL goals/lemmas. Clauses have TPTP format.
mengj
parents:
diff
changeset
|
7 |
[++equal(typeinfo(hAPP(typeinfo(hAPP(typeinfo(c_COMBK,tc_fun(A,tc_fun(B,A))),typeinfo(P,A)),tc_fun(B,A)),typeinfo(Q,B)),A),typeinfo(P,A))]). |
|
29c6cba140da
added some helper files for HOL goals/lemmas. Clauses have TPTP format.
mengj
parents:
diff
changeset
|
8 |
|
|
29c6cba140da
added some helper files for HOL goals/lemmas. Clauses have TPTP format.
mengj
parents:
diff
changeset
|
9 |
%S P Q R --> P R (Q R) |
|
29c6cba140da
added some helper files for HOL goals/lemmas. Clauses have TPTP format.
mengj
parents:
diff
changeset
|
10 |
input_clause(a2,axiom, |
|
29c6cba140da
added some helper files for HOL goals/lemmas. Clauses have TPTP format.
mengj
parents:
diff
changeset
|
11 |
[++equal(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(c_COMBS,tc_fun(tc_fun(A,tc_fun(B,C)),tc_fun(tc_fun(A,B),tc_fun(A,C)))),typeinfo(P,tc_fun(A,tc_fun(B,C)))),tc_fun(tc_fun(A,B),tc_fun(A,C))),typeinfo(Q,tc_fun(A,B))),tc_fun(A,C)),typeinfo(R,A)),C),typeinfo(hAPP(typeinfo(hAPP(typeinfo(P,tc_fun(A,tc_fun(B,C))),typeinfo(R,A)),tc_fun(B,C)),typeinfo(hAPP(typeinfo(Q,tc_fun(A,B)),typeinfo(R,A)),B)),C))]). |
|
29c6cba140da
added some helper files for HOL goals/lemmas. Clauses have TPTP format.
mengj
parents:
diff
changeset
|
12 |
|
|
29c6cba140da
added some helper files for HOL goals/lemmas. Clauses have TPTP format.
mengj
parents:
diff
changeset
|
13 |
%I P --> P |
|
29c6cba140da
added some helper files for HOL goals/lemmas. Clauses have TPTP format.
mengj
parents:
diff
changeset
|
14 |
input_clause(a3,axiom, |
|
29c6cba140da
added some helper files for HOL goals/lemmas. Clauses have TPTP format.
mengj
parents:
diff
changeset
|
15 |
[++equal(typeinfo(hAPP(typeinfo(c_COMBI,tc_fun(T,T)),typeinfo(P,T)),T),typeinfo(P,T))]). |
|
29c6cba140da
added some helper files for HOL goals/lemmas. Clauses have TPTP format.
mengj
parents:
diff
changeset
|
16 |
|
|
29c6cba140da
added some helper files for HOL goals/lemmas. Clauses have TPTP format.
mengj
parents:
diff
changeset
|
17 |
%B P Q R --> P(Q R) |
|
29c6cba140da
added some helper files for HOL goals/lemmas. Clauses have TPTP format.
mengj
parents:
diff
changeset
|
18 |
input_clause(a4,axiom, |
|
29c6cba140da
added some helper files for HOL goals/lemmas. Clauses have TPTP format.
mengj
parents:
diff
changeset
|
19 |
[++equal(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(c_COMBB,tc_fun(tc_fun(A,B),tc_fun(tc_fun(C,A),tc_fun(C,B)))),typeinfo(P,tc_fun(A,B))),tc_fun(tc_fun(C,A),tc_fun(C,B))),typeinfo(Q,tc_fun(C,A))),tc_fun(C,B)),typeinfo(R,C)),B),typeinfo(hAPP(typeinfo(P,tc_fun(A,B)),typeinfo(hAPP(typeinfo(Q,tc_fun(C,A)),typeinfo(R,C)),A)),B))]). |
|
29c6cba140da
added some helper files for HOL goals/lemmas. Clauses have TPTP format.
mengj
parents:
diff
changeset
|
20 |
|
|
29c6cba140da
added some helper files for HOL goals/lemmas. Clauses have TPTP format.
mengj
parents:
diff
changeset
|
21 |
|
|
29c6cba140da
added some helper files for HOL goals/lemmas. Clauses have TPTP format.
mengj
parents:
diff
changeset
|
22 |
%C P Q R --> P R Q |
|
29c6cba140da
added some helper files for HOL goals/lemmas. Clauses have TPTP format.
mengj
parents:
diff
changeset
|
23 |
input_clause(a5,axiom, |
|
29c6cba140da
added some helper files for HOL goals/lemmas. Clauses have TPTP format.
mengj
parents:
diff
changeset
|
24 |
[++equal(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(c_COMBC,tc_fun(tc_fun(A,tc_fun(B,C)),tc_fun(B,tc_fun(A,C)))),typeinfo(P,tc_fun(A,tc_fun(B,C)))),tc_fun(B,tc_fun(A,C))),typeinfo(Q,B)),tc_fun(A,C)),typeinfo(R,A)),C),typeinfo(hAPP(typeinfo(hAPP(typeinfo(P,tc_fun(A,tc_fun(B,C))),typeinfo(R,A)),tc_fun(B,C)),typeinfo(Q,B)),C))]). |
|
29c6cba140da
added some helper files for HOL goals/lemmas. Clauses have TPTP format.
mengj
parents:
diff
changeset
|
25 |
|
|
29c6cba140da
added some helper files for HOL goals/lemmas. Clauses have TPTP format.
mengj
parents:
diff
changeset
|
26 |
input_clause(a6,axiom, |
|
29c6cba140da
added some helper files for HOL goals/lemmas. Clauses have TPTP format.
mengj
parents:
diff
changeset
|
27 |
[--hBOOL(typeinfo(hAPP(typeinfo(hAPP(typeinfo(fequal,tc_fun(A,tc_fun(A,tc_bool))),typeinfo(X,A)),tc_fun(A,tc_bool)),typeinfo(Y,A)),tc_bool)), |
|
29c6cba140da
added some helper files for HOL goals/lemmas. Clauses have TPTP format.
mengj
parents:
diff
changeset
|
28 |
++equal(typeinfo(X,A),typeinfo(Y,A))]). |
|
29c6cba140da
added some helper files for HOL goals/lemmas. Clauses have TPTP format.
mengj
parents:
diff
changeset
|
29 |
|
| 19969 | 30 |
input_clause(a7,axiom, |
|
19492
29c6cba140da
added some helper files for HOL goals/lemmas. Clauses have TPTP format.
mengj
parents:
diff
changeset
|
31 |
[++hBOOL(typeinfo(hAPP(typeinfo(hAPP(typeinfo(fequal,tc_fun(A,tc_fun(A,tc_bool))),typeinfo(X,A)),tc_fun(A,tc_bool)),typeinfo(Y,A)),tc_bool)), |
|
29c6cba140da
added some helper files for HOL goals/lemmas. Clauses have TPTP format.
mengj
parents:
diff
changeset
|
32 |
--equal(typeinfo(X,A),typeinfo(Y,A))]). |
|
29c6cba140da
added some helper files for HOL goals/lemmas. Clauses have TPTP format.
mengj
parents:
diff
changeset
|
33 |
|
|
29c6cba140da
added some helper files for HOL goals/lemmas. Clauses have TPTP format.
mengj
parents:
diff
changeset
|
34 |