4.3 ITL library for Isabelle/HOL

Isabelle/HOL is a generic proof assistant. It allows mathematical formulas to be expressed in a formal language and provides tools for proving those formulas in a logical calculus.

We have given a deep embedding of propositional ITL and a shallow embedding of first order ITL in Isabelle/HOL. A shallow embedding represents ITL using Isabelle/HOL predicates, while a deep embedding would represent ITL formulas as mutually inductive datatypes. See, e.g., [103] for a discussion about deep vs. shallow embeddings in Isabelle/HOL. The shallow embedding of first order ITL uses techniques developed by Stefan Merz [186, 23] for the shallow embedding of Temporal Logic of Actions (TLA) in Isabelle/HOL.

4.3.1 Shallow embedding

Finite and Infinite ITL


Finite ITL


4.3.2 Deep embedding


Contact | Home | ITL home | Course | Proofs | Algebra | FL
© 1996-2023