Re: [Hol-info] Visualizing subgoals in a proof script

Dear Mario, >Hello. In HOL4 is there a way to generate something like the entries in >Metamath proof explorer for the subgoals generated within a proof and >the tactics used to solve them? Example: > For HOL Light there is Mark Adams's "tactician"

Re: [Hol-info] Installation Problem of HOL-Light

Dear all, Some time ago (in the times of Debian Stretch :-)) I made a Dockerfile for HOL Light, see the attachment. The commands I used for building the image and running it are: docker build -t hol-light . docker run -i -v /home/freek:/home/freek --name hol-light hol-light You need to run

Re: [Hol-info] 0 / 0 = 0 ???

Dear all, For what it's worth, a definition of division with 0/0 = 0 won't be possible constructively, because in constructive mathematics all functions of type real->real are continuous, and with this definition division is _not_ continuous. Also, in IEEE 754 floating point of course division

Re: [Hol-info] Tactic

Hi Dylan, What I would try in HOL Light: # g `a ==> b /\ c ==> d /\ e ==> k`;; Warning: Free variables in goal: a, b, c, d, e, k val it : goalstack = 1 subgoal (1 total) `a ==> b /\ c ==> d /\ e ==> k` # e (REPEAT DISCH_TAC);; val it : goalstack = 1 subgoal (1 total) 0 [`a`] 1 [`b /\ c`]

Re: [Hol-info] Experience and opinions on proof assistants with “rich” type systems

Hi Jeremy, >My dominant recollection is the difficulty of getting the system to do the >right type inference, and getting terms to typecheck. I was forever working >out where I needed to put in type annotations. In Coq and Mizar I don't have this experience, in the sense that I hardly ever need

Re: [Hol-info] Experience and opinions on proof assistants with “rich” type systems

Hi Ramana, >Perhaps it would make more sense to ask people who are using rich type >systems what their motivations are :) >(On this list it's probably mostly people who are satisfied with simple >type theory.) One can do everything with anything. So dependent tpes certainly are not _needed_ for

Re: [Hol-info] Emacs Macros for HOL Light Proof

Hi Rob, >>[...] and Freek Wiedijk's vi mode for HOL Light. >Where do I find the above-mentioned vi mode? The current version has been on the web for a while at but there is no link yet. Everyone should feel free to do with it whatever they like.

Re: [Hol-info] Viewing HOL proofs

Ramana: For HOL Light, I have seen a Vim-integration by Freek Wiedijk which is perhaps even better for interactive proof-viewing, since it also keeps track of where you are up to in the editor buffer, and shows all subgoals of the proof in the viewing terminal. FWIW, this thing I developed

Re: [Hol-info] Undefined operations such as division by zero in HOL

Hi Mike, Taking definedness to the level Freek is discussing would, I think, not let you prove that x DIV 0 = x DIV 0 Exactly. I think that what I want is much closer to PVS and B than to IMPS. I also don't want any change to the logic. I _hate_ partial logics. I want to be able to use all

Re: [Hol-info] Undefined operations such as division by zero in HOL

Hi Rob, Given a Z specification it could generate a set of proof obligations called domain conditions. The idea was that if the domain conditions were true, then the specification was insensitive to the interpretation of undefined terms. This is exactly what I was trying to describe, and the way

Re: [Hol-info] Learning HOL Light

Vincent: Then each time you type something that starts with a semi-colon (e.g., `;blabla`), you obtain the intermediate preterm instead of the term. Hey! miz3 already uses `;...` for proofs. So maybe it's less confusing if you use another symbol to get preterms? Freek

Re: [Hol-info] Fixing HOL Light

Phil: When a theorem is proven and HOL Light announces no subgoals, there is no jingle. or musical fanfare. Please fix. How about? let e tac = let gs = refine(by(VALID tac)) in match gs with | (_,gls,_)::_ - if length gls = 0 then let _ = Unix.system (mpg123 -q

Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light

Hi Bill, Can you jump into the discussion Michael and I were having about whether miz3 is intentionally weakened? Michael seems to think yes, I think no, but I wonder what effect the MESON depth limit of 50 has, or the fact that MESON is just FOL and not HOL. Ah no, there were no deep thoughts

Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light

Hi Bill, Thus, I conclude that the purpose of the default timeout isn't to weaken miz3, but to better instruct beginners Ah no, the main point was that if an inference is _not_ correct, often MESON will run for the full timeout time. So checking proofs with errors (= all proofs when you're not

Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light

Hi Bill, Why are miz3 and Mizar the only proof assistants where one can easily write up human readable proofs? I'm surprised you're not including Isar in this list! And do you know about ForTheL (see http://nevidal.org/download/forthel.pdf)? Now _there's_ a readable formal language! :-) Also,

Re: [Hol-info] HOL and the axiom of choice

Hi Rob, (exists f. forall x. P(x, f(x))) = (forall x. exists y. P(x, y)) So _this_ is the kind of choice that I have no problems with, as it doesn't threaten my Platonism. (It is even provable in type theory! (But only if you use the right flavor of existential quantifier of course :-))) I

Re: [Hol-info] HOL and the axiom of choice

Hi Cris, At a philosophical level I'm surprised that Freek's intervals of Platonism are during the week, with formalism on weekends. It was a reference to a book related to the philosophy of mathematics that I liked a lot when I was much younger. See the quote on

Re: [Hol-info] HOL and the axiom of choice

Hi Cris, To chime in on this: I don't have any problems with a system that doesn't allow you to disable the axiom of choice. In other words: hardwire choice all you like as far as I'm concerned. Without AC you get weirdnesses as that a union of countably many countable sets doesn't need to be

Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light

Hi Michael, miz3's by is just an invocation of MESON but with, as I understand, a time limit imposed. FWIW, one can turn off the time limit by setting timeout to -1. This is useful for example if one wants to recheck a proof that is known to be correct on a slow computer. Of course, if a miz3

Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light

Hi Bill, MESON[] `(!x y z. P x y /\ P y z == P x z) /\ (!x y z. Q x y /\ Q y z == Q x z) /\ (!x y. P x y == P y x) /\ (!x y. P x y \/ Q x y) == (!x y. P x y) \/ (!x y. Q x y)`;; MESON solves this logic puzzle (which I still haven't yet solved) quite quickly, and it writes ...solved at 23107

Re: [Hol-info] Proof assistants for way more people

Hi Ramana, In HOL4 that is called PROVE_HYP. In HOL Light too, thanks for answering my question! (Its arguments have the opposite order from the function I wrote though :-)) In HOL4 you can control how much assumptions are printed with a trace called assumptions, HOL Light just prints them in

Re: [Hol-info] Proof assistants for way more people

Hi Ramana, Later, after a long exploratory theory development, having settled on the right structures, you can go back and fill in the cheats with real proofs, Yes, for example Peter Aczel was arguing for this once too, I think. It's a tempting approach. But my experience is that whenever I

Re: [Hol-info] Proof assistants for way more people

Hi Cris, I was speaking from a software engineering and usability point of view. Okay, just to fix our minds: would you consider Knuth's/ Lamport's latex to be usable in this sense? Because I would strongly claim that it is. It's one of the most usable systems I know. That's why I think that

Re: [Hol-info] Proof assistants for way more people

Hi Mark, It's just that no-one's done it yet! There are just two things that make proof assistants difficult to use: 1. There is not sufficient automation of trivial stuff. I.e., you generally need to break down your reasoning into smaller steps than how you would experience things when

Re: [Hol-info] Proof assistants and high school math

Hi Grant, Are you familiar with Michael Beeson's MathXpert (formerly MathPert)? Yes, MathXpert-level mathematics is exactly what I had in mind when I was talking about high school mathematics. The main difference between what MathXpert provides and what I was asking for, is that MathXpert is

Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light

Hi Bill John, | Better error messages would be great. The way the error messages work is that first the proof is split into steps based on the semicolons and keywords. (I think certain keywords always start a new step and semicolons always end one, with now and proof being the exception because

Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light

Hi Bill, Freek's miz3 code in the miz3 dox 1201.3601-1.pdf solving the drinker's paradox on p 13--14 is perhaps designed to show various features of miz3, but it is more than twice as long as needed: It's mainly intended to be as close as possible to the Jaśkowsky/Fitch-style natural deduction

Re: [Hol-info] Mizar Light and miz3

Hi Felix, However, I discovered the following curious effect: The steps that previously failed without REWRITE_TAC can also be solved using *only* GOAL_TAC. For example, in the proof I posted a while ago, the following step will work. (\n. sum (0..n) (\k. f k * recip f (n - k))) = (\n. (if n

Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light

Hi John, Then every theorem would become |- TarskiModel((===),Between) == P instead of just |- P. Couldn't you set up things in a way that all the theorems would have the form TarskiModel((===),Between) |- P? I think I would find that more attractive. Freek

Re: [Hol-info] Mizar Light and miz3

Hi Felix, From what I understand by REWRITE_TAC[FUN_EQ_THM],2 and by FUN_EQ_THM,2 do very different things: by FUN_EQ_THM,2 runs the HOL_BY tactic, whereas by REWRITE_TAC[FUN_EQ_THM],2 runs REWRITE_TAC, but not HOL_BY. Or does the second option run first REWRITE_TAC and then HOL_BY? No, only

Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light

Hi Bill, I'm pondering the issue of miz3 not allowing free variables in contrast with how you want to work in an axiomatic framework. However, already: !(===) (Between:point#point#point-bool) (cong). TarskiModel((===),(Between:point#point#point-bool),(cong)) let (===) be

Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light

Hi John and Makarius, This is not very much about HOL as such, so if this reply is inappropriate for the HOL list, I apologise: mutating the names of constants. I always found this mutable constants complaint silly. Many people make it, but it never struck me as significant. Surely in every

Re: [Hol-info] Mizar Light and miz3

Hi Felix, 4) I start gvim and load a file with the following content: let ARITHMETIC_SUM = thm '; !n. nsum(1..n) (\i. i) = (n*(n+1)) DIV 2 proof qed by #INDUCT_TAC; ';; The quotes should be backquotes. With this I think miz3 will try to execute this as ocaml source (it does not match the

[Hol-info] Mizar Light and miz3

Dear everyone, John Harrison pointed out to me that the following query was posted on the hol-info mailing list (I'm subscribed to that list but often just delete the messages without looking, sorry about that. So I missed this): 6) I am very curious about Mizar Light and would like to convert

[Hol-info] Call for bids ITP 2012

and the voting phase will take place. The people eligible to vote are those who are seriously thinking of attending ITP 2012. The voting system used will be Single Transferable Vote between all received bids. Marko van Eekelen Herman Geuvers Julien Schmaltz Freek Wiedijk

[Hol-info] Call for Papers ACL2 2011

, USA) Julien Schmaltz (Open Universiteit, The Netherlands) Natarajan Shankar (SRI, USA) Sol Swords (Centaur, USA) Freek Wiedijk (Radboud Univ. Nijmegen, The Netherlands) -- WhatsUp Gold - Download Free Network Management

[Hol-info] ITP 2011 (Call for Workshop Proposals)

Eekelen, Radboud University Nijmegen/Open University of the Netherlands Herman Geuvers, Radboud University Nijmegen Julien Schmaltz, Open University of the Netherlands/Radboud University Nijmegen Freek Wiedijk, Radboud University Nijmegen

[Hol-info] ITP 2011 (Call for Papers)

Conference co-chairs: Marko Van Eekelen, Radboud University Nijmegen/Open University of the Netherlands Herman Geuvers, Radboud University Nijmegen Julien Schmaltz, Open University of the Netherlands/Radboud University Nijmegen Freek Wiedijk, Radboud University Nijmegen Program Committee: David

[Hol-info] 1 Postdoc and 1 PhD vacancy in the MathWiki project

1 POSTDOC and 1 PHD POSITION in the MathWiki project at Radboud University Nijmegen (NL) http://www.fnds.cs.ru.nl/fndswiki/Vacancies The Institute for Computing and Information Science of the Radboud University Nijmegen (NL) is looking for 2 researchers to work on the

[Hol-info] The QED Project

there is anything interesting to say to this question.) Freek Message-ID: 4975cdb4.2010...@univie.ac.at Date: Tue, 20 Jan 2009 14:12:20 +0100 From: Arnold Neumaier arnold.neuma...@univie.ac.at To: Freek Wiedijk fr...@cs.kun.nl Subject

[Hol-info] System Announcement: ProofWeb

on the ProofWeb home page. Cezary Kaliszyk Dan Synek Femke van Raamsdonk Freek Wiedijk Herman Geuvers James McKinna WHAT IS PROOFWEB? ProofWeb is both a system for teaching logic and for using proof assistants through the web. ProofWeb can be used in three ways. First, one can use the guest login

[Hol-info] Second CFP - JAR special issue for PLMMS

. * Notification: January 16th 2009. * Final versions: March 30th 2009. Editors of the special issue * Jacques Carette (McMaster University, Canada) * Makarius Wenzel (Technische Universitaet Muenchen, Germany) * Freek Wiedijk (Radboud University Nijmegen, Netherlands

[Hol-info] Special issue on Programming Languages and Mechanized Mathematics Systems (JAR)

. * Notification: January 16th 2009. * Final versions: March 30th 2009. Editors of the special issue * Jacques Carette (McMaster University, Canada) * Makarius Wenzel (Technische Universitaet Muenchen, Germany) * Freek Wiedijk (Radboud University Nijmegen, Netherlands