[opentheory-users] statistics based on opentheory

[Joe Leslie-Hurd]

Hi Robert,

The central concept in OpenTheory is the theory, which consists of

- A set of assumptions
- A set of theorems
- A proof that the theorems logically derive from the assumptions

So to take your second question first, in the output from

opentheory info --theory --show-assumptions --show-derivations pair

you will see printed a set of assumptions, numbered with (1), (2),
etc., followed by a set of theorems of the form

{ (i) (j) ... (k) } |- theorem

which means that the proof of the theorem depended on the numbered
assumptions (i) (j) ... (k).

And now to answer your first question, the OpenTheory fork of HOL
Light is not set up to track proofs back to the 3 axioms, but rather
to the most recent theory boundary. However, with just a little bit of
hacking we can fix that! Just add the line

Export.debug_export_thm_enable := false;;

after loads "opentheory/opentheory.ml";; in hol.ml, and then load
everything in with

#use "hol.ml";;

as normal. Now you can use the read_proof function to examine the
proofs of theorems all the way back to the axioms:

# read_proof EXCLUDED_MIDDLE;;
val it : proof =
  Eq_mp_proof (|- (!t. t \/ ~t) <=> (!t. t \/ ~t), |- !t. t \/ ~t)

With the read_proof building block you can write an ocaml function
that traverses a proof and extracts the set of axioms it finds, and
you will have what you need inside HOL Light.

Cheers,

Joe


On Mon, Jun 8, 2015 at 12:27 PM, Robert White
<ai.robert.wangshuai at gmail.com> wrote:
> Dear Joe,
>
> 1) Is there any function I can call in (OpenTheory's) HOL Light to test
> which axioms it is based on and how the dependency looks like? (to avoid
> collecting the result and do analysis from the terminal, which is too
> painful for a guy with poor eye sight)
>
>
> 2) I wonder what this is stating if I run the following command instead:
>  opentheory info --theory --show-assumptions --show-derivations pair
>
> Looks like it is also trying to find out what the dependency is like but
> this time much more complicated?
>
> 2 external type operators: -> bool
> 10 external constants: = select ! /\ ==> ? \/ ~ F T
> 20 theorems:
>   {(1) (2) (3) (8) (10) (11) (12) (13) (14) (15) (16) (17) (20) (21) (22)
>      (25) (26) (27) (28) (31) (32) (33) (34) (35) (36) (37) (38) (39) (41)
>      (42) (43) (44) (45) (46) (47)}
>     |- !x. (fst x, snd x) = x
>   {(1) (2) (3) (8) (10) (11) (12) (13) (15) (16) (17) (20) (21) (22) (25)
>      (26) (27) (28) (31) (32) (33) (34) (35) (36) (37) (38) (39) (41) (42)
>      (43) (44) (45) (46) (47)}
>     |- !a b. fst (a, b) = a
>   {(1) (2) (3) (8) (10) (11) (12) (13) (15) (16) (17) (20) (21) (22) (25)
>      (26) (27) (28) (31) (32) (33) (34) (35) (36) (37) (38) (39) (41) (42)
>      (43) (44) (45) (46) (47)}
>     |- !a b. snd (a, b) = b
>   {(1) (8) (10) (11) (12) (14) (26) (27) (33) (35) (36)}
>     |- !x. ?a b. x = (a, b)
>   {(1) (2) (3) (4) (8) (10) (11) (12) (13) (14) (15) (16) (17) (18) (19)
>      (20) (21) (22) (23) (24) (25) (26) (27) (28) (31) (32) (33) (34) (35)
>      (36) (37) (38) (39) (40) (41) (42) (43) (44) (45) (46) (47) (48) (49)}
>     |- !p. (!x. p x) <=> !a b. p (a, b)
>   {(1) (2) (3) (4) (5) (6) (7) (8) (10) (11) (12) (13) (14) (15) (16) (17)
>      (18) (19) (20) (21) (22) (23) (24) (25) (26) (27) (28) (31) (32) (33)
>      (34) (35) (36) (37) (38) (39) (40) (41) (42) (43) (44) (45) (46) (47)
>      (48) (49)}
>     |- !p. (?x. p x) <=> ?a b. p (a, b)
>   {(1) (2) (3) (8) (10) (11) (12) (13) (14) (15) (16) (17) (20) (21) (22)
>      (25) (26) (27) (28) (31) (32) (33) (34) (35) (36) (37) (38) (39) (41)
>      (42) (43) (44) (45) (46) (47)}
>     |- !p. (!a b. p (a, b)) ==> !x. p x
>   {(1) (2) (3) (8) (9) (10) (11) (12) (13) (15) (16) (17) (20) (21) (22)
>      (25) (26) (27) (28) (29) (30) (31) (32) (33) (34) (35) (36) (37) (38)
>      (39) (41) (42) (43) (44) (45) (46) (47)}
>     |- !p. (!f. p f) <=> !f. p (\a b. f (a, b))
>   {(1) (2) (3) (4) (8) (9) (10) (11) (12) (13) (15) (16) (17) (20) (21)
>      (22) (25) (26) (27) (28) (29) (30) (31) (32) (33) (34) (35) (36) (37)
>      (38) (39) (41) (42) (43) (44) (45) (46) (47)}
>     |- !p. (?f. p f) <=> ?f. p (\a b. f (a, b))
>   {(1) (2) (3) (8) (9) (10) (11) (12) (13) (15) (16) (17) (20) (21) (22)
>      (25) (26) (27) (28) (31) (32) (33) (34) (35) (36) (37) (38) (39) (41)
>      (42) (43) (44) (45) (46) (47)}
>     |- !f. ?fn. !a b. fn (a, b) = f a b
>   {(1) (2) (3) (4) (8) (9) (10) (11) (12) (13) (14) (15) (16) (17) (18)
>      (19) (20) (21) (22) (23) (24) (25) (26) (27) (28) (31) (32) (33) (34)
>      (35) (36) (37) (38) (39) (40) (41) (42) (43) (44) (45) (46) (47) (48)
>      (49)}
>     |- !p. (!x y. p x y) <=> !z. p (fst z) (snd z)
>   {(1) (2) (3) (4) (5) (6) (7) (8) (9) (10) (11) (12) (13) (14) (15) (16)
>      (17) (18) (19) (20) (21) (22) (23) (24) (25) (26) (27) (28) (31) (32)
>      (33) (34) (35) (36) (37) (38) (39) (40) (41) (42) (43) (44) (45) (46)
>      (47) (48) (49)}
>     |- !p. (?x y. p x y) <=> ?z. p (fst z) (snd z)
>   {(1) (2) (3) (4) (8) (9) (10) (11) (12) (13) (14) (15) (16) (17) (18)
>      (19) (20) (21) (22) (23) (24) (25) (26) (27) (28) (29) (30) (31) (32)
>      (33) (34) (35) (36) (37) (38) (39) (40) (41) (42) (43) (44) (45) (46)
>      (47) (48) (49)}
>     |- !f. (\x. f x) = \(a, b). f (a, b)
>   {(1) (2) (3) (8) (10) (11) (12) (13) (15) (16) (17) (20) (21) (22) (25)
>      (26) (27) (28) (31) (32) (33) (34) (35) (36) (37) (38) (39) (41) (42)
>      (43) (44) (46) (47)}
>     |- !a b a' b'. (a, b) = (a', b') <=> a = a' /\ b = b'
>   {(1) (2) (3) (4) (8) (9) (10) (11) (12) (13) (14) (15) (16) (17) (18)
>      (19) (20) (21) (22) (23) (24) (25) (26) (27) (28) (29) (30) (31) (32)
>      (33) (34) (35) (36) (37) (38) (39) (40) (41) (42) (43) (44) (45) (46)
>      (47) (48) (49)}
>     |- !p. (!f. p f) <=> !f. p (\(a, b). f a b)
>   {(1) (2) (3) (4) (8) (9) (10) (11) (12) (13) (14) (15) (16) (17) (18)
>      (19) (20) (21) (22) (23) (24) (25) (26) (27) (28) (29) (30) (31) (32)
>      (33) (34) (35) (36) (37) (38) (39) (40) (41) (42) (43) (44) (45) (46)
>      (47) (48) (49)}
>     |- !p. (?f. p f) <=> ?f. p (\(a, b). f a b)
>   {(1) (2) (3) (4) (8) (9) (10) (11) (12) (13) (14) (15) (16) (17) (18)
>      (19) (20) (21) (22) (23) (24) (25) (26) (27) (28) (29) (30) (31) (32)
>      (33) (34) (35) (36) (37) (38) (39) (40) (41) (42) (43) (44) (45) (46)
>      (47) (48) (49)}
>     |- !p. (!(a, b). p a b) <=> !a b. p a b
>   {(1) (2) (3) (4) (8) (9) (10) (11) (12) (13) (14) (15) (16) (17) (18)
>      (19) (20) (21) (22) (23) (24) (25) (26) (27) (28) (29) (30) (31) (32)
>      (33) (34) (35) (36) (37) (38) (39) (40) (41) (42) (43) (44) (45) (46)
>      (47) (48) (49)}
>     |- !p. (?(a, b). p a b) <=> ?a b. p a b
>   {(1) (2) (3) (4) (8) (9) (10) (11) (12) (13) (14) (15) (16) (17) (18)
>      (19) (20) (21) (22) (23) (24) (25) (26) (27) (28) (29) (30) (31) (32)
>      (33) (34) (35) (36) (37) (38) (39) (40) (41) (42) (43) (44) (45) (46)
>      (47) (48) (49)}
>     |- !p. (!(a, b, c). p a b c) <=> !a b c. p a b c
>   {(1) (2) (3) (4) (8) (9) (10) (11) (12) (13) (14) (15) (16) (17) (18)
>      (19) (20) (21) (22) (23) (24) (25) (26) (27) (28) (29) (30) (31) (32)
>      (33) (34) (35) (36) (37) (38) (39) (40) (41) (42) (43) (44) (45) (46)
>      (47) (48) (49)}
>     |- !p. (?(a, b, c). p a b c) <=> ?a b c. p a b c
>
> Looks confusing without any comments explaining what I got here.
>
> Thanks very much!
> --
>
> Regards,
> Robert White (Shuai Wang)
> INRIA Deducteam
> [Moving to ILLC of UvA from this Sep. ]
> [New email address will be shuai.wang at student.uva.nl]
>