LFSC for SMT Proofs: Work in Progress

LFSC for SMT Proofs: Work in Progress
复制标题

用于 SMT 打样的 LFSC：正在进行中

DOI：
--
复制
发表时间：
2012
期刊：
International Workshop on Proof Exchange for Theorem Proving
影响因子：
--
通讯作者：
Ruoyu Zhang
Ruoyu Zhang
中科院分区：
--
文献类型：
--
作者：
Aaron Stump;Andrew Reynolds;C. Tinelli;Austin Laugesen;H. Eades;C. Oliver;Ruoyu Zhang

文献摘要

被引文献

相似文献

本文介绍了正在公开发布的带有附带条件的逻辑框架 (LFSC) 新版本的进展情况，该框架之前曾被提议作为 SMT 求解器和其他证明生成系统的证明元格式。本文回顾了 LFSC 的类型论方法，提出了一种新的输入语法，该语法隐藏了类型论细节以提高可访问性，并讨论了形式化和实现修订后的核心语言方面正在进行的工作。
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 revised core language.