Certification of Nonclausal Connection Tableaux Proofs.
TABLEAUX(2019)
摘要
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.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络