*To*: Joseph Vidal-Rosset <joseph.vidal-rosset at univ-nancy2.fr>*Subject*: Re: [isabelle] checking if a formula is intuitionistically valid*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Wed, 14 Feb 2007 18:21:03 +0100*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <20070214105555.2416da98@debian>*References*: <45D29567.9080006@nicta.com.au> <20070214105555.2416da98@debian>*User-agent*: Thunderbird 1.5.0.2 (Macintosh/20060308)

First of all, I would be happy if I'd succeed to use isabelle just as as simple theorems checker for formulas of first order logic. For example, I do not even succeed in checking the validity of a classical formula like: (p \to q) \leftrightarrow (\neg q \to \neg p) (1) I know that it is not useful to get isabelle in order to use it at this low level, but I would be happy to get help just with the syntax. I do not know why when I try to read the manuals I meet always message of error. Thanks to tell me how to translate (1) in isar. That will helpme.

The second question that I want to ask here is maybe very naive, but I do not feel shame. Is it possible to use isabelle just to check it a propositional formula is intuionistically valid, or just classically valid? For example: can isabelle tell me that (p \lor \neg p) is not (intuitionistically) valid? And what about first order intuitionist

apply iprover (* for intuitionistic logic *) apply blast (* for classical logic *) Regards Tobias

**References**:**[isabelle] defining a constant with a long-identifier name***From:*Michael Norrish

**[isabelle] checking if a formula is intuitionistically valid***From:*Joseph Vidal-Rosset

- Previous by Date: Re: [isabelle] finite set syntax
- Next by Date: [isabelle] Accessing split-theorems on ML-level
- Previous by Thread: [isabelle] checking if a formula is intuitionistically valid
- Next by Thread: Re: [isabelle] defining a constant with a long-identifier name
- Cl-isabelle-users February 2007 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list