Hi Bill, | Thanks, John! Sorry I don't have my bug reports yet. I'm using | Scientific Linux, not Debian, so I can't use Hendrik's package.
Well, perhaps someone will also package it up for Red Hat before long. Maybe there is some way of importing "alien" packages, though I don't think I've ever done it. | What I'm trying to do is much simpler than what Phil etc are doing. | It should be trivial in HOL Light. It shouldn't require the full | strength of Freek's ambitious miz3. I just want 2-column high school | Geometry proofs. I'll use Hilbert's or Tarski's axioms, which | actually give rigorous proofs, but it's still 2-column proofs. If you really just want a list of "<statement> <reason>" pairs, then perhaps a full Mizar mode is overkill and there are simpler alternatives. I suppose that most geometric problems are purely universally quantified so the extra structuring steps are not as important. Nevertheless, they might be useful sometimes, and since you already have proofs in Mizar style, the difficulty of translation is probably lowest if you simply use miz3 as the first target. Moreover, while miz3 is a non-trivial piece of code, a lot of it is just a parsing and interaction wrapper round existing facilities. A principle of LCF-style systems like HOL Light is that you can easily write extensions that are guaranteed sound. (Just don't alter the small logical core in "fusion.ml", and avoid weird programming tricks, new_axiom etc., as Makarius and Freek have been discussing.) Users are welcome, I would almost say encouraged, to write custom extensions to the system. For example, you may want to tweak the behavior of miz3 a bit, or even write a simplified Mizar mode of your own. The idea of writing your own theorem proving code may seem intimidating, but once you have gained a bit of experience with HOL Light, it becomes surprisingly tractable. One of the motivating principles for HOL Light's simple and spartan nature is precisely that it makes such programmatic extensions relatively easy, so you can customize it and build your own interaction model around it. See for example sections 23 (custom tactics), 25 (custom inference rules) and 26 (linking external tools) of the HOL Light Tutorial. | Phil is trying to get HOL Light to fix profs from Hilbert's arcane | book, that takes a real theorem prover. Yes, this is really making use of programming to fill in tricky gaps in the incidence reasoning and so on, which is indeed more ambitious. It will be interesting to see whether you encounter similar issues in your own formalization from the Tarski axioms, with some of the steps becoming painful by hand and motivating more ambitious automation. | BTW what do you call HOL Light? Is it a proof assistant, or a | theorem prover, or a proof checker? I'm not sure I am very consistent in my own terminology, but "proof assistant" is probably the most accurate. Some might prefer to call it a "proof adversary". John. ------------------------------------------------------------------------------ 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
