zbMATH — the first resource for mathematics

Certification of nonclausal connection tableaux proofs. (English) Zbl 1435.03033
Cerrito, Serenella (ed.) et al., Automated reasoning with analytic tableaux and related methods. 28th international conference, TABLEAUX 2019, London, UK, September 3–5, 2019. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11714, 21-38 (2019).
Summary: 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.
For the entire collection see [Zbl 1428.68011].
Reviewer: Reviewer (Berlin)
03B35 Mechanization of proofs and logical operations
03F07 Structure of proofs
68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
Full Text: DOI