Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Implementing the First-Order Logic of Here and There

Jens Otten, Torsten Schaub

TL;DR

The paper addresses automated reasoning in Here and There ($HT$), an intermediate logic between classical and intuitionistic logics with a two-world Kripke semantics. It introduces four theorem provers: a native sequent-calculus prover (leanHaT) and three axiomatic-embedding provers (ileanSeP-HT, ileanTAP-HT, nanoCoP-i-HT) that embed HT into intuitionistic logic and leverage non-clausal proof calculi. Key contributions include optimized proof-search techniques (free variables, Skolemization, iterative deepening), restricted axiomatic embedding to prune search, and comprehensive benchmarking on the ILTP library showing strong performance of the non-translational approaches. The results demonstrate the viability of non-clausal, goal-oriented HT provers and establish a foundation for further development of practical, efficient HT reasoning tools, with future work on embedding completeness, benchmarks, and dedicated HT-proof technologies.

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.

Implementing the First-Order Logic of Here and There

TL;DR

The paper addresses automated reasoning in Here and There (), an intermediate logic between classical and intuitionistic logics with a two-world Kripke semantics. It introduces four theorem provers: a native sequent-calculus prover (leanHaT) and three axiomatic-embedding provers (ileanSeP-HT, ileanTAP-HT, nanoCoP-i-HT) that embed HT into intuitionistic logic and leverage non-clausal proof calculi. Key contributions include optimized proof-search techniques (free variables, Skolemization, iterative deepening), restricted axiomatic embedding to prune search, and comprehensive benchmarking on the ILTP library showing strong performance of the non-translational approaches. The results demonstrate the viability of non-clausal, goal-oriented HT provers and establish a foundation for further development of practical, efficient HT reasoning tools, with future work on embedding completeness, benchmarks, and dedicated HT-proof technologies.

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.
Paper Structure (17 sections, 4 figures, 3 tables)

This paper contains 17 sections, 4 figures, 3 tables.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Syntax and Semantics of HT
  4. Sequent Calculus for HT
  5. Axiomatic Embedding of HT
  6. Proof Search
  7. Proof Search in the Sequent Calculus LHT
  8. A Restricted Axiomatic Embedding of HT
  9. Intuitionistic Non-Clausal Connection Calculus
  10. The Implementations
  11. The Sequent Prover leanHa T
  12. The Axiomatic Sequent and Tableau Provers ileanSeP-HT and ilean T AP-HT
  13. The Axiomatic Connection Prover nanoCoP-i-HT
  14. Experimental Evaluation
  15. Benchmark Problems
  16. ...and 2 more sections

Figures (4)

  • Figure 1: The sequent calculus LHT for the first-order logic of HT.
  • Figure 2: The non-clausal connection calculus for intuitionistic logic.
  • Figure 3: The source code of the leanHa$\!$T sequent prover for the logic of HT.
  • Figure 4: Relation between intuitionistic logic, HT and classical logic.

Theorems & Definitions (8)

  • Definition 1: Sequent Calculus LHT for HT
  • Example 1
  • Definition 2: Axiomatic Embedding of HT
  • Example 2
  • Definition 3: Restricted Axiomatic Embedding of HT
  • Example 3
  • Example 4
  • Example 5: Sequent prover leanHaT