cl-banner

Certification of Nonclausal Connection Tableaux Proofs

Michael Färber, Cezary Kaliszyk

28th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, LNCS 11714, pp. 21 – 38, 2019.

Abstract

Nonclausal connection tableaux calculi enable proof search without performing clausification. We give a translation of nonclausal connection proofs to Gentzen’s sequent calculus LK and compare it to an existing translation of clausal connection proofs. Furthermore, we implement the translation in the interactive theorem prover HOL Light, enabling certification of nonclausal connection proofs as well as a new, complementary automation technique in HOL Light.

 

  PDF |    doi:10.1007/978-3-030-29026-9_2  

BibTeX 

@inproceedings{mfck-tableaux19,
author = {Michael Färber and Cezary Kaliszyk},
title = {Certification of Nonclausal Connection Tableaux Proofs},
booktitle = {28th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2019)},
year = {2019},
series = {LNCS},
pages = {21--38},
url = {https://doi.org/10.1007/978-3-030-29026-9_2},
doi = {10.1007/978-3-030-29026-9_2},
publisher = {Springer},
volume = {11714},
editor = {Serenella Cerrito and Andrei Popescu},
}
Nach oben scrollen