Order-Sorted Intensional Logic: Expressing Subtyping Polymorphism with Typing Assertions and Quantification over Concepts

• URL: http://arxiv.org/abs/2502.09224v1
• Date: Thu, 13 Feb 2025 11:51:22 GMT
• Title: Order-Sorted Intensional Logic: Expressing Subtyping Polymorphism with Typing Assertions and Quantification over Concepts
• Authors: Đorđe Marković, Marc Denecker,
• Abstract summary: Subtyping, also known as subtype polymorphism, is a concept extensively studied in programming language theory.<n>In this paper, we explore the capability of order-sorted logic for utilizing these ideas in the context of Knowledge Representation.
• Score: 1.104960878651584
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: 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.

Related papers

• Logic-Based Artificial Intelligence Algorithms Supporting Categorical Semantics [0.0]
  We develop forward chaining and normal form algorithms for reasoning about objects in cartesian categories with the rules for Horn logic. We also adapt first-order unification to support multi-sorted theories, contexts, and fragments of first-order logic.
  arXiv  Detail & Related papers  (2025-04-27T18:02:02Z)
• Homomorphic Encryption of Intuitionistic Logic Proofs and Functional Programs: A Categorical Approach Inspired by Composite-Order Bilinear Groups [0.0]
  We present a conceptual framework for extending homomorphic encryption beyond arithmetic or Boolean operations into the domain of intuitionistic logic. We outline strategies for making the approach potentially efficient, including software optimizations and hardware acceleration.
  arXiv  Detail & Related papers  (2025-02-26T10:10:10Z)
• A Semantic Parsing Algorithm to Solve Linear Ordering Problems [2.23890712706409]
  We develop an algorithm to semantically parse linear ordering problems.<n>Our method takes as input a number of premises and candidate statements.<n>We then utilize constraint logic programming to infer the truth of proposed statements about the ordering.
  arXiv  Detail & Related papers  (2025-02-12T13:58:42Z)
• An Encoding of Abstract Dialectical Frameworks into Higher-Order Logic [57.24311218570012]
  This approach allows for the computer-assisted analysis of abstract dialectical frameworks. Exemplary applications include the formal analysis and verification of meta-theoretical properties.
  arXiv  Detail & Related papers  (2023-12-08T09:32:26Z)
• Description Logics Go Second-Order -- Extending EL with Universally Quantified Concepts [0.0]
  We focus on the extension of description logic $mathcalEL$. We show that for a useful fragment of the extension, the conclusions entailed by the different semantics coincide. For a slightly smaller, but still useful, fragment, we were also able to show decidability of the extension.
  arXiv  Detail & Related papers  (2023-08-16T09:37:38Z)
• APOLLO: A Simple Approach for Adaptive Pretraining of Language Models for Logical Reasoning [73.3035118224719]
  We propose APOLLO, an adaptively pretrained language model that has improved logical reasoning abilities. APOLLO performs comparably on ReClor and outperforms baselines on LogiQA.
  arXiv  Detail & Related papers  (2022-12-19T07:40:02Z)
• Benchmarking Language Models for Code Syntax Understanding [79.11525961219591]
  Pre-trained language models have demonstrated impressive performance in both natural language processing and program understanding. In this work, we perform the first thorough benchmarking of the state-of-the-art pre-trained models for identifying the syntactic structures of programs. Our findings point out key limitations of existing pre-training methods for programming languages, and suggest the importance of modeling code syntactic structures.
  arXiv  Detail & Related papers  (2022-10-26T04:47:18Z)
• Join-Chain Network: A Logical Reasoning View of the Multi-head Attention in Transformer [59.73454783958702]
  We propose a symbolic reasoning architecture that chains many join operators together to model output logical expressions. In particular, we demonstrate that such an ensemble of join-chains can express a broad subset of ''tree-structured'' first-order logical expressions, named FOET. We find that the widely used multi-head self-attention module in transformer can be understood as a special neural operator that implements the union bound of the join operator in probabilistic predicate space.
  arXiv  Detail & Related papers  (2022-10-06T07:39:58Z)
• Discourse-Aware Graph Networks for Textual Logical Reasoning [142.0097357999134]
  Passage-level logical relations represent entailment or contradiction between propositional units (e.g., a concluding sentence) We propose logic structural-constraint modeling to solve the logical reasoning QA and introduce discourse-aware graph networks (DAGNs) The networks first construct logic graphs leveraging in-line discourse connectives and generic logic theories, then learn logic representations by end-to-end evolving the logic relations with an edge-reasoning mechanism and updating the graph features.
  arXiv  Detail & Related papers  (2022-07-04T14:38:49Z)
• A unified logical framework for explanations in classifier systems [10.256904719009471]
  We present a modal language of a ceteris paribus nature which supports reasoning about binary input classifiers and their properties. We study a family of models, axiomatize it as two proof systems regarding the cardinality of the language and show completeness of our axiomatics. We leverage the language to formalize counterfactual conditional as well as a variety of notions of explanation including abductive, contrastive and counterfactual explanations.
  arXiv  Detail & Related papers  (2021-05-30T07:49:56Z)
• Hierarchical Poset Decoding for Compositional Generalization in Language [52.13611501363484]
  We formalize human language understanding as a structured prediction task where the output is a partially ordered set (poset) Current encoder-decoder architectures do not take the poset structure of semantics into account properly. We propose a novel hierarchical poset decoding paradigm for compositional generalization in language.
  arXiv  Detail & Related papers  (2020-10-15T14:34:26Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.