Faithful Logic Embeddings in HOL -- A recipe to have it all: deep and shallow, automated and interactive, heavy and light, proofs and counterexamples, meta and object level

• URL: http://arxiv.org/abs/2502.19311v1
• Date: Wed, 26 Feb 2025 17:08:07 GMT
• Title: Faithful Logic Embeddings in HOL -- A recipe to have it all: deep and shallow, automated and interactive, heavy and light, proofs and counterexamples, meta and object level
• Authors: Christoph Benzmüller,
• Abstract summary: This paper presents a recipe for the simultaneous deployment of different forms of deep and shallow embeddings in classical higher-order logic.<n>The approach is fruitful for logic education, research and application.
• 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 automated reasoning tools in recent years. This paper presents a recipe for the simultaneous deployment of different forms of deep and shallow embeddings in classical higher-order logic, enabling not only flexible interactive and automated theorem proving and counterexample finding at meta and object level, but also automated faithfulness proofs between the logic embeddings. The approach, which is fruitful for logic education, research and application, is deliberately illustrated here using simple propositional modal logic. However, the work presented is conceptual in nature and not limited to such a simple logic context.

Related papers

• 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)
• 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.