• search hit 21 of 36
Back to Result List

Hyper tableaux with equality

  • In most theorem proving applications, a proper treatment of equational theories or equality is mandatory. In this paper we show how to integrate a modern treatment of equality in the hyper tableau calculus. It is based on splitting of positive clauses and an adapted version of the superposition inference rule, where equations used for paramodulation are drawn (only) from a set of positive unit clauses, the candidate model. The calculus also features a generic, semantically justified simplification rule which covers many redundancy elimination techniques known from superposition theorem proving. Our main results are soundness and completeness, but we briefly describe the implementation, too.

Download full text files

Export metadata

Additional Services

Search Google Scholar
Metadaten
Author:Peter Baumgartner, Ulrich Furbach, Björn Pelzer
URN:urn:nbn:de:kola-1464
Series (Serial Number):Arbeitsberichte, FB Informatik (2007,12)
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:Equality; Hyper Tableau Calculus; Theorem Proving
Page Number:29
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.