Kripke Semantics for Intersection Formulas
ACM Transactions on Computational Logic(2021)
摘要
AbstractWe propose a notion of the Kripke-style model for intersection logic. Using a game interpretation, we prove soundness and completeness of the proposed semantics. In other words, a formula is provable (a type is inhabited) if and only if it is forced in every model. As a by-product, we obtain another proof of normalization for the Barendregt–Coppo–Dezani intersection type assignment system.
更多查看译文
关键词
Intersection types, games in logic, Kripke models
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要