Hi Shruti. Have you checked out the HOL Light tutorial? http://www.cl.cam.ac.uk/~jrh13/hol-light/tutorial.pdf
On 21/11/14 20:37, Shruti Chawla wrote: > Hi, I am fairly new to HOL Light and OCaml. I'm unable to find a proof > for Pierce's law in HOL Light. Could you provide me with a proof for it? HOL Light has a decision procedure TAUT for classical tautologies like this. The manually proven propositional theorems and just there, I believe, to bootstrap that decision procedure. I'm pretty sure Pierce's law isn't among them. > > Also, I was trying to prove a simple goal > # g `!p q r. p \/ (q /\ r) ==> p /\ q \/ p /\ r`;; > # e (INTRO_TAC "!p q r; p | q r");; > > but I keep getting the error 'Unbound value INTRO_TAC" I wasn't even aware such a tactic existed! It turns out it was contributed in 2013. My guess is that you need to make sure you're version of HOL Light is up-to-date: svn checkout http://hol-light.googlecode.com/svn/trunk/ hol-light-read-only > > I would really appreciate it if someone could clarify my doubts. Looking > forward to your response eagerly. > > Thanks and Regards > Shruti > > > ------------------------------------------------------------------------------ > Download BIRT iHub F-Type - The Free Enterprise-Grade BIRT Server > from Actuate! Instantly Supercharge Your Business Reports and Dashboards > with Interactivity, Sharing, Native Excel Exports, App Integration & more > Get technology previously reserved for billion-dollar corporations, FREE > http://pubads.g.doubleclick.net/gampad/clk?id=157005751&iu=/4140/ostg.clktrk > > > > _______________________________________________ > hol-info mailing list > [email protected] > https://lists.sourceforge.net/lists/listinfo/hol-info > -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. ------------------------------------------------------------------------------ Download BIRT iHub F-Type - The Free Enterprise-Grade BIRT Server from Actuate! Instantly Supercharge Your Business Reports and Dashboards with Interactivity, Sharing, Native Excel Exports, App Integration & more Get technology previously reserved for billion-dollar corporations, FREE http://pubads.g.doubleclick.net/gampad/clk?id=157005751&iu=/4140/ostg.clktrk _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
