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.

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},
}