Email Gateway (Aug 18 2022 at 17:13): Email Gateway (Aug 18 2022 at 17:13):From: John Munroe <munddr@gmail.com>
Hi,
If I have a theory containing something like:
rule1: "a = 1 --> p = 0"
where a and p are naturals. Is there a good way to express that
whether there exists a condition such that if it is satisfied, then "p
= 0"? We know that there is because "a = 1" by rule1.
Thank you in advance.
Regards,
John
Email Gateway (Aug 18 2022 at 17:13):From: Tjark Weber <webertj@in.tum.de>
John,
I am not sure I understand your question. Working in higher-order
logic, you can quantify over truth values/predicates:
lemma "EX Q. Q --> p = 0"
However, the lemma trivially holds (independently of rule1): Q can be
instantiated to False, or to "p = 0".
Kind regards,
Tjark
Email Gateway (Aug 18 2022 at 17:13):From: John Munroe <munddr@gmail.com>
lemma "EX Q. Q --> p = 0"
However, the lemma trivially holds (independently of rule1): Q can be
instantiated to False, or to "p = 0".
Hi Tjark,
Yes, quantifying over Q was the first thing that came to my mind. But
like you said, it trivially holds. So is there a way to formulate it
such that it isn't trivial? I want to check that if there is such a
precondition such that "p = 0". If there isn't, then the statement
should be evaluated to False.
Thanks
John
Kind regards,
Tjark
Email Gateway (Aug 18 2022 at 17:13):From: Timothy McKenzie <tjm1983@gmail.com>
I don't know if this is precisely what you're looking for, but
what you're asking for seems to have the flavour of modal logic:
http://en.wikipedia.org/wiki/Modal_logic
I don't know how easily this could be (or perhaps already has
been) incorporated into Isabelle. Perhaps someone else could
address that question.
Timothy
<><
signature.asc
Email Gateway (Aug 18 2022 at 17:13):From: Timothy McKenzie <tjm1983@gmail.com>
I don't know if this is precisely what you're looking for, but
what you're asking for seems to have the flavour of modal logic:
http://en.wikipedia.org/wiki/Modal_logic
I don't know how easily this could be (or perhaps already has
been) incorporated into Isabelle. Perhaps someone else could
address that question.
Timothy
<><
signature.asc
Email Gateway (Aug 18 2022 at 17:14):From: Tjark Weber <webertj@in.tum.de>
Isabelle/Sequents
(http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/Sequents/index.html) contains implementations of modal logics.
However, depending on John's application, it might be more appropriate
to define the modal operators in Isabelle/HOL. An extensive repository
that defines modal (and other) algebras is currently available at
http://staffwww.dcs.shef.ac.uk/people/G.Struth/isa/
Kind regards,
Tjark
Last updated: Nov 21 2024 at 12:39 UTC