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,
On Thu, Jul 19, 2012 at 9:54 AM, Freek Wiedijk fr...@cs.ru.nl wrote:
I forgot who wrote this
One way to ameliorate this problem is to compose proofs lazily.
That was me.
but anyway:
Doesn't the Isabelle kernel now have a feature that you can
postpone proving a thm and still already being
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
Hi Konrad,
On Thu, Jul 19, 2012 at 7:35 AM, Konrad Slind konrad.sl...@gmail.comwrote:
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
On Thu, 19 Jul 2012, Freek Wiedijk wrote:
Doesn't the Isabelle kernel now have a feature that you can postpone
proving a thm and still already being allowed to use it? I think
Makarius put that in the kernel especially to be able to parallelize
Isabelle proof checking on multi-core
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
On Wed, Jul 18, 2012 at 7:49 PM, Felix Breuer fe...@fbreuer.de wrote:
Hi Ramana!
2012/7/16 Ramana Kumar ramana.ku...@gmail.com
One way to ameliorate this problem is to compose proofs lazily.
By that, I mean when you get to a step that's obvious to you, just cheat
(most proof assistants have
One way to ameliorate this problem is to compose proofs lazily.
By that, I mean when you get to a step that's obvious to you, just cheat
(most proof assistants have some option to make a tagged theorem without
proof).
Do you (or anyone) know if there is a way to do this in HOL Light?
Hi Ramana!
2012/7/16 Ramana Kumar ramana.ku...@gmail.com
One way to ameliorate this problem is to compose proofs lazily.
By that, I mean when you get to a step that's obvious to you, just cheat
(most proof assistants have some option to make a tagged theorem without
proof).
Do you (or
Do you (or anyone) know if there is a way to do this in HOL Light?
Looking at HOL Light's kernel briefly I think the only thing you can
do is call new_axiom a lot
How about making assumptions? Then at the end you just have to check that
your theorems have no unwanted assumptions...
Freek, you're running a very interesting discussion with Mark, Felix,
Chris etc. I'd like to know why Mark can't do his interface
improvements on HOL Light. Responding to your points:
Maybe you _would_ experience those steps very fleetingly, but you
wouldn't focus at them in the way a
Hello everyone,
I think the two problems Freek mentioned are indeed by far the most
important obstacles to creating a truly usable proof assistant. However,
there is also merit in addressing the points Mark and Cris mention: A nice
system that solves all these surface usability issues, may well
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
On Wed, Jul 11, 2012 at 8:38 PM, Mark m...@proof-technologies.com wrote:
I intend to cater for both the declarative style (i.e. stating the result
of
the step) and the imperative style (i.e. stating what operation to apply
next), and a mixture of both. I think that this is a huge subject
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
Hi Ramana,
I'm not quite sure how to interpret your question. Are you suggesting that
HOL4's user interface, with it's existing provision for mixing declarative
and imperative styles, is perfectly good already, or are you suggesting that
it's difficult to get any better (regardless of whether
On Thu, Jul 12, 2012 at 3:37 AM, Freek Wiedijk fr...@cs.ru.nl 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
I was reading the following article when this message arrived. Hope some
of you might find it useful.
http://www.useit.com/alertbox/20030825.html
On 2012-07-12, at 3:32 PM, Mark wrote:
Hi Ramana,
I'm not quite sure how to interpret your question. Are you suggesting that
HOL4's user
on 9/7/12 5:48 PM, Cris Perdue c...@perdues.com wrote:
What I was talking about though is ease of use of software products,
and a proof assistant is definitely a software product. To get many
people to use a software product, especially one that is not just a
minor variation on one
Mark wrote:
on 9/7/12 5:48 PM, Cris Perdue c...@perdues.com wrote:
What I was talking about though is ease of use of software products,
and a proof assistant is definitely a software product. To get many
people to use a software product, especially one that is not just a
minor
Hi Cris,
Thanks for the enthusiastic endorsement! I know what you mean about years
of training instead of months of training. I was erring on the side of
understatement rather than overstatement!
I'm not sure if I've got the webpage working properly on the Khan Academy
website. What is
What I am aiming at is a theorem prover that makes formalising such
pen-and-paper [Undergraduate textbook] proofs quick and trivial.
Mark, since this is an HOL newsgroup, can you say something about how
you're going to do this? Why is your classic LCF-style interactive
theorem prover going
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
23 matches
Mail list logo
