Hyper tableaux with equality

Peter Baumgartner*, Ulrich Furbach, Björn Pelzer

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

22 Citations (Scopus)

Abstract

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.

Original languageEnglish
Title of host publicationAutomated Deduction - CADE-21 - 21st International Conference on Automated Deduction, Proceedings
PublisherSpringer Verlag
Pages492-507
Number of pages16
ISBN (Print)3540735941, 9783540735946
DOIs
Publication statusPublished - 2007
Externally publishedYes
Event21st International Conference on Automated Deduction, CADE-21 2007 - Bremen, Germany
Duration: 17 Jul 200720 Jul 2007

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume4603 LNAI
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference21st International Conference on Automated Deduction, CADE-21 2007
Country/TerritoryGermany
CityBremen
Period17/07/0720/07/07

Fingerprint

Dive into the research topics of 'Hyper tableaux with equality'. Together they form a unique fingerprint.

Cite this