Implementing the First-Order Logic of Here and There
By: Jens Otten, Torsten Schaub
Potential Business Impact:
Helps computers prove tricky math problems faster.
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.
Similar Papers
Hammering Higher Order Set Theory
Logic in Computer Science
Makes math proofs faster and easier for computers.
Craig Interpolation for HT with a Variation of Mints' Sequent System
Logic in Computer Science
Helps computers understand tricky logic puzzles.
An abstract fixed-point theorem for Horn formula equations
Logic in Computer Science
Proves computer programs are correct and safe.