Craig's Interpolation Theorem formalised and mechanised in Isabelle/HOL

Simple item page
dc.creatorRidge, Tom
dc.date2006-07-12
dc.date.accessioned2026-07-07T07:16:19Z
dc.date.available2026-07-07T07:16:19Z
dc.descriptionWe formalise and mechanise a construtive, proof theoretic proof of Craig's Interpolation Theorem in Isabelle/HOL. We give all the definitions and lemma statements both formally and informally. We also transcribe informally the formal proofs. We detail the main features of our mechanisation, such as the formalisation of binding for first order formulae. We also give some applications of Craig's Interpolation Theorem.
dc.identifierhttps://arxiv.org/abs/cs/0607058
dc.identifierhttp://arxiv.org/abs/cs/0607058
dc.identifier.urihttp://salesiana.dossiersoluciones.com/handle/123456789/113550
dc.subjectLogic in Computer Science
dc.titleCraig's Interpolation Theorem formalised and mechanised in Isabelle/HOL
dc.typetext

Files

Collections

arXiv