Implementing the First-Order Logic of Here and There

TL;DR

This paper introduces automated theorem provers for the first-order logic of here and there (HT), utilizing a native sequent calculus and an embedding into intuitionistic logic, optimized for efficient proof search.

Contribution

It presents a novel approach combining sequent calculus and axiomatic embedding for HT, enabling more effective automated theorem proving in this logic.

Findings

Provers successfully tested on large benchmark set

Embedding improves proof search efficiency

Foundation for future HT prover development

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.