@TechReport{wernhard:14:2003,
  author	= "Christoph Wernhard",
  title		= "{System Description: KRHyper}",
  institution	= "{Universität Koblenz-Landau}",
  year		= "{2003}",
  type		= "Fachberichte Informatik",
  number	= "14--2003",
  language	= "english",
  address	= "Universität Koblenz-Landau, Institut für Informatik,
		  Universitätsstr. 1, D-56070 Koblenz",
  url		= "http://www.uni-koblenz.de/fb4/publikationen/gelbereihe/RR-14-2003.pdf",
  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 contrast 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, arithmetic evaluation and stratified negation
		  as failure. "
}