Faithful Logic Embeddings in HOL -- Deep and Shallow

• URL: http://arxiv.org/abs/2502.19311v3
• Date: Sun, 01 Jun 2025 11:17:37 GMT
• Title: Faithful Logic Embeddings in HOL -- Deep and Shallow
• Authors: Christoph Benzmüller,
• Abstract summary: This paper presents a method for the simultaneous deployment of deep and shallow embeddings of various degrees in classical higher-order logic.<n>The method is beneficial for logic education, research and application and is illustrated here using a simple propositional modal logic.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Deep and shallow embeddings of non-classical logics in classical higher-order logic have been explored, implemented, and used in various reasoning tools in recent years. This paper presents a method for the simultaneous deployment of deep and shallow embeddings of various degrees in classical higher-order logic. This enables flexible, interactive and automated theorem proving and counterexample finding at meta and object level, as well as automated faithfulness proofs between these logic embeddings. The method is beneficial for logic education, research and application and is illustrated here using a simple propositional modal logic. However, this approach is conceptual in nature and not limited to this simple logic context.

Related papers

• On the Logical Content of Logic Programs [0.0]
  This paper introduces a novel perspective on Logic programming (LP) by defining a support'' relation that explicates what a program knows''<n>Results are formalized using the idea of base-extension semantics within proof-theoretic semantics.<n>Our approach offers new insights into the logical foundations of LP and has potential applications in knowledge representation, automated reasoning, and formal verification.
  arXiv  Detail & Related papers  (2025-03-07T11:58:08Z)
• Logical Modalities within the European AI Act: An Analysis [0.0]
  The paper presents a comprehensive analysis of the European AI Act in terms of its logical modalities. It aims to prepare its formal representation within the logic-pluralistic Knowledge Engineering Framework and methodology. LogiKEy develops computational tools for normative reasoning based on formal methods.
  arXiv  Detail & Related papers  (2025-01-31T13:15:33Z)
• Aristotle: Mastering Logical Reasoning with A Logic-Complete Decompose-Search-Resolve Framework [93.59256448185954]
  We propose a logic-complete reasoning framework, Aristotle, with three key components: Logical Decomposer, Logical Search Router, and Logical Resolver. In our framework, symbolic expressions and logical rules are comprehensively integrated into the entire reasoning process. The experimental results on several datasets demonstrate that Aristotle consistently outperforms state-of-the-art reasoning frameworks in both accuracy and efficiency.
  arXiv  Detail & Related papers  (2024-12-22T10:14:09Z)
• 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)
• LOGICSEG: Parsing Visual Semantics with Neural Logic Learning and Reasoning [73.98142349171552]
  LOGICSEG is a holistic visual semantic that integrates neural inductive learning and logic reasoning with both rich data and symbolic knowledge. During fuzzy logic-based continuous relaxation, logical formulae are grounded onto data and neural computational graphs, hence enabling logic-induced network training. These designs together make LOGICSEG a general and compact neural-logic machine that is readily integrated into existing segmentation models.
  arXiv  Detail & Related papers  (2023-09-24T05:43:19Z)
• Towards Invertible Semantic-Preserving Embeddings of Logical Formulae [1.0152838128195467]
  Learning and optimising logic requirements and rules has always been an important problem in Artificial Intelligence. Current methods are able to construct effective semantic-preserving embeddings via kernel methods, but the map they define is not invertible. In this work we address this problem, learning how to invert such an embedding leveraging deep architectures based on the Graph Variational Autoencoder framework.
  arXiv  Detail & Related papers  (2023-05-03T10:49:01Z)
• 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)
• An Extensible Logic Embedding Tool for Lightweight Non-Classical Reasoning [91.3755431537592]
  The logic embedding tool provides a procedural encoding for non-classical reasoning problems into classical higher-order logic. It can support an increasing number of different non-classical logics as reasoning targets.
  arXiv  Detail & Related papers  (2022-03-23T12:08:51Z)
• Automated Reasoning in Non-classical Logics in the TPTP World [58.720142291102135]
  The TPTP World currently supports only classical logics. Similar standards for non-classical logic reasoning do not exist. This paper describes the latest extension of the TPTP World, which provides languages and infrastructure for reasoning in non-classical logics.
  arXiv  Detail & Related papers  (2022-02-20T15:29:30Z)
• Modeling and Automating Public Announcement Logic with Relativized Common Knowledge as a Fragment of HOL in LogiKEy [0.0]
  This article presents a semantical embedding for public announcement logic with relativized common knowledge. It enables the first-time automation of this logic with off-the-shelf theorem provers for classical higher-order logic. The work constitutes an important addition to the pluralist LogiKEy knowledge engineering methodology.
  arXiv  Detail & Related papers  (2021-11-02T15:14:52Z)
• A Formalisation of Abstract Argumentation in Higher-Order Logic [77.34726150561087]
  We present an approach for representing abstract argumentation frameworks based on an encoding into classical higher-order logic. This provides a uniform framework for computer-assisted assessment of abstract argumentation frameworks using interactive and automated reasoning tools.
  arXiv  Detail & Related papers  (2021-10-18T10:45:59Z)
• On syntactically similar logic programs and sequential decompositions [0.0]
  Rule-based reasoning is an essential part of human intelligence prominently formalized in artificial intelligence research via logic programs. Describing complex objects as the composition of elementary ones is a common strategy in computer science and science in general. We show how similarity can be used to answer queries across different domains via a one-step reduction.
  arXiv  Detail & Related papers  (2021-09-11T15:22:17Z)
• Logic-Driven Context Extension and Data Augmentation for Logical Reasoning of Text [65.24325614642223]
  We propose to understand logical symbols and expressions in the text to arrive at the answer. Based on such logical information, we put forward a context extension framework and a data augmentation algorithm. Our method achieves the state-of-the-art performance, and both logic-driven context extension framework and data augmentation algorithm can help improve the accuracy.
  arXiv  Detail & Related papers  (2021-05-08T10:09:36Z)
• Public Announcement Logic in HOL [0.0]
  shallow semantical embedding for public announcement logic with relativized common knowledge is presented. This embedding enables the first-time automation of this logic with off-the-shelf theorem provers for classical higher-order logic.
  arXiv  Detail & Related papers  (2020-10-02T06:46:02Z)
• Higher-order Logic as Lingua Franca -- Integrating Argumentative Discourse and Deep Logical Analysis [0.0]
  We present an approach towards the deep, pluralistic logical analysis of argumentative discourse. We use state-of-the-art automated reasoning technology for classical higher-order logic.
  arXiv  Detail & Related papers  (2020-07-02T11:07:53Z)

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.