Solving Quantified Modal Logic Problems by Translation to Classical Logics

• URL: http://arxiv.org/abs/2212.09570v3
• Date: Mon, 29 Apr 2024 13:40:01 GMT
• Title: Solving Quantified Modal Logic Problems by Translation to Classical Logics
• Authors: Alexander Steen, Geoff Sutcliffe, Christoph Benzmüller,
• Abstract summary: The problems are translated to both typed first-order and higher-order logic using an embedding approach. The results from native modal logic ATP systems are considered, and compared with the results from the embedding approach.
• Score: 47.24825031148412
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: This article describes an evaluation of Automated Theorem Proving (ATP) systems on problems taken from the QMLTP library of first-order modal logic problems. Principally, the problems are translated to both typed first-order and higher-order logic in the TPTP language using an embedding approach, and solved using first-order resp. higher-order logic ATP systems and model finders. Additionally, the results from native modal logic ATP systems are considered, and compared with the results from the embedding approach. The findings are that the embedding process is reliable and successful when state-of-the-art ATP systems are used as backend reasoners, The first-order and higher-order embeddings perform similarly, native modal logic ATP systems have comparable performance to classical systems using the embedding for proving theorems, native modal logic ATP systems are outperformed by the embedding approach for disproving conjectures, and the embedding approach can cope with a wider range of modal logics than the native modal systems considered.

Related papers

• Do It for HER: First-Order Temporal Logic Reward Specification in Reinforcement Learning (Extended Version) [49.462399222747024]
  We propose a novel framework for the logical specification of non-Markovian rewards in Decision Processes (MDPs) with large state spaces.<n>Our approach leverages Linear Temporal Logic Modulo Theories over finite traces (LTLfMT)<n>We introduce a method based on reward machines and Hindsight Experience Replay (HER) to translate first-order logic specifications and address reward sparsity.
  arXiv  Detail & Related papers  (2026-02-05T22:11:28Z)
• Logic-Parametric Neuro-Symbolic NLI: Controlling Logical Formalisms for Verifiable LLM Reasoning [13.291627429657412]
  We propose a logic-parametric framework for neuro-symbolic natural language inference.<n>We embed a range of classical and non-classical formalisms into higher-order logic.<n>We show that logic-internal strategies can consistently improve performance.
  arXiv  Detail & Related papers  (2026-01-09T10:47:30Z)
• Beyond Correctness: Exposing LLM-generated Logical Flaws in Reasoning via Multi-step Automated Theorem Proving [11.24425572063955]
  Large Language Models (LLMs) have demonstrated impressive reasoning capabilities, leading to their adoption in high-stakes domains such as healthcare, law, and scientific research.<n>They often contain subtle logical errors masked by fluent language, posing significant risks for critical applications.<n>We present MATP, an evaluation framework for systematically verifying LLM reasoning via Multi-step Automatic Theorem Proving.
  arXiv  Detail & Related papers  (2025-12-29T14:48:15Z)
• LFC-DA: Logical Formula-Controlled Data Augmentation for Enhanced Logical Reasoning [3.553493344868413]
  LFC-DA is a symbolic-logic-controlled pipeline for complex logical data augmentation.<n>It maps logical text to propositional expressions, a compact rule library is compiled, and a bounded state-space search systematically discovers valid formulas.<n>Experiments on ReClor and LogiQA show significant improvements in the logical-reasoning accuracy of pretrained models.
  arXiv  Detail & Related papers  (2025-11-05T11:26:38Z)
• A Reduction of Input/Output Logics to SAT [51.82266520875928]
  Deontic logics are formalisms for reasoning over norms, obligations, permissions and prohibitions.<n>In this paper, an automation approach for I/O logics is presented that makes use of suitable reductions to propositional satisfiability problems.
  arXiv  Detail & Related papers  (2025-08-22T09:22:26Z)
• Speaking in Words, Thinking in Logic: A Dual-Process Framework in QA Systems [0.602276990341246]
  Text-JEPA is a framework for converting natural language into first-order logic (NL2FOL)<n>We show that Text-JEPA achieves competitive performance with significantly lower computational overhead compared to larger LLM-based systems.<n>Our findings highlight the potential of structured, interpretable reasoning frameworks for building efficient and explainable QA systems in specialized domains.
  arXiv  Detail & Related papers  (2025-07-28T03:00:35Z)
• CTRLS: Chain-of-Thought Reasoning via Latent State-Transition [57.51370433303236]
  Chain-of-thought (CoT) reasoning enables large language models to break down complex problems into interpretable intermediate steps.<n>We introduce groundingS, a framework that formulates CoT reasoning as a Markov decision process (MDP) with latent state transitions.<n>We show improvements in reasoning accuracy, diversity, and exploration efficiency across benchmark reasoning tasks.
  arXiv  Detail & Related papers  (2025-07-10T21:32:18Z)
• Automated Generation of Massive Reasonable Empirical Theorems by Forward Reasoning Based on Strong Relevant Logics -- A Solution to the Problem of LLM Pre-training Data Exhaustion [0.0]
  It is often said that the data used for the pre-training of large language models (LLMs) have been exhausted. This paper proposes a solution to the problem: Automated generation of massive reasonable empirical theorems by forward reasoning.
  arXiv  Detail & Related papers  (2024-12-16T23:18:17Z)
• Logic Agent: Enhancing Validity with Logic Rule Invocation [24.815341366820753]
  Chain-of-Thought prompting has emerged as a pivotal technique for augmenting the inferential capabilities of language models during reasoning tasks. This paper introduces the Logic Agent (LA), an agent-based framework aimed at enhancing the validity of reasoning processes in Large Language Models.
  arXiv  Detail & Related papers  (2024-04-28T10:02:28Z)
• LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers [60.009969929857704]
  Logical reasoning is an important task for artificial intelligence with potential impacts on science, mathematics, and society. In this work, we reformulating such tasks as modular neurosymbolic programming, which we call LINC. We observe significant performance gains on FOLIO and a balanced subset of ProofWriter for three different models in nearly all experimental conditions we evaluate.
  arXiv  Detail & Related papers  (2023-10-23T17:58:40Z)
• Modeling Hierarchical Reasoning Chains by Linking Discourse Units and Key Phrases for Reading Comprehension [80.99865844249106]
  We propose a holistic graph network (HGN) which deals with context at both discourse level and word level, as the basis for logical reasoning. Specifically, node-level and type-level relations, which can be interpreted as bridges in the reasoning process, are modeled by a hierarchical interaction mechanism.
  arXiv  Detail & Related papers  (2023-06-21T07:34:27Z)
• An optimized fuzzy logic model for proactive maintenance [0.0]
  The ITTFLM can generate outputs in 5ms, the results demonstrate that this model based on the Trapezoidal membership functions identifies the failure states with high accuracy. The ITTFLM was tested on fan data collected in real-time from a plant machine.
  arXiv  Detail & Related papers  (2022-12-24T15:49:46Z)
• 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)
• Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version) [72.38188258853155]
  This paper studies Linear Temporal Logic over Finite Traces (LTLf) proposition letters are replaced with first-order formulas interpreted over arbitrary theories. The resulting logic, called Satisfiability Modulo Theories (LTLfMT), is semi-decidable.
  arXiv  Detail & Related papers  (2022-04-28T17:57:33Z)
• Neuro-Symbolic Inductive Logic Programming with Logical Neural Networks [65.23508422635862]
  We propose learning rules with the recently proposed logical neural networks (LNN) Compared to others, LNNs offer strong connection to classical Boolean logic. Our experiments on standard benchmarking tasks confirm that LNN rules are highly interpretable.
  arXiv  Detail & Related papers  (2021-12-06T19:38:30Z)
• ORCHARD: A Benchmark For Measuring Systematic Generalization of Multi-Hierarchical Reasoning [8.004425059996963]
  We show that Transformer and LSTM models surprisingly fail in systematic generalization. We also show that with increased references between hierarchies, Transformer performs no better than random.
  arXiv  Detail & Related papers  (2021-11-28T03:11:37Z)
• Refining Labelled Systems for Modal and Constructive Logics with Applications [0.0]
  This thesis serves as a means of transforming the semantics of a modal and/or constructive logic into an 'economical' proof system. The refinement method connects two proof-theoretic paradigms: labelled and nested sequent calculi. The introduced refined labelled calculi will be used to provide the first proof-search algorithms for deontic STIT logics.
  arXiv  Detail & Related papers  (2021-07-30T08:27:15Z)
• 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)

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.