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.
Cite
CITATION STYLE
Färber, M., & Kaliszyk, C. (2019). Certification of Nonclausal Connection Tableaux Proofs. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 11714 LNAI, pp. 21–38). Springer. https://doi.org/10.1007/978-3-030-29026-9_2
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
