LOGIC: A Coq Library for Logics.

Yichen Tao,Qinxiang Cao

SETTA(2022)

引用 0|浏览4
暂无评分
摘要
LOGIC is a Coq library for formalizing logic studies, concerning both logics' applications and logics themselves (meta-theories). For applications, users can port derived rules and efficient proof automation tactics from LOGIC to their own program-logic-based verification projects. For meta-theories, users can easily formalize a standard soundness proof or a Henkin-style completeness proof for logics like classical/intuitionistic propositional logic, separation logic and modal logic with LOGIC's help. In this paper, we present how compositional and portable proof engineering is possible in LOGIC.
更多
查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络