Extending a High-Performance Prover to Higher-Order Logic.

TACAS (2)(2023)

引用 1|浏览10
暂无评分
摘要
Most users of proof assistants want more proof automation. Some proof assistants discharge goals by translating them to first-order logic and invoking an efficient prover on them, but much is lost in translation. Instead, we propose to extend first-order provers with native support for higher-order features. Building on our extension of E to -free higher-order logic, we extend E to full higher-order logic. The result is the strongest prover on benchmarks exported from a proof assistant.
更多
查看译文
关键词
higher-order higher-order,logic,high-performance
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络