[Hol-info] Fwd: Job Opportunity at D-RisQ

If the below is of interest please contact Colin (rather than me or the list :-)) Regards, Rob. > Begin forwarded message: > > From: "Colin O'Halloran" mailto:c...@drisq.com>> > Subject: Job Opportunity at D-RisQ > Date: 15 November 2018 at 15:28:23 GMT > To: mailto:c...@drisq.com>> > > I am

Re: [Hol-info] [isabelle] Axiom of Choice – Re: Hilbert's epsilon operator in Church's Type Theory and Gordon's HOL logic

> On 12 Mar 2018, at 19:12, Ken Kubota wrote: > > Thanks, this is what I expected. > > Concerning the Axiom of Choice (answering Mario's email, too), its use should > be expressed as a conditional of the form AC => THM (or as a hypothesis) and > not as an axiom in order to make the appeal to

Re: [Hol-info] Similar trouble building HOL Light's pa_j.ml

: > > File "pa_j.ml", line 1918, characters 35-43: > While expanding quotation "str_item": > Parse error: antiquot "_" or antiquot "" or [ident] expected after 'type' (in > [str_item]) > > I found a similar issue on Github at &g

Re: [Hol-info] conservativity of HOL constant and type definitions

Ondrej, > On 24 Oct 2016, at 20:32, Ondřej Kunčar wrote: > > On 10/24/2016 09:16 PM, Rob Arthan wrote: >> I am pretty sure nothing has been published and, if you are right about >> (2.2), >> then I don't think type definitions can be proof-theoretically con

Re: [Hol-info] conservativity of HOL constant and type definitions

Andrei, > On 24 Oct 2016, at 19:16, Andrei Popescu wrote: > > Since the conservativity topic has been touched upon, I would like to > summarize the situation in HOL as I understand it now, after our discussion. > > (Myself, I am mainly interested in Isabelle/HOL, but this is an important >

Re: [Hol-info] [isabelle] definability of new types (HOL), overloaded constant definitions for axiomatic type classes (Isabelle) - Re: Who is ProofPower "by" (and STT)?

Andrei, > On 23 Oct 2016, at 14:31, Andrei Popescu wrote: > > Hi Rob, > > >> It’s the other way round. Soundness implies that proof-theoretic > >> conservativity implies model-theoretic conservativity. > > Ondra's statement was the correct one. > > Let's spell this out, to make sure we are

Re: [Hol-info] [isabelle] definability of new types (HOL), overloaded constant definitions for axiomatic type classes (Isabelle) - Re: Who is ProofPower "by" (and STT)?

Ondrej, > On 22 Oct 2016, at 20:07, Ondřej Kunčar wrote: > > Hi Rob, > you are right that we mention only the plain definitions in HOL and not > the implicit ones, when we compare the definitional mechanism of HOL and > Isabelle/HOL. (If this what you meant; I assume you didn't mean to say >

Re: [Hol-info] [isabelle] definability of new types (HOL), overloaded constant definitions for axiomatic type classes (Isabelle) - Re: Who is ProofPower "by" (and STT)?

Ken, Unfortunately, the paper by Ondrej Kuncar and Andrei Popescu that you cite gives a description of the definitional mechanisms in HOL that is about 25 years out of date. The new_specification mechanism allows implicit definitions and cannot be viewed as a syntactic abbreviation mechanism. The

Re: [Hol-info] Foundations of Mathematics: Type Theory after Church's Simple Theory of Types (1940)

readable well-documented specifications as well as proof; support for other formal languages via semantic embedding (eventually picked up as a hot topic in all the other descendants of Mike Gordon’s HOL). The main architect was Roger Bishop Jones. References: @article{proofpower, author={Rob

Re: [Hol-info] Difficulty with higher order matching

> On 9 Jun 2016, at 00:15, Ramana Kumar wrote: > > Hi Peter, > > I'm not sure I can explain why HO_MATCH_MP_TAC is not powerful enough for > this kind of match [snip] > 1. Incomplete goalstack: > Initial goal: > > BIT (LEAST n. BIT n x) x > > > : >proofs > > whileTheory.LEAS

[Hol-info] Google is not always your friend

I was trying to find a reference for the introduction of conversions in LCF. The link below is interesting, but not what I was looking for :-). http://www.lcfconversions.com Regards, Rob.

Re: [Hol-info] What is the advantage of HOL4?

I'd add to Ramana's list that HOL4 adds a very simple but powerful form of polymorphism to the system discussed in Bill Farmer's "The seven virtues of simple type theory". Both PVS and Coq support dependent types which adds some extra expressiveness compared with the polymorphism in HOL4 at th

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

> On 4 Nov 2015, at 05:22, Joe Leslie-Hurd wrote: > > and Freek > Wiedijk's vi mode for HOL Light. Where do I find the above-mentioned vi mode? Regards, Rob. -- ___ hol-in

Re: [Hol-info] Different topologies on a given set in HOL

> On 31 May 2015, at 14:04, Esseger wrote: > > Dear all, > > I recently became interested in HOL, especially with Isar which I find > quite fascinating and powerful for "classical" mathematicians. During my > experimentations, there is one construction that I failed completely to > formalize

Re: [Hol-info] sanity checks on exported theorems

Ramana, You are far too young to be having senior moments and (if memory serves) you don’t drink, but you might have been thinking about this thread on the ProofPower mailing list: http://lemma-one.com/pipermail/proofpower_lemma-one.com/2012-March/000780.html Regards, Rob On 9 Apr 2015, at 16:

[Hol-info] Controlling instantiation in rewriting

I am working on a paper about a proof procedure and realised that I was about to write something rather specific to ProofPower. In ProofPower, the rewriting conversions and tactics treat free variables on the left-hand side of the equations you are rewriting with as constants and will only instanti

Re: [Hol-info] formalizing an axiom schema and MacOS OCaml/Camlp binaries

On 15 Nov 2014, at 08:25, Bill Richter wrote: > Does anyone know how to formalize an axiom schema in HOL Light? I'm > interested in formalizing the Tarski axiomatic geometry > Axiom schema of Continuity > http://en.wikipedia.org/wiki/Tarski%27s_axioms#The_axioms > and the part I don't know ho

Re: [Hol-info] Theorems Produced by Type Definitions

Ramana, On 16 Oct 2014, at 17:18, Ramana Kumar wrote: > Hi all, > > There has been an interesting discussion on the OpenTheory mailing list > recently regarding how to simplify the two theorems produced by a type > definition in HOL Light and remove their free variables. The latest message

Re: [Hol-info] Learning HOL Light

On 28 Apr 2014, at 00:57, Bill Richter wrote: > Rob, I want to argue that Peter Andrews's book To Truth Through Proof > supports my idea of informal mathematics documentation for HOL Light. I > don't understand yet how the informal math compares to your HOL documentation > http://www.lemma-

Re: [Hol-info] Learning HOL Light

On 26 Mar 2014, at 07:58, Bill Richter wrote: > Thanks, Konrad! The proof of SYM in the HOL4 manual Description (p 46) is > fine because the HOL4 SUBST is much more powerful than the HOL Light INST. > On p 26, SUBST is described by > > SUBST : (thm * term)list -> term -> thm -> thm > > t

Re: [Hol-info] Learning HOL Light

Bill, On 26 Mar 2014, at 23:01, Bill Richter wrote: > Thanks, Rob! Then since I only technically have a model, I would say I'm > working in your class (c): > > (c) Informal mathematical proofs that an assertion is provable in > some agreed deductive system. No. When I wrote "an assertion",

Re: [Hol-info] Learning HOL Light

Bill, On 26 Mar 2014, at 09:37, Bill Richter wrote: > Rob, thanks for the excellent post! Let me more clearly tell you what I > think I'm doing, using your terminology, and maybe we can discuss your > classes a--e. > > Take HOL Light and possibly some extra types, constants and axioms create

Re: [Hol-info] Learning HOL Light

Bill, On 25 Mar 2014, at 07:27, Bill Richter wrote: > So the similarity is that in both FOL and HOL, > 1) You can define a set of statements to study (wffs and proto-sequents). "Proto-sequent" and “sequent” are usually referred to as “sequent” and “theorem” respectively. E.g., see the HOL4 Lo

Re: [Hol-info] Learning HOL Light

Bill, On 24 Mar 2014, at 06:28, Bill Richter wrote: > Thanks, Rob! You're right, I hadn't looked at Section 1.4 "A Formulation > Based on Equality" of Andrew's link >> http://plato.stanford.edu/entries/type-theory-church/ and more to the point, >> I didn't read the longer version Andrew's wro

Re: [Hol-info] Learning HOL Light

Bill, On 23 Mar 2014, at 18:44, Bill Richter wrote: > > The claim (which you may not be making) that Hankin derived FOL from the > basic LC axioms (e.g. the HOL axioms) seems to contradict Andrew's link > http://plato.stanford.edu/entries/type-theory-church/ > which as I posted lists Prop Log

Re: [Hol-info] Learning HOL Light

Andrew, On 21 Mar 2014, at 09:13, Andrew Butterfield wrote: > > On 20 Mar 2014, at 16:50, Rob Arthan wrote: > >> >> ProofPower is no different from HOL4 and HOL Light as regards substitution. >> The ProofPower documentation does include a formal specificati

Re: [Hol-info] Learning HOL Light

Bill, On 19 Mar 2014, at 07:02, Bill Richter wrote: > work is. If I understood it, I'm sure I'd say it was elegant mathematics, > and that it's good we're assuming the weakest possible set of axioms. Have you looked at Peter Andrews’ book "An Introduction to Mathematical Logic and Type The

Re: [Hol-info] Learning HOL Light

On 17 Mar 2014, at 00:52, Konrad Slind wrote: > RE: type bool. I think BOOL_CASES_AX can be derived from choice. > There's a topos-flavoured proof (due to Diaconescu?) in Lambek and Scott, > which I think John ported to HOL-Light. Yes. I don’t know the right reference: the comment in the HOL Li

Re: [Hol-info] More on set comprehensions

; quotations pick up the types of existing free variables in the subgoal > package proof)? Yes. That's why I mentioned a context when I said "the same string of symbols should always parse to the same term in any given context". Regards, Rob. > > Mark. > > o

Re: [Hol-info] More on set comprehensions

Bill, > On 4 Jan 2014, at 05:17, Bill Richter wrote: ... On 7 Jan 2014, at 16:22, Rob Arthan wrote: > I think we will just have to agree differ about this. Let me just make two > comments: > Something very odd happened with my e-mail client which caused it to discard the two co

Re: [Hol-info] More on set comprehensions

Bill, On 4 Jan 2014, at 05:17, Bill Richter wrote: > So the expandsion order doesn't matter The real issue is that r is now free > in (f x, R x), unlike the first example. Yes. My explanation of the phenomena you were observing was wrong. > > Why do you need to calculate it? > > We don't ne

Re: [Hol-info] More on set comprehensions

Bill, On 1 Jan 2014, at 03:04, Bill Richter wrote: > Rob, I learned a lot from your post! My conclusion is that in both HOL Light > and HOL4, > {f x | R x} = λa. ∃x. R x ∧ a = f x > for some variable a than is not free in R x or f x. I judge both HOL > approaches to have pluses & minuses, an

Re: [Hol-info] More on set comprehensions

and babs is p. So HOL Light has a special case when t has just 1 free variable: # frees `{x + y + 1 | z > 0}`;; val it : term list = [`z`; `x`; `y`] # frees `{x + 1 | z > 0}`;; val it : term list = [`z`] I wonder why? HOL4 rejects both of the above. Regards, Rob. > > Konrad.

[Hol-info] More on set comprehensions

Here are a few observations about the set comprehension syntax in HOL Light and HOL4. The HOL4 Description manual says that {t | p} parses to: GSPEC(\(x1,. . .,xn).(t,p)) where x1, . . . , xn are those free variables that occur in both t and p. It also says that it is an error if there are no such

Re: [Hol-info] HOL Light set comprehensions

Bill, On 27 Dec 2013, at 18:47, Bill Richter wrote: > ... > Now this last part surprised me. I didn't know that numerals are > combinations, and I would have guessed they were constants. So let me > practice my is_*/dest_* skills: > > dest_comb `1`;; > > val it : term * term = (`NUMERAL`,

Re: [Hol-info] HOL Light set comprehensions

On 18 Dec 2013, at 04:21, Michael Norrish wrote: > On 18/12/13 14:56, Bill Richter wrote: >> I tried something like this when you first posted, but I didn't think to use >> dest_comb. Do you have any general tips on how to recognize a term as say a >> combination (which worked here) on an abstra

Re: [Hol-info] HOL Light set comprehensions

On 13 Dec 2013, at 03:51, Bill Richter wrote: > Thanks, Rob! Can you explain how HOL4 performs the quantification with > GSPEC? I would think that GSPEC would have to choose a fresh variable, and > I've never understood how that's to be done, because you have know that your > new fresh varia

Re: [Hol-info] HOL Light set comprehensions

On 7 Dec 2013, at 07:19, Bill Richter wrote: > Rob, I think the answer to your interesting question involves more > complicated set abstractions like {y + 6 | y < 0}. I think here we see the > merit of the HOL Light invisible variables, as this simple proof shows: > > … > I think that's co

[Hol-info] alpha-equivalent assumptions

Ramana assures me that HOL4 manages the assumptions of a theorem as a set modulo alpha-convertibility. I had been suspicious because of the following statement in the Reference Manual description of DISCH_ALL: "Two or more alpha-convertible hypotheses will be discharged by a single impl

[Hol-info] HOL Light set comprehensions

This is idle curiosity on my part about HOL Light: why are the constants that support set comprehensions defined in such a way that the parser has to generate an invisible bound variable? This results in surprising behaviour like: # `{x | x > 9}` = `{x | x > 9}`;; val it : bool = false HOL4 def

Re: [Hol-info] Trouble building HOL light

Mark, Thanks for the info and the pointers to your excellent HOL Zero documentation. On 15 Oct 2013, at 14:03, Mark Adams wrote: > … > I think the warnings you get may be from superfluous #load directives in > your adapted 'pa_j.ml' file, so comment out the following two lines in the > adapted

Re: [Hol-info] Trouble building HOL light

Ramana, On 14 Oct 2013, at 14:41, Ramana Kumar wrote: > From what I remember, camlp5 and ocaml versioning is a nightmare... (though > it may be that HOL Light is a particularly strenuous application for it). > One might find Alex Krauss's approach useful: > http://sourceforge.net/mailarchive/m

Re: [Hol-info] Trouble building HOL light

On 14 Oct 2013, at 12:53, Rob Arthan wrote: > Can anyone help me with building HOL light? I get the following when I run > make: > > File "pa_j.ml", line 1918, characters 35-43: > While expanding quotation "str_item": > Parse error: antiquot "_"

[Hol-info] Trouble building HOL light

Can anyone help me with building HOL light? I get the following when I run make: File "pa_j.ml", line 1918, characters 35-43: While expanding quotation "str_item": Parse error: antiquot "_" or antiquot "" or [ident] expected after 'type' (in [str_item]) Error while running external preprocessor

[Hol-info] Documentation for new_type_definition (and a little bug)

I think the section on new_type_definition in the HOL 4 reference manual should say that it fails if the theorem in the parameter has free variables. E.g., app load ["PairedLambda", "Q"]; open PairedLambda pairTheory; val tyax1 = new_type_definition ("bad1", Q.prove(`?p.(\(x,y). ~(x /\ y /\ z))

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

On 10 Apr 2013, at 11:04, Freek Wiedijk wrote: >> > What I just want is to have some story + infrastructure > that allows me to -- at the very very end -- prove that > the result that I have established is "meaningful", in the > sense that it doesn't depend on/refer to what functions do > outside

Re: [Hol-info] Documentation about the Simplifier internals

On 17 Mar 2013, at 00:38, Michael Norrish wrote: > The HOL4 Description manual has a section on the simplifier. And yes, it > should preserve the probability of goals because at the top level, it is only > capable of replacing equals with equals. > I am not convinced. I often set up a goal

Re: [Hol-info] Learning HOL Light

Bill, On Jan 16, 2013, at 1:31 PM, Bill Richter wrote: > > … > And as Rob says that eventually we should modify HOL to allow type > quantification You make me sound more definite about this than I actually feel. In fact it has already been done (for HOL4) in the shape of Peter Homeier's HOL-

Re: [Hol-info] Learning HOL Light

Bill, On Jan 6, 2013, at 6:18 AM, Bill Richter wrote: > Thanks, Ramana! I'll try to find Larry's book ($66.30 on Amazon). One caution: Larry's (excellent) book is about Standard ML, which is the metalanguage used in HOL IV and ProofPower. HOL Light is implemented in OCaml. With a few notabl

Re: [Hol-info] data-respecting relation

On 5 Sep 2012, at 15:50, Ramana Kumar wrote: > What is the usual name for this kind of relation? > > Given an inductive data type like > foo = C1 of bool | C2 of foo list > So foo is a type of trees with arbitrary finite branching and with Boolean labels on the leaves. > I want to classify r

Re: [Hol-info] Can I define a ZF FOL constant using only FOL symbols?

On 7 Sep 2012, at 16:13, Gottfried Barrow wrote: > On 9/7/2012 4:41 AM, Josef Urban wrote: >> Hi, >> >> just a quick comment before this becomes into some HOL vs FOL issue: >> (conservative) extension by definitions >> (http://en.wikipedia.org/wiki/Extension_by_definitions) is a standard >> FOL

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

On 14 Aug 2012, at 00:30, Cris Perdue wrote: > > > On Mon, Aug 13, 2012 at 6:05 PM, Bill Richter > wrote: > >I prefer not to say that a type is a set, because the set of all >things having a type is expressible as \x. T (or {x | T}. > > Cris, I'm tempted to go with Michael, who

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

On 13 Aug 2012, at 00:53, Bill Richter wrote: > > What is a type? > If you have time to look at a textbook reference as background to all this, here is a good one describing a system that is very similar in spirit to HOL. @BOOK{andrews, author = "Peter B. Andrews",

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

Michael, On 9 Aug 2012, at 11:06, Michael Norrish wrote: > > I can do all the rest of your proof, and will have that assumption > everywhere. I will then eliminate it at the very end with the theorem > > ?cf. !P x. P x ==> P (cf P) > > and existential elimination. But where does that theor

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

On 8 Aug 2012, at 12:55, Michael Norrish wrote: > On 8/08/12 9:17 PM, Freek Wiedijk wrote: > >> I've had this discussion with John Harrison as well. He then >> pointed out a book about the "epsilon calculus" in which >> it is proved that any statement that you can prove using >> the epsilon ope

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

On 5 Aug 2012, at 22:32, Cris Perdue wrote: > In the end I'm quite curious to know: is there some philosophical or > engineering reason not to introduce the law of the excluded middle separately > from an axiom of choice in HOL logics? There are good practical reasons for having AC wired in. I

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

On 5 Aug 2012, at 08:18, Bill Richter wrote: > Thanks, Ramana! I've often wanted Isabelle locales. Are you going to code > them in HOL4? Locales are one of the many things that (I believe) make the Isabelle HOL logic much more bloated than the original and best HOL logic as supported by HOL4

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

On 3 Aug 2012, at 05:49, Michael Norrish wrote: > On 03/08/12 07:48, Bill Richter wrote: >> Back to my earlier question, my miz3 code begins new_type("point",0);; >> new_type_abbrev("point_set",`:point->bool`);; >> new_constant("Line",`:point_set->bool`);; I still don't know what the HOL, or >> H

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

Bill, On 30 Jul 2012, at 09:31, Bill Richter wrote: > https://dl.dropbox.com/u/34693999/nonobv.pdf > > Rob, thanks for the acknowledgment and modifying your proof 2 of Los's Logic > result. Sorry for posting my code yesterday with my Isabelle-type fonts > still in. I'm including the versio

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

Bill, On 29 Jul 2012, at 07:28, Bill Richter wrote: > https://dl.dropbox.com/u/34693999/nonobv.pdf > > Rob, I like your 2nd proof (although I think your 4 cases are about P and not > P, instead of P and Q), My argument does work exactly as stated, but I agree that it is simpler to avoid hav

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

On 22 Jul 2012, at 10:39, Bill Richter wrote: > https://dl.dropbox.com/u/34693999/nonobv.pdf > > Congratulations, Rob, Thank you! > I had no idea how to prove Los's non-obvious theorem until I read your > solution. I'm not quite satisfied with your exposition, though, and here's > a miz3

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

On 21 Jul 2012, at 05:49, Bill Richter wrote: > Chris, your MESON example was illuminating, and I hope someone can tell me > what it means. Paste this code from p 36 of John's tutorial into the HOL > Light window: > > MESON[] > `(!x y z. P x y /\ P y z ==> P x z) /\ > (!x y z. Q x y /\ Q y z

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

On 26 Jun 2012, at 09:39, Ramana Kumar wrote: > I think you shouldn't use new_constant and new_definition. Just the latter > should be enough to create the new constant with its definition. The former > creates a constant without a definition > Correct. > (it's like new_axiom in that it shoul

Re: [Hol-info] VSTTE

Tom Ridge and I formed two teams of one each using HOL4 and ProofPower-HOL (respectively) in the first VSTTE competition which was a slightly smaller scale affair at the previous VSTTE (it was a rather open-ended 2 hours during the conference rather than 48 hours strictly timed several weeks bef

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

On 29 May 2012, at 06:06, Bill Richter wrote: > Your code > doesn't work for me yet, but maybe that's a problem with my definition > of the function line, which is a bad variable name, so I changed it: > > let Line_DEF = new_definition > `!A B. Line(A, B) = if (A = B) then {} else (@l. A IN l

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

On 28 May 2012, at 05:01, Bill Richter wrote: > Rob, thank you very much for answering my questions! That was smart > of you to notice this problem, which I have worried about: > > your axioms seem to be loose about whether `(A, B) same_side l` > holds if A or B is on the line l. > > I lik

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

On 27 May 2012, at 11:47, Rob Arthan wrote: > >> .. or generalise the above definitions to the notion of an equivalence >> relation on a subset: > > let refl_on_def = new_definition > `ReflOn R P = !x:'a. P x ==> R x x`;; > let symm_on_def = new_defini

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

On 27 May 2012, at 08:20, Bill Richter wrote: > John, I'm over 400 lines now formalizing my Hilbert axiom paper > http://www.math.northwestern.edu/~richter/hilbert.pdf (code below) and > proved that being on the same side of a line defines an equivalence > relation. This is really a lot of fun,

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

On 7 May 2012, at 00:22, Bill Richter wrote: > John, that's definitely an example of poor hol_light readability, and > I vastly prefer my pseudo-TeX: > > (x1^2 + x2^2 + x3^2 + x4^2) (y1^2 + y2^2 + y3^2 + y4^2) > = > (x1 y1 - x2 y2 - x3 y3 - x4 y4)^2 + > (x1 y2 + x2 y1 + x3 y4 - x4 y3)^2 + > (

Re: [Hol-info] HOL Constant Definition Done Right

On 28 Apr 2012, at 16:17, Roger Bishop Jones wrote: > On Saturday 28 Apr 2012 13:14, Rob Arthan wrote: > >> On 28 Apr 2012, at 09:53, Roger Bishop Jones wrote: >>> Is the revised new_specification "complete"? >>> i.e. are there any conservative exten

Re: [Hol-info] HOL Constant Definition Done Right

Roger, On 28 Apr 2012, at 09:53, Roger Bishop Jones wrote: > Is the revised new_specification "complete"? > i.e. are there any conservative extensions which cannot be > achieved by it? > (an argument for this would strengthen the case) I would be rather surprised if there were any nice c

Re: [Hol-info] HOL Constant Definition Done Right

On 25 Apr 2012, at 14:03, Ramana Kumar wrote: > Looks like interesting conversations. Congratulations on doing such a great > job of writing them up! I would be more than happy to fix the relevant > OpenTheory importer/exporters if OpenTheory and/or HOL4 and/or HOL Light > adopt this proposal.

[Hol-info] HOL Constant Definition Done Right

Conversations with Mark Adams and John Harrison at the Milner Symposium earlier last week inspired me to think through a new approach to defining constants in HOL. This generalises what was done in early versions of HOL Light. It constitutes an adjustment to new_specification that supersedes new

Re: [Hol-info] Zermelo Proof Checker

On 25 Jan 2012, at 20:21, Jeremy Bem wrote: > I would like to announce a new proof assistant called the Zermelo Proof > Checker. It features a type system similar to the one of HOL, but is based on > standard foundations. It is available online at http://zermelo.org/. That's very interesting. Y

Re: [Hol-info] hol-light , is this a bug of BETA_CONV

On 13 May 2011, at 08:11, hao deng wrote: > Hi, there: >I'm a new user of hol-light and I find the following thing strange : > > # BETA_CONV `(\x. ?y. x = a /\ y = b) y`;; > Warning: inventing type variables > val it : thm = |- (\x. ?y. x = a /\ y = b) y <=> (?y. y = a /\ y = b) > > the ?y

[Hol-info] Miller/Nipklow modulo pairing and projection

Can anyone give me any pointers to extensions of the Miller/Nipkow algorithms for higher-order unification and matching for linear patterns to work modulo pairing and projection? I.e., if I am doing matching, I want `p(x, y)` to be a valid pattern and I want `\z.(FST z, SND z)` to be an instance

[Hol-info] Test cases for higher-order matching with linear patterns

Can anyone point me at a source of test cases for higher-order matching with linear patterns, please. Regards, Rob. -- Beautiful is writing same markup. Internet Explorer 9 supports standards for HTML5, CSS3, SVG 1.1,

Re: [Hol-info] well-ordering theorem

On 21 Jan 2010, at 18:07, Roger Bishop Jones wrote: > On Wednesday 20 January 2010 16:02:10 Roger Bishop Jones wrote: > >> On Tuesday 19 January 2010 18:07:32 Lockwood Morris wrote: >>> The only relevant information I have come across is Stewart Shapiro's >>> statement, in Foundations without Fo

[Hol-info] A little bit of formal methods history

-interference security properties that I believe still has many features of interest. Regards, Rob Arthan. -- Return on Information: Google Enterprise Search pays you back Get the facts. http://p.sf.net/sfu/google-dev2dev

Re: [Hol-info] How were type variables added to higher order logic?

On Thursday 25 Sep 2008 10:28 pm, Peter Vincent Homeier wrote: > Since I began using HOL88 many years ago, I have always heard that the > logic of HOL was "higher order logic," > ... However, when reading both of these, I see that in neither case does the > type system proposed contain type variab

Re: [Hol-info] How were type variables added to higher order logic?

[Rseend: I got no response first time round] On Thursday 25 Sep 2008 10:28 pm, Peter Vincent Homeier wrote: > Since I began using HOL88 many years ago, I have always heard that the > logic of HOL was "higher order logic," > ... However, when reading both of these, I see that in neither case does