An Extensible Logic Embedding Tool for Lightweight Non-Classical
Reasoning
- URL: http://arxiv.org/abs/2203.12352v1
- Date: Wed, 23 Mar 2022 12:08:51 GMT
- Title: An Extensible Logic Embedding Tool for Lightweight Non-Classical
Reasoning
- Authors: Alexander Steen
- Abstract summary: 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.
- Score: 91.3755431537592
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: The logic embedding tool provides a procedural encoding for non-classical
reasoning problems into classical higher-order logic. It is extensible and can
support an increasing number of different non-classical logics as reasoning
targets. When used as a pre-processor or library for higher-order theorem
provers, the tool admits off-the-shelf automation for logics for which
otherwise few to none provers are currently available.
Related papers
- Improving Complex Reasoning over Knowledge Graph with Logic-Aware Curriculum Tuning [89.89857766491475]
We propose a complex reasoning schema over KG upon large language models (LLMs)
We augment the arbitrary first-order logical queries via binary tree decomposition to stimulate the reasoning capability of LLMs.
Experiments across widely used datasets demonstrate that LACT has substantial improvements(brings an average +5.5% MRR score) over advanced methods.
arXiv Detail & Related papers (2024-05-02T18:12:08Z) - 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) - Automated reasoning support for Standpoint-OWL 2 [1.160208922584163]
The tool works by translating the standpoint-enhanced version of the description logic SROIQ to its plain (i.e. classical) version.
Existing reasoners can then be directly used to provide automated support for reasoning about diverse standpoints.
arXiv Detail & Related papers (2023-04-30T19:50:14Z) - 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) - 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) - 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) - Extending Automated Deduction for Commonsense Reasoning [0.0]
The paper argues that the methods and algorithms used by automated reasoners for classical first-order logic can be extended towards commonsense reasoning.
The proposed extensions mostly rely on ordinary proof trees and are devised to handle commonsense knowledge bases containing inconsistencies, default rules, operating on topics, relevance, confidence and similarity measures.
We claim that machine learning is best suited for the construction of commonsense knowledge bases while the extended logic-based methods would be well-suited for actually answering queries from these knowledge bases.
arXiv Detail & Related papers (2020-03-29T23:17:16Z)
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.