On Herbrand's Theorem for Intuitionistic Logic

Abstract In this paper we reduce the question of validity of a first-order intuitionistic formula without equality to generating ground instances of this formula and then checking whether the instances are deducible in a propositional intuitionistic tableaux calculus, provided that the propositional proof is compatible with the way how the instances were generated. This result can be seen as a form of the Herbrand theorem, and so it provides grounds for further theoretical investigation of computer-oriented intuitionistic calculi.

Authors

• Alexander V. Lyaletski
• Boris Konev

Keywords

No keywords are indexed for this paper.