用带保护符的有序排序逻辑表达类型子关系，提升知识表示的灵活性
Order-Sorted Intensional Logic: Expressing Subtyping Polymorphism with Typing Assertions and Quantification over Concepts
- 引入保护符标注类型信息，解决传统逻辑无法约束项类型的问题
- 结合内涵逻辑实现对概念的量化，支持类型层次的抽象表达
- 适合研究类型系统与知识表示交叉领域的学者使用
子类型（又称子类型多态）是编程语言理论中广泛研究的概念，描述数据类型间的可替换关系。该性质保证为超类型设计的程序仍能兼容其子类型。本文探讨有序排序逻辑在知识表示中的应用潜力。我们发现该逻辑存在两个根本局限：一是无法处理非逻辑符号的概念而非值；二是缺乏约束项类型的语言构造。为此，我们提出受保护的有序排序内涵逻辑，其中保护符用于标注类型信息，内涵逻辑则支持对概念的量化。
原文摘要 · Abstract (English)
Subtyping, also known as subtype polymorphism, is a concept extensively studied in programming language theory, delineating the substitutability relation among datatypes. This property ensures that programs designed for supertype objects remain compatible with their subtypes. In this paper, we explore the capability of order-sorted logic for utilizing these ideas in the context of Knowledge Representation. We recognize two fundamental limitations: First, the inability of this logic to address the concept rather than the value of non-logical symbols, and second, the lack of language constructs for constraining the type of terms. Consequently, we propose guarded order-sorted intensional logic, where guards are language constructs for annotating typing information and intensional logic provides support for quantification over concepts.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。