This is the homepage of the new implementation of KRHyper in OCaml. KRHyper has originally been written by Peter Baumgartner in Eclipse Prolog (see An extension of the OCaml implementation by superposition based equality handling is currently developed by Björn Pelzer (see

What is KRHyper?

Applications of KRHyper

User Documentation

System Description


Performance Evaluation with the TPTP

Implementation Documentation

Send Bug Reports, Suggestions, ... to

Christoph Wernhard <>