Implementing the First-Order Logic of Here and There

Jens Otten, Torsten Schaub

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…