System description KRHyper.pdf

System Description: KRHyper Christoph Wernhard 14/2003 Fachberichte INFORMATIK Universita?t Koblenz-Landau Institut fu?r Informatik, Universita?tsstr. 1, D-56070 Koblenz E-mail: researchreports@uni-koblenz.de, WWW: http://www.uni-koblenz.de/fb4/ System Description: KRHyper Christoph Wernhard Institut fu?r Informatik, Universita?t Koblenz-Landau, D-56070 Koblenz, Germany, wernhard@uni-koblenz.de Abstract. KRHyper is a first order logic theorem proving and model generation system based on the hyper tableau calculus. It is targeted for use as an embedded system within knowledge based applications. In con- trast to most first order theorem provers, it supports features important for those applications, for example queries with predicate extensions as answers, handling of large sets of uniformly structured input facts, arith- metic evaluation and stratified negation as failure. 1 Introduction KRHyper is a first order logic theorem proving and model generation system based on the hyper tableau calculus [2]. It is targeted for use as an embedded system within knowledge based applications such as those described in [1, 3]. While KRHyper is based on techniques used in first order theorem provers — the hyper tableau calculus for first order logic proving, unification, term indexing and fair search control by iterative deepening — it supports a number of features important for knowledge based applications that are not usually found in first order provers. These features are discussed in the following section. Compared to state-of-the-art first order provers, as represented by the par- ticipants of the annual CADE ATP System Competition1, the performance of KRHyper is in the mid range for unsatisfiable Horn problems without equality and for satisfiable problems with finite Herbrand universe. It is at the low edge for unsatisfiable non-Horn problems without equality and Horn problems with equality. For other problem classes it is poor. KRHyper is not equipped with special equali