Facets of the PIE Environment for Proving, Interpolating and Eliminating on the Basis of First-Order Logic

• URL: http://arxiv.org/abs/2002.10892v1
• Date: Mon, 24 Feb 2020 16:09:10 GMT
• Title: Facets of the PIE Environment for Proving, Interpolating and Eliminating on the Basis of First-Order Logic
• Authors: Christoph Wernhard
• Abstract summary: PIE is a Prolog-embedded environment for automated reasoning on the basis of first-order logic. It supports a workflow based on documents that intersperse macro definitions, invocations of reasoners, andformatted natural language text.
• Score: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: PIE is a Prolog-embedded environment for automated reasoning on the basis of first-order logic. Its main focus is on formulas, as constituents of complex formalizations that are structured through formula macros, and as outputs of reasoning tasks such as second-order quantifier elimination and Craig interpolation. It supports a workflow based on documents that intersperse macro definitions, invocations of reasoners, and LaTeX-formatted natural language text. Starting from various examples, the paper discusses features and application possibilities of PIE along with current limitations and issues for future research.

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)
• Multi-Agent Procedural Graph Extraction with Structural and Logical Refinement [66.51979814832332]
  model formulates procedural graph extraction as a multi-round reasoning process with dedicated structural and logical refinement.<n>Experiments demonstrate that model achieves substantial improvements in both structural correctness and logical consistency over strong baselines.
  arXiv  Detail & Related papers  (2026-01-27T04:00:48Z)
• Eliminating Agentic Workflow for Introduction Generation with Parametric Stage Tokens [3.6588919376939733]
  We propose eliminating external agentic to write research introductions.<n>Instead, we parameterize their logical structure into a large language model.<n>This allows the generation of a complete introduction in a single inference.
  arXiv  Detail & Related papers  (2025-12-28T12:51:36Z)
• From Language to Logic: A Bi-Level Framework for Structured Reasoning [6.075080928704587]
  Structured reasoning over natural language inputs remains a core challenge in artificial intelligence.<n>We propose a novel framework that maps language to logic through a two-stage process: high-level task abstraction and low-level logic generation.<n>Our approach significantly outperforms existing baselines in accuracy, with accuracy gains reaching as high as 40%.
  arXiv  Detail & Related papers  (2025-07-11T11:24:09Z)
• A Semantic Parsing Algorithm to Solve Linear Ordering Problems [2.23890712706409]
  We develop an algorithm to semantically parse linear ordering problems. Our method takes as input a number of premises and candidate statements. 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)
• H-STAR: LLM-driven Hybrid SQL-Text Adaptive Reasoning on Tables [56.73919743039263]
  This paper introduces a novel algorithm that integrates both symbolic and semantic (textual) approaches in a two-stage process to address limitations. Our experiments demonstrate that H-STAR significantly outperforms state-of-the-art methods across three question-answering (QA) and fact-verification datasets.
  arXiv  Detail & Related papers  (2024-06-29T21:24:19Z)
• 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)
• Physics of Language Models: Part 1, Learning Hierarchical Language Structures [51.68385617116854]
  Transformer-based language models are effective but complex, and understanding their inner workings and reasoning mechanisms is a significant challenge.<n>We introduce a family of synthetic CFGs that produce hierarchical rules, capable of generating lengthy sentences.<n>We demonstrate that generative models like GPT can accurately learn and reason over CFG-defined hierarchies and generate sentences based on it.
  arXiv  Detail & Related papers  (2023-05-23T04:28:16Z)
• Query Structure Modeling for Inductive Logical Reasoning Over Knowledge Graphs [67.043747188954]
  We propose a structure-modeled textual encoding framework for inductive logical reasoning over KGs. It encodes linearized query structures and entities using pre-trained language models to find answers. We conduct experiments on two inductive logical reasoning datasets and three transductive datasets.
  arXiv  Detail & Related papers  (2023-05-23T01:25:29Z)
• HPE:Answering Complex Questions over Text by Hybrid Question Parsing and Execution [92.69684305578957]
  We propose a framework of question parsing and execution on textual QA. The proposed framework can be viewed as a top-down question parsing followed by a bottom-up answer backtracking. Our experiments on MuSiQue, 2WikiQA, HotpotQA, and NQ show that the proposed parsing and hybrid execution framework outperforms existing approaches in supervised, few-shot, and zero-shot settings.
  arXiv  Detail & Related papers  (2023-05-12T22:37:06Z)
• MURMUR: Modular Multi-Step Reasoning for Semi-Structured Data-to-Text Generation [102.20036684996248]
  We propose MURMUR, a neuro-symbolic modular approach to text generation from semi-structured data with multi-step reasoning. We conduct experiments on two data-to-text generation tasks like WebNLG and LogicNLG.
  arXiv  Detail & Related papers  (2022-12-16T17:36:23Z)
• Guiding the PLMs with Semantic Anchors as Intermediate Supervision: Towards Interpretable Semantic Parsing [57.11806632758607]
  We propose to incorporate the current pretrained language models with a hierarchical decoder network. By taking the first-principle structures as the semantic anchors, we propose two novel intermediate supervision tasks. We conduct intensive experiments on several semantic parsing benchmarks and demonstrate that our approach can consistently outperform the baselines.
  arXiv  Detail & Related papers  (2022-10-04T07:27:29Z)
• Applying Second-Order Quantifier Elimination in Inspecting G\"odel's Ontological Proof [0.0]
  Formula macros are used to structure complex formulas and tasks. G"odel's ontological proof and variations are formalized and analyzed with automated tools.
  arXiv  Detail & Related papers  (2021-10-21T12:50:23Z)
• Structural Decompositions of Epistemic Logic Programs [29.23726484912091]
  Epistemic logic programs (ELPs) are a popular generalization of standard Answer Set Programming (ASP) We show that central problems can be solved in linear time for ELPs exhibiting structural properties in terms of bounded treewidth. We also provide a full dynamic programming algorithm that adheres to these bounds.
  arXiv  Detail & Related papers  (2020-01-13T13:16:13Z)

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.