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 and shallow embedding of several variants of 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., [106] for a discussion about deep vs. shallow embeddings in Isabelle/HOL. The shallow embedding of ITL uses techniques developed by Stefan Merz [192, 24] for the shallow embedding of Temporal Logic of Actions (TLA) in Isabelle/HOL.

4.3.1 Finite and Infinite ITL, shallow and deep embedding

Download:

4.3.2 Finite ITL, shallow embedding

Download:

4.3.3 Finite ITL, deep embedding

Download:

2025-03-20
Contact | Home | ITL home | Course | Proofs | Algebra | FL
© 1996-2025