Implementing the First-Order Logic of Here and There

• URL: http://arxiv.org/abs/2601.03848v1
• Date: Wed, 07 Jan 2026 12:08:15 GMT
• Title: Implementing the First-Order Logic of Here and There
• Authors: Jens Otten, Torsten Schaub,
• Abstract summary: We present automated theorem provers for the first-order logic of here and there (HT)<n>They are based on a native sequent calculus for the logic of HT and an axiomatic embedding of the logic of HT into intuitionistic logic.<n>All provers are evaluated on a large benchmark set of first-order formulas.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: We present automated theorem provers for the first-order logic of here and there (HT). They are based on a native sequent calculus for the logic of HT and an axiomatic embedding of the logic of HT into intuitionistic logic. The analytic proof search in the sequent calculus is optimized by using free variables and skolemization. The embedding is used in combination with sequent, tableau and connection calculi for intuitionistic first-order logic. All provers are evaluated on a large benchmark set of first-order formulas, providing a foundation for the development of more efficient HT provers.

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-Based Artificial Intelligence Algorithms Supporting Categorical Semantics [0.0]
  We develop forward chaining and normal form algorithms for reasoning about objects in cartesian categories with the rules for Horn logic.<n>We also adapt first-order unification to support multi-sorted theories, contexts, and fragments of first-order logic.
  arXiv  Detail & Related papers  (2025-04-27T18:02:02Z)
• FSLI: An Interpretable Formal Semantic System for One-Dimensional Ordering Inference [0.9048611509540079]
  We develop a system for solving logical deduction one-dimensional ordering problems.<n>It transforms natural language premises and candidate statements into first-order logic.<n>It achieves 100% accuracy on BIGbench's logical deduction task and 88% on a syntactically simplified subset of AR-LSAT.
  arXiv  Detail & Related papers  (2025-02-12T13:58:42Z)
• Improving Complex Reasoning over Knowledge Graph with Logic-Aware Curriculum Tuning [89.89857766491475]
  We propose a curriculum-based logical-aware instruction tuning framework, named LACT.<n>Specifically, we augment the arbitrary first-order logical queries via binary tree decomposition.<n> Experiments across widely used datasets demonstrate that LACT has substantial improvements(brings an average +5.5% MRR score) over advanced methods, achieving the new state-of-the-art.
  arXiv  Detail & Related papers  (2024-05-02T18:12:08Z)
• Proving Theorems using Incremental Learning and Hindsight Experience Replay [45.277067974919106]
  We propose a general incremental learning algorithm for training domain specific provers for first-order logic without equality. We adapt hindsight experience replay to theorem proving, so as to be able to learn even when no proof can be found. We show that provers trained this way can match and sometimes surpass state-of-the-art traditional provers on the TPTP dataset.
  arXiv  Detail & Related papers  (2021-12-20T16:40:26Z)
• 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)
• 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)
• Superposition with Lambdas [59.87497175616048]
  We design a superposition calculus for a clausal fragment of extensional polymorphic higher-order logic that includes anonymous functions but excludes Booleans. The inference rules work on $betaeta$-equivalence classes of $lambda$-terms and rely on higher-order unification to achieve refutational completeness.
  arXiv  Detail & Related papers  (2021-01-31T13:53:17Z)
• RNNLogic: Learning Logic Rules for Reasoning on Knowledge Graphs [91.71504177786792]
  This paper studies learning logic rules for reasoning on knowledge graphs. Logic rules provide interpretable explanations when used for prediction as well as being able to generalize to other tasks. Existing methods either suffer from the problem of searching in a large search space or ineffective optimization due to sparse rewards.
  arXiv  Detail & Related papers  (2020-10-08T14:47:02Z)
• Superposition for Lambda-Free Higher-Order Logic [62.997667081978825]
  We introduce refutationally complete superposition calculi for intentional and extensional clausal $lambda$-free higher-order logic. The calculi are parameterized by a term order that need not be fully monotonic, making it possible to employ the $lambda$-free higher-order lexicographic path and Knuth-Bendix orders.
  arXiv  Detail & Related papers  (2020-05-05T12:10:21Z)
• An Experimental Study of Formula Embeddings for Automated Theorem Proving in First-Order Logic [13.633012068936894]
  We study and experimentally compare pattern-based embeddings that are applied in current systems with popular graph-based encodings. Our experiments show that the advantages of simpler encoding schemes in terms of runtime are outdone by more complex graph-based embeddings.
  arXiv  Detail & Related papers  (2020-02-02T16:07:15Z)

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.