2 papers
cs.LO2026
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…
cs.SC2019
Converting ALC Connection Proofs into ALC Sequents
Eunice Palmeira, Fred Freitas, Jens Otten
The connection method has earned good reputation in the area of automated theorem proving, due to its simplicity, efficiency and rational use of memory. This method has been applie…