[Hol-info] Sample code from John Harrison's "Handbook of Practical Logic and Automated Reasoning"

This is perhaps slightly off-topic, but it relates to using OCaml's utop with some of John Harrison's code. It might have some degree of relevance to William Mitchell's recent request regarding HOL Light code. A few months ago I put together a GitHub repository with some utilities and slightly mo

Re: [Hol-info] Inquiry: Introducing new types as predicates

Hello Mario, Thanks for your various comments, suggestions, and thoughts. Where I have a response, they are below, inline. On Fri, Jan 26, 2018 at 7:45 PM, Mario Xerxes Castelán Castro < marioxcc...@yandex.com> wrote: > On 24/01/18 14:47, Cris Perdue wrote: > > As it turns out,

Re: [Hol-info] Inquiry: Introducing new types as predicates

e opportunity to properly grasp the issues, at least not in this lifetime. Best regards, Cris On Tue, Jan 23, 2018 at 10:16 AM, Mario Castelán Castro < marioxcc...@yandex.com> wrote: > On 22/01/18 18:35, Cris Perdue wrote: > > Are any of you readers of this list aware of investi

Re: [Hol-info] Inquiry: Introducing new types as predicates

as concerned though with types that conceptually do not have overlapping membership. For what it's worth, I understand the flexibility of set theory, but for various reasons would prefer to work in a simple higher-order logic. -Cris > > > Michael > > > > > > *From:

[Hol-info] Inquiry: Introducing new types as predicates

Are any of you readers of this list aware of investigations or implementations of logics that, like the HOL family of provers, are based on the simple theory of types, but which support introduction of new types through new predicates rather than new type constants? Presumably numbers then could be

Re: [Hol-info] Error Loading Theory in HOL Light

On Sun, Oct 16, 2016 at 12:44 PM, wrote: > Hi Adnan, > > | I have another query. Can anybody know the way to reduce the loading time > | of HOL-Light theories? > > If you are using some version of Linux there are checkpointing options, > as explained in the README file. Personally I tend to just

Re: [Hol-info] Learning HOL Light

On Tue, Apr 29, 2014 at 5:51 AM, Bill Richter wrote: > > Here's a more substantive point that's always bothered me. Suppose if one > is working in one's preferred logical framework (e.g. ZFC), and one engages > in metamathematics. On what grounds to we believe the metamathematics? > The poin

[Hol-info] How "LC" implies FOL

On Fri, Mar 21, 2014 at 9:08 AM, Bill Richter wrote: > Thanks, Konrad! I'll read your proof of NOT_FORALL_THM, and try to find > Gordon and Melham's book. Two points: > > I don't believe that Church ever explained how typed LC implies FOL. > Church certainly does not explain this in his paper

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

On Wed, Apr 10, 2013 at 3:04 AM, Freek Wiedijk wrote: > 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

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

On Tue, Apr 9, 2013 at 2:22 AM, Freek Wiedijk wrote: > Hi Chris, > > Thanks for bringing up this topic, which is very > interesting question to me. It's question III in my talk > . I'm replying > here because there is an approach that I've been wanting

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

encs.concordia.ca/~vincent > > > Am 2013-04-04 um 18:11 schrieb Cris Perdue : > > Dear HOL experts, > > I am hoping for wisdom and recommendations from you all related to a > question I have. Let me start with a bit of background information, which > is here largel

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

lt; n ==> > !k. (k = k DIV n * n + k MOD n) /\ k MOD n < n > > Check the development in src/num/theories/arithmeticScript.sml > for details. > > Konrad. > > > > > On Thu, Apr 4, 2013 at 5:11 PM, Cris Perdue wrote: > >> Dear HOL experts, >

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

Dear HOL experts, I am hoping for wisdom and recommendations from you all related to a question I have. Let me start with a bit of background information, which is here largely to orient you to my understanding of the situation. I know the facts are elementary. Usually in mathematics some operat

Re: [Hol-info] MP_TAC

On Tue, Oct 30, 2012 at 6:44 PM, Konrad Slind wrote: > > Ok, so if I understand this correctly the validity checks are only in > > place to keep you from going down an inference chain that is guarenteed > > to go no where in making progress towards proving your goal. This being > > only an issue

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

Bill or Michael in particular, one question: On Thu, Aug 30, 2012 at 7:39 PM, Bill Richter wrote: > Thanks for the HOL lesson, Michael, and clarifying about theorem-proving! > Can you give me some advice on how to read your 45 page Logic manual? I > need to understand why > >x : point [mea

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

Bill, Michael, and all, Let me second Michael's comments right from the start. He has expressed most gracefully much of what I thought needed to be said. On Tue, Aug 28, 2012 at 11:11 PM, Bill Richter < rich...@math.northwestern.edu> wrote: > Thanks, Michael! I like what you wrote about (me and

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

On Fri, Aug 24, 2012 at 1:28 PM, John Harrison wrote: > > Hi Bill, > > | Thanks, John! I'm up to Euclid's Prop I.28, so I have formalized > | Hartshorne's result > | http://www.math.northwestern.edu/~richter/RichterHOL-LightMiz3HilbertA > | xiomGeometry.tar.gz Thm 10.4: All of Euclid's propositio

[Hol-info] Presenting HOL Light tactic proofs in forward style

Using the function-wrapping concepts in Mark's Tactician and some of that code, I am now able to execute HOL Light tactic proofs and present them as rather traditional-style forward proofs. (Mark in turn credits Roland Zumkeller in the Tactician code.) At the bottom of this email are two of Mark's

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

Michael's comments below have been quite interesting to me as part of understanding set comprehensions better, so thanks Michael! I have comments and questions below: On Thu, Aug 16, 2012 at 11:40 PM, Michael Norrish < michael.norr...@nicta.com.au> wrote: > On 17/08/12 07:51, Bill Richter wrote:

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

On Mon, Aug 13, 2012 at 6:05 PM, Bill Richter wrote: > Michael, Konrad, Rob, Mark, Cris, thank you very much for all the > messages! This partly answers many questions that have puzzled me. Among > other things, I'm well on way to having to give you guys acknowledgments in > my paper. I think

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

Bill, On Sun, Aug 12, 2012 at 9:53 PM, Bill Richter wrote: > Thanks, Mark! I looked at Tom Hales's Notices article, as you suggested > www.ams.org/notices/200811/tx081101370p.pdf > Now Tom is a great mathematician (he's the main reason I'm here), but Tom > is now an HOL Light expert, and I thin

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

Freek, Mark, Bill, Thanks very much for the stimulating and I think helpful responses, including Mark's historical sketch. I'm glad to learn that inclusion of an axiom of choice is considered unsurprising, perhaps leading to less weird consequences than if it is left out. Freek's example of the un

[Hol-info] HOL and the axiom of choice

In a post earlier today Rob Arthan commented that "in HOL you are working in a model of Zermelo set theory with choice", which certainly seems to be true of HOL Light. I'm a bit surprised that HOL Light (and HOL Zero, and Proof Power, etc.) has this as a rather fundamental part. John Harrison goes

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

Hi Bill, On Fri, Jul 20, 2012 at 12:00 PM, Bill Richter < rich...@math.northwestern.edu> wrote: > Thanks, Cris, I did not know about John's paper > http://www.cl.cam.ac.uk/~jrh13/papers/me.html. It looks very > interesting, but his interesting details aren't what what I want to talk > about.

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

On Fri, Jul 20, 2012 at 12:21 AM, Bill Richter < rich...@math.northwestern.edu> wrote: >Sorry to disagree, but this seems wrong to me. This is only true >if you don't put tactics in the justifications. I especially allow >_arbitrary_ HOL Light tactics there for exactly this reason: s

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

The assumption seems to do the job provided that it has no free variables. Then once proven it can be removed by modus ponens or other cut-like rule. I'm not seeing a problem with type variables, though it's true they must match in both parts of tm |- tm or |- tm --> tm. -Cris On Thu, Jul 19, 20

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

Hi Konrad, On Thu, Jul 19, 2012 at 7:35 AM, Konrad Slind wrote: > > HOL Light just prints them in full, I think. Ah well, > > as I already wrote, this way of working does not appeal > > too much to me anyway :-) > > > > Freek > > It also suffers from the problem that a polymorphic formula > assu

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

Hi Freek, On Fri, Jul 13, 2012 at 5:32 AM, Freek Wiedijk wrote: > 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 clai

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

On Thu, Jul 12, 2012 at 3:37 AM, Freek Wiedijk wrote: > Hi Mark, > > >It's just that no-one's done it yet! > This from Mark was a reply to my comment that making a proof assistant really easy to use will be "a huge challenge". I was speaking from a software engineering and usability point of vie

[Hol-info] Common HOL Platform, definition?

Hello Mark and All, I noticed Mark's publication "Introducing HOL Zero", and the abstract mentions a Common HOL Platform. Can anyone point me to a definition of this? Thanks, Cris -- Live Security Virtual Conference Exclu

[Hol-info] Proposed solution to problems building HOL Light

Various users have reported the same problem over the last year or so, see http://code.google.com/p/hol-light/issues/detail?id=2. I have encountered the same problem using Camlp5 version 6.06 as Colin Rowat also did recently. There seems to be a trend here, that all new versions of camlp5 work wi

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

nt to assisting with proofs of theorems. > > Actually, a very interesting exercise was Freek's challenge at ICMS 2006, > where he asked expert users of various theorem provers, including HOL > Light, > Mizar, Coq and Isabelle/HOL Isar, to formalise a classic textbook proof. >

[Hol-info] Proof assistants for way more people

Mark and all, Yay! That's a beautiful description of key characteristics of tools that I believe will have great benefit and impact when they arrive on the scene. Reading through it a couple more times, I'm not sure there is any point where I do not heartily agree. This is something I want to cont

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

Cris > > You can find links to papers about it on Beeson's homepage (publication > #'s 28-31): http://www.michaelbeeson.com/research/papers/pubs.html > The MathXpert website is here: http://helpwithmath.com/ , and there is > some background on the ideas underlying it h

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

On Fri, May 25, 2012 at 3:23 AM, Freek Wiedijk wrote: > 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 wha

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

or one step of the problem. Repeat as needed. Should work in modern Firefox, Chrome, or Safari browsers. This way the system can see and analyze the student's work step by step in "real time", and the tool may help guide the student as well. Of course I'm not trying to limit u

[Hol-info] Proof assistants and high school math

Reading Freek Wiedijk's paper "Formal Proofs: Getting Started" has been very interesting for me, but raised a question that seems important to some of my goals, and it seems to me that he and other members of this group are probably a great resour

Re: [Hol-info] Announcement: Prooftoys visual proof assistant for higher-order logic

: > > You might want to consider implementing import/export of OpenTheory > proofs > > (http://www.gilith.com/research/opentheory/) to get access to some > larger > > existing proofs. It would be interesting to see how they would look in > the > > web interface. >

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

I'm not a HOL Light expert (nor a mathematician in fact), but here are a couple of thoughts: About axioms: You can assert new axioms using new_axiom ( http://www.cl.cam.ac.uk/~jrh13/hol-light/HTML/new_axiom.html). The page discusses the alternatives too. Your comments on teaching rigorous axiomat

[Hol-info] Announcement: Prooftoys visual proof assistant for higher-order logic

primitive derived rules of inference so it is possible to experiment with real numbers. More information is available on the Prooftoys <http://prooftoys.org/> web site. Best regards, Cris Perdue -- For Developers, A L

Re: [Hol-info] Problem building HOL Light

both Johns for your communications on this. -Cris On Mon, Jan 2, 2012 at 6:25 PM, Cris Perdue wrote: > I am looking for suggestions on successfully running "make" to install the > current version of HOL Light. > > On an Ubuntu 11.10 system, with: > > $ ocaml -version &

Re: [Hol-info] Problem building HOL Light

ll down towards the bottom for a link to previous versions. > > Mark. > > > on 3/1/12 7:33 AM, Cris Perdue wrote: > > > I am looking for suggestions on successfully running "make" to install > the > > current version of HOL Light. > > > > On an

[Hol-info] Problem building HOL Light

I am looking for suggestions on successfully running "make" to install the current version of HOL Light. On an Ubuntu 11.10 system, with: $ ocaml -version The Objective Caml toplevel, version 3.12.0 $ camlp5 -v Camlp5 version 6.02.2 (ocaml 3.12.0) # Running "make" I get: $ make if test `ocamlc