Email Gateway (Aug 18 2022 at 10:11): Email Gateway (Aug 18 2022 at 10:11):From: Tobias Nipkow <nipkow@in.tum.de>
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 help
me.
Please consult the table of ascii equivalents of mathematical symbols in
the appendix of the Tutorial on Isabelle/HOL.
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
Last updated: May 03 2024 at 12:27 UTC