Making Higher-Order Superposition Work

AUTOMATED DEDUCTION, CADE 28(2022)

引用 19|浏览21
暂无评分
摘要
Superposition is among the most successful calculi for first-order logic. Its extension to higher-order logic introduces new challenges such as infinitely branching inference rules, new possibilities such as reasoning about Booleans, and the need to curb the explosion of specific higher-order rules. We describe techniques that address these issues and extensively evaluate their implementation in the Zipperposition theorem prover. Largely thanks to their use, Zipperposition won the higher-order division of the CASC-J10 competition.
更多
查看译文
关键词
Higher-order theorem proving,Heuristics,Zipperposition,Superposition
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要