System Description: E-KRHyper

  • The E-KRHyper system is a model generator and theorem prover for first-order logic with equality. It implements the new E-hyper tableau calculus, which integrates a superposition-based handling of equality into the hyper tableau calculus. E-KRHyper extends our previous KRHyper system, which has been used in a number of applications in the field of knowledge representation. In contrast to most first order theorem provers, it supports features important for such 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. It is our goal to extend the range of application possibilities of KRHyper by adding equality reasoning.

Download full text files

Export metadata

Additional Services

Search Google Scholar
Metadaten
Author:Björn Pelzer, Christoph Wernhard
URN:urn:nbn:de:kola-1473
Series (Serial Number):Arbeitsberichte, FB Informatik (2007,13)
Document Type:Part of Periodical
Language:English
Date of Publication (online):2007/09/20
Date of first Publication:2007/09/20
Publishing Institution:Universität Koblenz-Landau, Campus Koblenz, Universitätsbibliothek
Release Date:2007/09/20
Tag:E-KRHyper; Equality; Tableau Calculus; Theorem Proving
Page Number:6
Institutes:Fachbereich 4 / Institut für Informatik
Dewey Decimal Classification:0 Informatik, Informationswissenschaft, allgemeine Werke / 00 Informatik, Wissen, Systeme / 004 Datenverarbeitung; Informatik
Licence (German):Es gilt das deutsche Urheberrecht: § 53 UrhG
Einverstanden ✔
Diese Webseite verwendet technisch erforderliche Session-Cookies. Durch die weitere Nutzung der Webseite stimmen Sie diesem zu. Unsere Datenschutzerklärung finden Sie hier.