Email Gateway (Aug 18 2022 at 14:26): Email Gateway (Aug 18 2022 at 14:26):From: Сергей Каунов <skaunov@gmail.com>
Hello!
I'm sorry for disturbing you with the question, which may be quite
silly. I want to use Isabelle for some very simple temporal reasoning by
modal logic. Neither S4, neither Modal0 nor other modal thys aren't
covered in logics.pdf. :sad:
I starred on corresponding files and twisted them as I could, but didn't
found any natural way to evaluate propositions in Sequents logic. Is
there some hidden door, walkaround or a simple decision I missed?
Thanks in advance!
Email Gateway (Aug 18 2022 at 14:26):From: Stephan Merz <Stephan.Merz@loria.fr>
Hello Sergei,
most textbook presentations of proofs in modal and temporal logics are based on either Hilbert-style or sequent-style proof systems, neither of which are well supported in Isabelle. (The formalization of sequents as an Isabelle object logic that you refer to is quite old and has, AFAIK, not evolved since at least a decade; it is not supported by Isabelle's efficient automatic proof methods.)
An alternative is to embed the "forcing" relation "sigma |= phi" (phi holds over structure sigma) in one of the well-developed object logics of Isabelle such as Isabelle/HOL, and to define validity "|= phi" as "\<forall> sigma. sigma |= phi".
For example, for linear-time temporal logic, sigma would be an infinite sequence of states, which themselves are valuations of atomic propositions. You would then define the semantics of operators such as X (next time) and G (always) according to their standard definition over sequences. From these you can derive standard LTL laws such as
|= (G phi) <=> phi /\ XG phi
within the representation of LTL. Branching-time temporal logics can be handled similarly.
This approach has been followed several times. You may want to look at sessions "Modelcheck" or "Unity" in the HOL library for similar formalizations. (My own "TLA" embedding is related, but stupidly based on an axiomatic rather than definitional approach to defining temporal operators.)
If you are interested, I could send you (off-list) a simple embedding of LTL in HOL.
Best regards,
Stephan
Last updated: Apr 20 2024 at 04:19 UTC