LFSC for SMT Proofs: Work in Progress

Second International Workshop on Proof Exchange for Theorem Proving

Aaron Stump ; Andrew Reynolds ; Cesare Tinelli ; Austin Laugesen

Others  :  http://ceur-ws.org/Vol-878/paper1.pdf
PID  :  43479

来源: CEUR

【 摘 要 】

This paper presents work in progress on a new version, for public release, of the Logical Framework with Side Conditions (LFSC), previously proposed as a proof meta-format for SMT solvers and other proof-producing systems. The paper reviews the type-theoretic approach of LFSC, presents a new input syntax which hides the type-theoretic details for better accessibility, and discusses work in progress on formalizing and implementing a