Hyper tableaux

Peter Baumgartner, Ulrich Furbach, Ilkka Niemelä

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

77 Citations (Scopus)

Abstract

This paper introduces a variant of clausal normal form tableaux that we call "hyper tableaux". Hyper tableaux keep many desirable features of analytic tableaux while taking advantage of the central idea from (positive) hyper resolution, namely to resolve away all negative literals of a clause in a single inference step. Another feature of the proposed calculus is the extensive use of universally quantified variables. This enables new efficient forward-chaining proof procedures for full first order theories as variants of tableaux calculi.

Original languageEnglish
Title of host publicationLOGICS IN ARTIFICIAL INTELLIGENCE
Subtitle of host publicationEuropean Workshop, JELIA '96 Évora, Portugal September 30 – October 3, 1996. Proceedings
EditorsJJ Alferes, LM Pereira, E Orlowska
Pages1-17
Number of pages17
ISBN (Electronic)978-3-540-70643-4
DOIs
Publication statusPublished - 1996
MoE publication typeA4 Article in a conference publication
EventEuropean Workshop on Logics in Artificial Intelligence - Evora, Portugal
Duration: 30 Sep 19963 Oct 1996

Publication series

NameLecture Notes in Artificial Intelligence
PublisherSPRINGER-VERLAG BERLIN
Volume1126
ISSN (Print)0302-9743

Workshop

WorkshopEuropean Workshop on Logics in Artificial Intelligence
Abbreviated titleJELIA
CountryPortugal
CityEvora
Period30/09/199603/10/1996

Cite this