John, I'm now certain that your proof of TRIANGLE_ANGLE_SUM_LEMMA is pretty
much what I posted yesterday. I was confused about LAW_OF_COSINES, a vector
triviality which I actually used. Here's a better proof that my son I worked
out today. Which is to say, I gave it to him as a guided
John, I'm finally responding to your Aug 31 post. I lifted a bold, clever
proof of TRIANGLE_ANGLE_SUM in Multivariate/geom.ml, although your actual proof
may be simpler. I ran your code below, and saw the goalstacks, but they didn't
help much, because it's really TRIANGLE_ANGLE_SUM_LEMMA I
Thanks for correcting my typed LC, Ramana: no Y combinator (that makes sense,
as Y sorta comes from Russell's paradox, which typing was designed to prevent),
and it's simply typed LC. My heavy was just slang, and generated is from
Hales's Notices article. Maybe I wasn't clear about syntax and
Hi Cris,
| To what document is Bill referring here as Michael's Logic manual?
If you go to the HOL4 documentation page, there are links to several
manuals, one of which is the Logic one:
http://hol.sourceforge.net/documentation.html
As the introduction to that manual makes clear, the
Thanks, Konrad! Are you and Michael interested in adding more introductory
material to your HOL4 Logic manual, e.g. along the lines of the excellent intro
material Michael just posted? If so, I might have useful feedback. Or do you
want to keep your manual in its present form? When I hit
Michael, I detect in your previous post a disturbing definition of
theorem-proving:
[Bill] is mathematically sophisticated but a novice as far as
theorem-proving is concerned.
I think I'm quite good at theorem-proving (I have 11 papers published in Math
journals). I'm a novice at
On 30/08/2012, at 17:58, Bill Richter rich...@math.northwestern.edu wrote:
Michael, I detect in your previous post a disturbing definition of
theorem-proving:
[Bill] is mathematically sophisticated but a novice as far as
theorem-proving is concerned.
I think I'm quite good at
Hi Bill,
| Thanks, John! I'd be thrilled if you included my code in the HOL Light
| distribution (miz3 dir sounds good)! I think it would improve my paper's
| chance of being accepted.
OK, I'll be very happy to incorporate it whenever you regard it as
final. Or if you prefer, I can put a
Hi Bill,
Thanks a lot for the detailed discussion of how the angle sum theorem
is typically proved in standard texts, and how the formalization goes.
It's been chastening to me to discover how hard it can be to formalize
what I thought was easy during my schooldays!
| let ANGLES_ADD_BETWEEN =
Michael, that's extremely helpful, I need to read the part about
[p 17] The meaning of HOL terms in such a model will now be described.
and terms means constants as well as abstractions. I should be able to decode
your simple picture from the general description there. Page 19 more
Generally speaking, I'd say that the automation is too powerful
is a problem we'd love [miz3] to have!
Great! Right now it's not powerful enough for me.
Bill, I'm struggling to understand your point of view. Of course,
more automation is a good thing, but presumably in your setting
Bill or Michael in particular, one question:
On Thu, Aug 30, 2012 at 7:39 PM, Bill Richter rich...@math.northwestern.edu
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
Thanks, Michael! I like what you wrote about (me and) the student with little
sophistication when it comes to writing proofs, but I can't see we're helping
by shackling their proof assistant. I want people to learn how to write and
understand mathematical proofs, and I think proof assistants
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)
Hi Bill,
I've worked very hard to make my miz3 Hilbert axiomatic geometry code
readable, and taking huge leaps nobody could follow would be
counterproductive. But I'm against shackling the proof assistant, as we agree
Mizar does but miz3 does not:
Yes, Mizar is certainly shackled in
On 28/08/12 13:29, Bill Richter wrote:
Yes, Mizar is certainly shackled in the way Michael described.
I can't figure out your position. I agree there might be some value in
shackling for retrieval from huge libraries. Why don't we concentrate on
education. I contend that shackling the
Hi Bill,
Josef, it sounds like you're saying that Mizar is intentionally weak, and
that the reason for weakness is to make it practical to make calls to the
huge Mizar library.
The reasoning is that speed implies easy refactoring, and that
facilitates optimization of the library. Making the
I'll be interested to see how the angle sum proof looks in
axiomatic style. I remember being a bit surprised and disappointed
at how messy the vectorial proof is that I once formalized. (See
TRIANGLE_ANGLE_SUM in Multivariate/geom.ml).
John, I now have the angle sum proof formalized,
Thanks, Josef, that's very helpful, and you're saying I was wrong (but right
originally)
I think the original intention behind the weakness was to capture
the right level of reasoning that would be obvious to humans,
i.e., not too strong to puzzle the readers and not too weak to
Thanks, John! I'd be thrilled if you included my code in the HOL Light
distribution (miz3 dir sounds good)! I think it would improve my paper's
chance of being accepted. I'll definitely write to both Hartshorne
Greenberg, but I'll let HOL Light finish debugging my paper first. I think BTW
Freek, can you assure me this is not a bug (it works), ending a miz3 proof with
a semicolon:
angle F O' D _ang angle C O A [H3'] by H3, AngleSymmetry_THM;
seg F D __ seg C A by H1', H2, H3', H4, EuclidPropositionI_24Help;
qed by -, SegmentSymmetry_THM;
end;
`;;
John, something that convinced me that miz3 wants to be strong was stimulated
by Josef, who got the FOL prover Vampire to give 1-line proofs of almost all of
my Tarski miz3 results. Eventually I tried doing the same in miz3, and I'm
including my biggest success below. In about 2 hrs on my
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 propositions (I.1) to
| (I.28) except (I.1) and (I.22), can be proved in an
On Fri, Aug 24, 2012 at 1:28 PM, John Harrison
john.harri...@cl.cam.ac.ukwrote:
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
Hi Bill,
| Thanks! But the OP (me) really was asking a different question: why
| aren't you, Konrad, Rob and Michael all working on the same program,
| which you could maybe call HOL4LightPower? Wouldn't that increase
| productivity? John, you seem to be on the extreme Math end of CS, and
|
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-LightMiz3HilbertAxiomGeometry.tar.gz
Thm 10.4:
All of Euclid's propositions (I.1) to (I.28) except (I.1) and (I.22), can be
proved in an arbitrary Hilbert
On Wed, Aug 22, 2012 at 4:39 AM, Bill Richter rich...@math.northwestern.edu
wrote:
John, I'm still excited by your SET_RULE, but I ran into a problem that
maybe is a serious miz3/set problem, unlike miz3's incomplete ability to
prove abstractions and sets were equal. I distilled my problem
Hi Bill,
| let DoubletonPlusSymmetry_THM = thm `;
| let a b be A;
| let X Y be A-bool;
| assume X = Y;
| thus {a, b} UNION X = {b, a} UNION Y
| by SET_RULE`;;
I think Ramana correctly diagnosed the problem, namely that the X = Y
assumption is not being implicitly used. If you change
Rob wrote:
| Why are there so many HOLs, HOL Light, Hol4, Holzero?
|
| That's a very long story. HOL4 and ProofPower came first in the early
| 90s as a result of roughly simultaneous efforts in academia (HOL4) and
| industry (ProofPower) to port Mike Gordon's original Classic HOL onto
|
Thank Ramana and John, and how dumb of me! Yes, your fix works fine:
horizon := 0;;
let DoubletonPlusSymmetry_THM = thm `;
let a b be A;
let X Y be A-bool;
assume X = Y [H1];
thus {a, b} UNION X = {b, a} UNION Y
by SET_RULE, H1`;;
So I don't have an explanation of why my miz3 code
John and Ramana, thanks again! It turns out that my problem was entirely
caused by my abstraction definition union replacement for UNION. This now
works (as part of 4200 lines of code formalizing Euclid up to Prop I.26, the
Alternate Interior Angles thm), since I switched back to UNION:
let
John, thanks for explaining #trace SET_RULE;; and for your long interesting
response.
A crude approach would be simply to use SET_TAC in place of
MESON_TAC [...] However, I would like to do things a bit more
carefully [...] this would make a good excuse. I will think about
it a bit
John, I'm still excited by your SET_RULE, but I ran into a problem that maybe
is a serious miz3/set problem, unlike miz3's incomplete ability to prove
abstractions and sets were equal. I distilled my problem down to this example,
where the first three results are fine, but the last
John, can you make SET_RULE part of the miz3 by justification? What I just
wrote about Collinear {A, B, C} doesn't yet make sense, because miz3 does not
know that
{A, B, C} = {A, C, B} = {B, A, C} = {B, C, A} = {C, A, B} = {C, B, A}.
At least, I had to work to prove a simpler result that's
On Sat, Aug 18, 2012 at 5:55 AM, Bill Richter rich...@math.northwestern.edu
wrote:
Right now I'm worrying about a different problem, that I've never
understood sets.ml, especially its use of IN_ELIM_THM to prove the
IN_operation theorems. After Michael taught me that a {...} is equal, in
a
Thanks for responding, Ramana! I see only one advantage to redefining set
operations (e.g. INTER) as abstractions: it makes my code easier to read for me
and my target audience of mathematicians, as I can substitute the very easy
BETA_THM for the subtle and complicated IN_ELIM_THM that Michael
Here's something quite interesting that HOL Light taught me about geometry
recently. As I've said, I'm basically rigorously proving something that
Hartshorne sketched in
Geometry, Euclid and Beyond, Undergraduate Texts in Math., Springer, 2000
that Hilbert's work gives a beautiful
On 17/08/12 07:51, Bill Richter wrote:
There's no reason for me to use these defs explicitly rather than
IN_ELIM_THM, which uses them, but this definition bewilders me:
let IN_ELIM_THM = prove
(`(!P x. x IN GSPEC (\v. P (SETSPEC v)) = P (\p t. p /\ (x = t))) /\
(!p x. x IN GSPEC (\v.
On 17/08/12 14:11, Bill Richter wrote:
Michael, here's a 1-line HOL Light proof of your exercise
{ x | x ∈ P ∧ x ∈ Q} = λx. P x ∧ Q x:
let IntersectionAbstractionIsLambda = prove (
`!P Q :A-bool. {x | x IN P /\ x IN Q} = \x. x IN P /\ x IN Q`,
REWRITE_TAC[IN_ELIM_THM; EXTENSION]);;
If
Hi Bill,
| and I see no reason not to code up the parts of sets.ml using lambdas.
Is the main motivation for doing this the fact that miz3's default
prover doesn't handle set notations very competently, or the fact that
the encoding of sets and the IN_ELIM_THM theorem that's used to
unravel
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:
On 18/08/2012, at 4:18, Cris Perdue c...@perdues.com wrote:
REWRITE_CONV [IN_ELIM_THM] `{x + y | x IN P /\ 10 y}`
it won't be disturbed because it doesn't have that external `x IN` at the
front.
It appears to me that Michael is trying to make a point here that I'm not
grasping, and
Thanks for explaining GSPEC, SETSPEC IN_ELIM_THM, Michael! I'm glad to know
that HOL4 can replicate my 1-line proof with SRW_TAC [][EXTENSION], similarly
complicated underneath the hood. I'm confused by you paraphrasing Konrad as
saying that your exercise was annoying to prove. It would
Michael, here's a 1-line HOL Light proof of your exercise { x | x ∈ P ∧ x ∈ Q}
= λx. P x ∧ Q x:
let IntersectionAbstractionIsLambda = prove
(`!P Q :A-bool. {x | x IN P /\ x IN Q} = \x. x IN P /\ x IN Q`,
REWRITE_TAC[IN_ELIM_THM; EXTENSION]);;
If you can't do that in HOL4, that's evidence for
On 15/08/12 14:41, Bill Richter wrote:
A counterexample to what you wrote:
If you never use that [{ n + 1 | n 6 }] notation, then it's
certainly fine to just view { x | P x } as a fancy way of writing
(λx. P x).
I'll give 3 reasons below to indicate this isn't true for me (I
Thanks, Michael! I definitely did not know that, but I should have, as it
sounds like EXTENSION should prove it. Here's miz3 evidence for that, as this
proof works with MESON solved at number 69,282:
#load unix.cma;;
loadt miz3/miz3.ml;;
horizon := 0;;
timeout := 30;;
let
Thanks, Konrad! Could you check to see if the HOL4 method of proving the IN_*
theorems is simpler than the HOL Light method? If it isn't, then maybe I
should be satisfied with what I came up with,following sets.ml
let IN_Interval = prove
(`! A B X. X IN open (A,B) = Between A X B`,
Michael, I'm really grateful to you, as you cleared up my main problem:
Now is my interpretation of my own code correct?
Your interpretation of what you've written seems fine to me.
That's great. I have to tell my audience of mathematicians what theorems HOL
Light is verifying, even
Hi Bill,
It's important to understand that the HOL4 Logic Manual gives a
(more-or-less) formal semantics of a formal logic. That's two levels of
formal! None of the set theory given in this document is actually part of
the HOL logic itself. Rather the set theory is a formal way of portraying
Does HOL4 have anything comparable to sets.ml?
Yes it will have, and it will probably be spread over many source code
files, but I'm afraid I don't know where this is in the HOL4 source. This
is a question for HOL4 community, Michael et al. I'm more of a HOL Light
and HOL Zero person.
The
Bill,
On Sun, Aug 12, 2012 at 9:53 PM, Bill Richter rich...@math.northwestern.edu
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
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 the point of an acknowledgment isn't to pay someone for
http://plato.stanford.edu/entries/type-theory/ by Thierry Coquand
(associated with Coq), and
http://plato.stanford.edu/entries/type-theory-church/ by Peter Andrews
Cris, these look really good! Are you telling me that the term Coq comes from
Thierry Coquand's name?
--
Best,
Bill
Konrad, this is very interesting, because it's so much like sets.ml:
There is also a description of sets in HOL4 in the manual. Start at
p. 102 of the HOL4 Description document:
Yours Michael's Description manual starts pretty much like sets.ml which I
cited above.
Not surprising.
Le 13 août 12 à 21:13, Bill Richter a écrit :
http://plato.stanford.edu/entries/type-theory/ by Thierry Coquand
(associated with Coq), and
http://plato.stanford.edu/entries/type-theory-church/ by Peter
Andrews
Cris, these look really good! Are you telling me that the term Coq
comes
On 11/08/2012, at 17:05, Bill Richter rich...@math.northwestern.edu wrote:
My main problem is that I don't understand HOL, so I don't know what theorems
HOL Light is proving for me. The HOL4 Logic manual looks like a very
respectable CS document, but I haven't been able to read it yet, and
Hi Bill,
There are a few points which you may or may not already realise. Sorry if
these are obvious, but I haven't been following the (very lengthy!) thread
in detail.
1. Just checking you understand this: In HOL Light and HOL4 (but not
ProofPower HOL), sets are represented as functions to
Hi Bill,
... My main problem is that I don't understand HOL, so I don't know what
theorems HOL Light is proving for me. The HOL4 Logic manual looks like
a very respectable CS document, but I haven't been able to read it yet,
and
it's not a HOL Light document.
And it's not a particularly
Thanks, Michael! I will treat the Logic Manual as a true description of the
HOL in HOL Light, and I will try harder to read it. I have a lot of trouble
with your 3 sentences:
Sets in HOL Light and HOL4 are predicates over their respective
types. Types correspond to non-empty sets (as
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 think mathematicians can't be expected to
understand him. He starts
On 13/08/12 14:17, Bill Richter wrote:
Thanks, Michael! I will treat the Logic Manual as a true description of the
HOL in HOL Light, and I will try harder to read it. I have a lot of trouble
with your 3 sentences:
Sets in HOL Light and HOL4 are predicates over their respective types.
On 13/08/12 14:53, Bill Richter wrote:
That sounds great, but here I want more details:
The types are presented in the HOL Light System box.
Terms are the basic mathematical objects of the HOL Light system. The
syntax is based on Church’s lambda-calculus [to define functions]
Now that the Platonism discussion has died down (didn't Russell's paradox show
the Platonic world of forms doesn't exist?), let me repeat two requests for
help, as I should be done in 2 or 3 weeks. I have 3700 lines of miz3 code
I made real progress on my set theory problem, but I'd like to do even better.
My 3860 lines of miz3 Hilbert axiomatic geometry code
http://www.math.northwestern.edu/~richter/RichterHOL-LightMiz3HilbertAxiomGeometry.tar.gz
now uses set abstraction to define rays:
let Ray_DEF = new_definition
My old definition of ray OK. The problem was int_angle, where I needed this
clumsy looking usage, with the useless and unsettling first line of the proof
let InteriorWellDefined_THM = thm `;
let A O B X P be point;
assume P IN int_angle A O B [H1];
assume X IN ray O B DELETE O
I'm going to consider the matter settled: the real miz3, with timeout = -1, was
not weakened by John Freek. They did not desire to restrict the miz3 by
to small inference leaps. Arguing that the default timeout of 1 is an
intentional weakness has a certainly logical correctness, but it's
On 08/08/12 16:45, Bill Richter wrote:
My claim [on whether miz3 is intentionally weakened] is based on my
believing that miz3 imposes a time limit,
Thus, I conclude that the purpose of the default timeout isn't to weaken
miz3, but to better instruct beginners who, if I'm a representative
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
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
Michael, this is a discussion of motivation. My desire is for miz3 to become
stronger, so I can take bigger inference leaps that will take less time. That
would be pointless if John Freek's desire was that miz3 be ``less able to
prove goals,'' as you did not quite say. So I've tried to
Freek, I just caught myself making a big inference leap that I didn't intend.
The line below
F NOTIN l [notFl] by l_line, Distinct, I1, Collinear_DEF, Fexists,
NOTIN;
is a bug on my part. I meant to write
F NOTIN l [notFl] by l_line, Cl, Collinear_DEF, -, NOTIN;
Miz3
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,
On Tue, Aug 7, 2012 at 1:19 PM, Freek Wiedijk fr...@cs.ru.nl wrote:
Also, does anyone know what is the status of Mohan
Ganesalingam's work in this direction (see for example
http://people.pwf.cam.ac.uk/mg262/CSLI%20talk.pdf)?
No, but we can ask him :) (CC'ed)
Context:
You check that your definition is correct by proving appropriate
theorems about it. For example, HOL4 provides an EVAL function so
that you can do things like
EVAL ``FACT 20``;
val it = |- FACT 20 = 243290200817664: thm
and this is the sort of thing you'd like to
On 08/08/12 11:21, Bill Richter wrote:
Thanks, Michael! HOL Light does not have your EVAL, but maybe it has
something similar. EVAL is indeed the sort of thing that Colin Rowat and I
were looking for. I did read a bit about rewriting, and I see that it's in
the EVAL ballpark, but it
On Sun, 5 Aug 2012, Konrad Slind wrote:
My opinion is that Peter Homeier's HOL-Omega is the right setting to
properly implement something locale-like, since it provides
quantification over type variables in the logic. In plain old HOL the
implementation of locales as essentially
Thanks, Ramana! I've often wanted Isabelle locales. Are you going to code
them in HOL4? For readability I'd like to not constantly have this annoying
TarskiModel hypothesis hanging around, as Michael said, but it would be good
to write up a longer version of at least part of my code to show
It also looks as if you could dispense with the T parameter, and just have
A1axiom (===) = !a b. a,b === b,a
Thanks, Michael, it works!!! Whether or not I use first
parse_as_infix(===,(12, right));;
But I think that's only because === is already declared to be an infix. I
don't
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
HOL4 meaning of
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,
On 5/08/12 8:49 PM, Bill Richter wrote:
parse_as_infix(cong,(12, right));;
let cong_DEF = new_definition `a,b,c cong x,y,z = a,b === x,y /\
a,c === x,z /\ b,c === y,z`;;
My problem, I think, is that cong is now a function of ===, which is
now a variable being passed around. Here's my miz3
On 5/08/12 7:42 PM, Rob Arthan wrote:
A non-polymorphic type denotes a non-empty ZFC set. We can assume
that this set is one of the non-empty sets in the von Neumann
cumulative hierarchy formed before stage ω + ω (Logic Manual,
p10)
That isn't quite right. What the Logic Manual correctly
On 5/08/12 5:18 PM, Bill Richter wrote:
Thanks, Ramana! I've often wanted Isabelle locales. Are you going to
code them in HOL4? For readability I'd like to not constantly have
this annoying TarskiModel hypothesis hanging around, as Michael
said, but it would be good to write up a longer
Anyway, I've asked myself the same question above, when some HOL person
will start to implement a version of sections or locales. My estimate
is that when starting today, it would take approx. 5 years to make this
become real. Our very first version of Isabelle locales can be seen here
(14
Cris, the axiom of choice is essential in much of modern math, and I'm guessing
that's John's reason.
Rob, that was a very interesting post, which I can't do justice too. I would
be very interested if you say anything about Vladimir V's Coq work. Your
Topology paper looks very cool, and I'll
Thanks, Michael, I'll try out your cong trick. Your type_of `MAP`;; was plenty
illuminating, that's how I figured out what polymorphism meant, with the Scheme
analogy, but I'm confused. On p 350 of
http://www.cl.cam.ac.uk/~jrh13/hol-light/reference.pdf
it explains lower-case map:
map : ('a -
On Fri, Aug 3, 2012 at 4:43 AM, Bill Richter
rich...@math.northwestern.eduwrote:
Define a four-argument predicate
Hilbert_plane H (Between) (===) Line = axiom_1_holds /\ axiom_2_holds
/\
...
and use that as a hypothesis on all your theorems.
Thanks, Ramana! The code below
On Thu, Aug 2, 2012 at 8:03 AM, Bill Richter
rich...@math.northwestern.eduwrote:
Thanks, Ramana and Rob! As Rob says, I don't use new_axiom to define by
type point, but I do use new_axiom to define Hilbert's geometry axioms,
so I took no offense. I would definitely prefer to use neither
Thanks, Ramana! I don't quite understand. In each theorem I should
make an extra hypothesis which will look something like assume
Hilbert_plane H (Between) (===) Line {HP};
And I'll add the label HP to each by list in which I refer to one of
my earlier theorems? In your earlier post, I think
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
HOL4 meaning of this is, but I have a new conjecture: My new_type
On Wed, Aug 1, 2012 at 6:00 AM, Bill Richter
rich...@math.northwestern.eduwrote:
new_type(point,0);;
new_type_abbrev(point_set,`:point-bool`);;
new_constant(Between,`:point-point-point-bool`);;
new_constant(Line,`:point_set-bool`);;
new_constant(≡,`:(point-bool)-(point-bool)-bool`);;
I
Thank you Rob! I was hoping for someone to clear up my mistakes and teach
me something more about conservative extension :)
(I may come off sounding confident but usually I am not.)
Also, Bill if you're not using new_axiom, then sorry for any offence caused
by the tone of my previous email.
On
Ramana,
new_type and new_constant add new types and new constants to HOL
by fiat.
What these functions do is introduce new names into the available
vocabulary (or signatures and type signatures to use the terminologies of
the LOGIC manual). This is a conservative extension mechanism. For
Rob, thanks for explaining your ProofPower proof was shorter than mine. I went
to your ProofPower web site, and it sounds similar to HOL Light. Is it easy to
port code from one to the other? You must be a HOL Light expert, because John
H thanked you (along with Freek W and Michael N) in his
the intuition is just in a little diagram with 4 points and lots of
edges labelled P and Q.
Thanks, Rob, and I think I understand now! You solved Los's Logic problem
because you had the courage to try a bold frontal attack, while I floundered
for the lack of some cool insight. This is
Sorry, Rob, I had a dumb typo, and meant to write there exists a b such that a
!~ b (i.e. a ~ b is false).
Konrad and Michael, as I see you're an author of the HOL Logic manual
http://sourceforge.net/projects/hol/files/hol/kananaskis-7/kananaskis-7-logic.pdf/download
I'll ask you a question
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 version which runs in HOL Light. I recommend you learn
miz3, and I
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 version
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), and it got me thinking, and I now have some
understanding of Los's Logic problem. The problem with Los's result is it
makes no sense: P is
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 having
1 - 100 of 240 matches
Mail list logo
