Finite tree-like model property for multi-modal logic in Isabelle/HOLZF

HAL 2026 Preprint Open access

Read full text
Authors: Yiming Xu, Jasmin Christian Blanchette, Sophie Tourret
Cited by: 0

Abstract

We describe an Isabelle formalization of the finite tree-like model property of multi-modal logic, which considers families of modal operators. This property can be used to restrict structures that are models of satisfiable formulas to be "finite tree-like". We use Isabelle/HOL's HOLZF extension to prove the theorem independently of the type underlying the structures.

Fields of Study & Subjects

Logic Reasoning and Knowledge programming and type systems Formal Methods in Verification

Publication details

Journal / source
HAL
Publication date
1 February 2026
Language
EN
Document type
Preprint