Formalizing Cut Elimination of Coalgebraic Logics in Coq
In: Lecture Notes in Computer Science ISBN: 9783642405365 TABLEAUX; (2013)
Online
unknown
Zugriff:
In their work on coalgebraic logics, Pattinson and Schroder prove soundness, completeness and cut elimination in a generic sequent calculus for propositional multi-modal logics [1]. The present paper reports on a formalization of Pattinson’s and Schroder’s work in the proof assistant Coq that provides machine-checked proofs for soundness, completeness and cut elimination of their calculus. The formalization exploits dependent types to obtain a very concise deep embedding for formulas and proofs. The work presented here can be used to verify cut elimination theorems for different modal logics with considerably less effort in the future.
Titel: |
Formalizing Cut Elimination of Coalgebraic Logics in Coq
|
---|---|
Autor/in / Beteiligte Person: | Tews, Hendrik |
Link: | |
Quelle: | Lecture Notes in Computer Science ISBN: 9783642405365 TABLEAUX; (2013) |
Veröffentlichung: | Springer Berlin Heidelberg, 2013 |
Medientyp: | unknown |
ISBN: | 978-3-642-40536-5 (print) |
DOI: | 10.1007/978-3-642-40537-2_22 |
Schlagwort: |
|
Sonstiges: |
|