Certification of Prefixed Tableau Proofs for Modal Logic

Different theorem provers tend to produce proof objects in different formats and this is especially the case for modal logics, where several deductive formalisms (and provers based on them) have been presented. This work falls within the general project of establishing a common specification languag...

Full description

Bibliographic Details
Main Authors: Tomer Libal, Marco Volpe
Format: Article
Language:English
Published: Open Publishing Association 2016-09-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1609.04100v1