I understand exactly what you are looking for (or at least I think I do!) - a theorem prover with very clearly defined functionality, that automates what is "trivial" and does not automate what is not "trivial"
Thanks, Mark, and that's exactly right. and that is easy to use, caters for all the classic styles of doing (symbolic) proof on paper and does not require months of training. Yeah, and right now only one style: 2-column proofs that are common in US high school Geometry courses, except I want rigorous proofs you get from Hilbert's axioms, and not the ''when the going gets tough we'll draw a picture and say it's obvious'' style going back to Euclid. I've had in mind for many years a design of a system that does exactly what you want You don't have to implement your system to help me. Maybe it's enough to clarify what "trivial" means. I should know by now, from writing 2300 lines of miz3 Hilbert axiomatic geometry code http://www.math.northwestern.edu/~richter/RichterHOL-LightMiz3HilbertAxiomGeometry.tar.gz but I don't. Somehow my fuzzy idea is that the automation ought to just be calculating how to use the the axioms and theorems I list to prove the statements I want. Uh, that didn't sound right! Isn't any proof like that? If someone would run my code and watch MESON churn, maybe they could clarify what "trivial" means. I suppose a problem with using existing systems is that they are trying to do something different - to enable proofs to be proved with minimal amount of user effort. I don't think that's the problem. I think the problem is my practical ignorance of FOL. I haven't read John's purple book yet and understood what he thinks a Mizar-like proof assistant in FOL is. And if this system is also a "serious" system involved in the formalisation of mathematics, and is highly trustworthy, then all the better. You see such a system as being an excellent way of teaching students how to do proof. Yes, particularly as the students may feel they are learning valuable computer skills. But I've actually learned a lot about my paper http://www.math.northwestern.edu/~richter/hilbert.pdf I believe my proofs more because HOL Light checked them, and formalizing the proofs clarified my thinking. Here's the first thing I learned, and I sure felt dumb when I figured it out. http://en.wikipedia.org/wiki/Hilbert%27s_axioms I. Combination 7. Upon every straight line there exist at least two points, in every plane at least three points not lying in the same straight line, and in space there exist at least four points not lying in a plane I translated this (restricting to one plane) as there ∃ X Y Z:point . ¬∃ l: line. X ∈ l ∧ Y ∈ l ∧ Z ∈ l Well, I was wrong! We have to insist that X, Y, Z are distinct points. Arguably that's what `at least three points' means. If we use my busted version of the axiom, then we can get a model of Hilbert plane geometry with one point and no lines! I've learned more complicated things about my paper as well :) By the way, "malicious" proofs are not proofs that use a theorem prover's automatic facilities when they are not intended to be used. Malicious proofs are proofs that deliberately take advantage of unsoundness (or other trustworthiness issues) in the theorem prover, to prove a fallacy, or to appear to prove a fallacy. Thanks. I suppose your unsoundness and my excessive power are related ideas, but they're quite different too. your problem is that you don't know how powerful (in the automation dimension) each of the miz3 keywords is, so you wouldn't know which ones to include in your restricted set anyway. For that you will have to search for documentation, read the miz3 code, or wait for someone who knows to answer because unfortunately I don't :) That's right, Ramana, and Freek doesn't seem to know either, so reading the miz3 code is probably quite difficult. A while back Freek said that miz3 has two pieces, HOLBY and MESON, and that HOLBY does everything that Mizar does, and then MESON takes over (and you can see this, because it churns numbers and prints "solved at"), so miz3 is more powerful than Mizar! That was very helpful of Freek, but I posted that my very Mizar-like Tarski axiomatic geometry code where MESON did quite a lot of work. The first time I did this, Freek said no, you have to curry your functions to get a miz3/Mizar comparison, because MESON has to calculate all the pairs, so I uncurried every function of mine, and still have pretty big MESON solved at numbers. -- Best, Bill ------------------------------------------------------------------------------ Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
