A Verified Proof of Craig Interpolation for Basic Modal Logic via Tableaux in Lean

Authors

B.R.M. Gattinger

Date (dd-mm-yyyy)

2022

Title

A Verified Proof of Craig Interpolation for Basic Modal Logic via Tableaux in Lean

Publication Year

2022

Number of pages

Document type

Paper

Abstract

We present a formalisation of tableaux for Basic Modal Logic (K) in the Lean proof assistant. We cover soundness, completeness, and Craig Interpolation via tableaux.
In the future we aim to extend this proof from Basic Modal Logic to Propositional Dynamic Logic (PDL). Specifically, this is a first step towards a formal verification of Borzechowski (1988) which claims that PDL has Craig Interpolation.

Permalink

https://hdl.handle.net/11245.1/c3c3745a-9e56-495d-8b08-1f1a08e897fa