Hyper tableaux

Peter Baumgartner, Ulrich Furbach, Ilkka Niemelä

Tutkimustuotos: Artikkeli kirjassa/konferenssijulkaisussaConference contributionScientificvertaisarvioitu

87 Sitaatiot (Scopus)

Abstrakti

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.

AlkuperäiskieliEnglanti
OtsikkoLOGICS IN ARTIFICIAL INTELLIGENCE
AlaotsikkoEuropean Workshop, JELIA '96 Évora, Portugal September 30 – October 3, 1996. Proceedings
ToimittajatJJ Alferes, LM Pereira, E Orlowska
Sivut1-17
Sivumäärä17
ISBN (elektroninen)978-3-540-70643-4
DOI - pysyväislinkit
TilaJulkaistu - 1996
OKM-julkaisutyyppiA4 Artikkeli konferenssijulkaisuussa
TapahtumaEuropean Workshop on Logics in Artificial Intelligence - Evora, Portugali
Kesto: 30 syysk. 19963 lokak. 1996

Julkaisusarja

NimiLecture Notes in Artificial Intelligence
KustantajaSPRINGER-VERLAG BERLIN
Vuosikerta1126
ISSN (painettu)0302-9743

Workshop

WorkshopEuropean Workshop on Logics in Artificial Intelligence
LyhennettäJELIA
Maa/AluePortugali
KaupunkiEvora
Ajanjakso30/09/199603/10/1996

Siteeraa tätä