Kripke Semantics for Intersection Formulas
| Autor: | Andrej Dudenhefner, Paweł Urzyczyn |
|---|---|
| Rok vydání: | 2021 |
| Předmět: |
Discrete mathematics
Soundness Interpretation (logic) General Computer Science Logic Semantics (computer science) 010102 general mathematics 0102 computer and information sciences Type (model theory) 01 natural sciences Theoretical Computer Science Computational Mathematics Intersection 010201 computation theory & mathematics If and only if Completeness (logic) Kripke semantics 0101 mathematics Mathematics |
| Zdroj: | ACM Transactions on Computational Logic. 22:1-16 |
| ISSN: | 1557-945X 1529-3785 |
| DOI: | 10.1145/3453481 |
| Popis: | We 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|