On 03/01/2013 10:07, Ramana Kumar wrote:
> On Thu, Jan 3, 2013 at 6:06 PM, Bill Richter
> <[email protected] <mailto:[email protected]>>
> wrote:
>
> Β Β > BTW how does HOL and Informatics fit together?
>
> Β Β How do they not? :) They are connected in so many ways...
>
> I think hol-info ought to have much more info about how HOL is used
> in the real world. Β Why not more details!
>
I agree gathering this kind of information (not only for informatics but
also for any applicable field) would be beneficial especially for
newcomers in the community.
HOL systems are commonly used in informatics for software and hardware
verification. For example, (as far as I can tell) this is the kind of
thing John is working on at Intel.
For my research, as another example, I am using an embedding of Linear
Logic to specify and reason about services/processes and their
compositions/workflows in HOL Light.
> Β
>
>
> Β Β (Note how DISCH_TAC is *roughly* equivalent to DISCH_THEN
> ASSUME_TAC.)
>
> Michael posted that too, and I'm confused. Β I think DISCH_TAC is
> exactly DISCH_THEN ASSUME_TAC.
>
>
> In HOL4, you are right: they are exactly the same.
> (The only difference I see is that DISCH_TAC will re-raise any
> exceptions as having originated with DISCH_TAC rather than with DISCH_THEN).
My apologies for confusing you Bill. My memory betrayed me. They are in
fact the same (apart from what Ramana pointed out), as shown by the
definition of DISCH_THEN:
let (DISCH_THEN: thm_tactic -> tactic) =
fun ttac -> DISCH_TAC THEN POP_ASSUM ttac;;
Regards,
Petros
--
Petros Papapanagiotou
CISA, School of Informatics
The University of Edinburgh
Email: [email protected]
---
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
------------------------------------------------------------------------------
Master Visual Studio, SharePoint, SQL, ASP.NET, C# 2012, HTML5, CSS,
MVC, Windows 8 Apps, JavaScript and much more. Keep your skills current
with LearnDevNow - 3,200 step-by-step video tutorials by Microsoft
MVPs and experts. ON SALE this month only -- learn more at:
http://p.sf.net/sfu/learnmore_122712
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
