Introducing general redundancy criteria for clausal tableaux, and proposing resolution tableaux

Kovásznai, Gergely, Kusper, Gábor (2009) Introducing general redundancy criteria for clausal tableaux, and proposing resolution tableaux Annales Mathematicae et Informaticae. 36. pp. 85-101. ISSN 1787-5021 (Print), 1787-6117 (Online)

pdf AMI_36_from85to101.pdf Download (208kB)

Absztrakt (kivonat)

Hyper tableau calculi are well-known as attempts to combine hyper-res- olution and tableaux. Besides their soundness and completeness, it is also important to give an appropriate redundancy criterion. The task of such a criterion is to filter out “unnecessary” clauses being attached to a given tableau. This is why we investigate what redundancy criteria can be defined for clausal tableaux, in general. This investigation leaded us to a general idea for combining resolution calculi and tableaux. The goal is the same as in the case of hyper-tableau calculi: to split (hyper-)resolution derivations into branches. We propose a novel method called resolution tableaux. Resolution tableaux are more general than hyper tableaux, since any resolution calculus (not only hyperresolution) can be applied, like, e.g., binary resolution, input resolution, or lock resolution etc. We prove that any resolution tableau calculus inherits the soundness and the completeness of the resolution calculus which is being applied. Hence, resolution tableaux can be regarded as a kind of parallelization of resolution.

Mű típusa:	Folyóiratcikk
Szerző:	Szerző neve MTMT azonosító ORCID azonosító Közreműködés Kovásznai, Gergely NEM RÉSZLETEZETT NEM RÉSZLETEZETT Szerző Kusper, Gábor NEM RÉSZLETEZETT NEM RÉSZLETEZETT Szerző
Kapcsolódó URL-ek:	Folyóirat honlapja
Nyelv:	angol
Kötetszám:	36.
ISSN:	1787-5021 (Print), 1787-6117 (Online)
Felhasználó:	Tibor Gál
Dátum:	05 Már 2019 16:58
Utolsó módosítás:	05 Már 2019 16:58
URI:	http://publikacio.uni-eszterhazy.hu/id/eprint/3121

Műveletek (bejelentkezés szükséges)

Tétel nézet