KRHyper

This is the homepage of the new implementation of KRHyper in OCaml. KRHyper has originally been written by Peter Baumgartner in Eclipse Prolog (see http://www.uni-koblenz.de/~peter/KRHYPER/). An extension of the OCaml implementation by superposition based equality handling is currently developed by Björn Pelzer (see http://www.uni-koblenz.de/~bpelzer/ekrhyper/).

What is KRHyper?

• 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
• It supports features which are important for such applications but can not usually be found in first order theorem provers:
  • Queries with predicate extensions as answers
  • Handling of large sets of uniformly structured input facts
  • Arithmetic evaluation and stratified negation as failure

Applications of KRHyper

User Documentation

• News (Last update: Apr 22 2005)
• Reference Manual
• Usage Hints (Frequently Encountered Difficulties, Examples)
• Using the Local Installation at Campus Koblenz
• KRHyper with Windows
• Known Bugs and Limitations

System Description

• Christoph Wernhard
  System Description: KRHyper
  Fachberichte Informatik 14--2003, Universität Koblenz-Landau, 2003
  [BibTeX | Postscript ]

Downloads

• Sources of the Latest Version: krh_latest.tgz
• Further ad-hoc stuff that may be unmaintained [Local Access Only]

Performance Evaluation with the TPTP

Implementation Documentation

• OCamlDoc
• OcamlDoc Dependency Graphs: Modules | Modules MLI | Types | Types MLI

Send Bug Reports, Suggestions, ... to

Christoph Wernhard <wernhard@uni-koblenz.de>