A Structured Set of Higher-Order Problems

14 years 1 months ago
A Structured Set of Higher-Order Problems
Abstract. We present a set of problems that may support the development of calculi and theorem provers for classical higher-order logic. We propose to employ these test problems as quick and easy criteria preceding the formal soundness and completeness analysis of proof systems under development. Our set of problems is structured according to different technical issues and along different notions of semantics (including Henkin semantics) for higher-order logic. Many examples are either theorems or non-theorems depending on the choice of semantics. The examples can thus indicate the deductive strength of a proof system. 1 Motivation: Test Problems for Higher-Order Reasoning Systems Test problems are important for the practical implementation of theorem provers as well as for the preceding theoretical development of calculi, strategies and heuristics. If the test theorems can be proven (resp. the non-theorems cannot) then they ideally provide a strong indication for completeness (resp. s...
Christoph Benzmüller, Chad E. Brown
Added 25 Jun 2010
Updated 25 Jun 2010
Type Conference
Year 2005
Authors Christoph Benzmüller, Chad E. Brown
Comments (0)