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)

[thumbnail of AMI_36_from85to101.pdf] pdf
AMI_36_from85to101.pdf

Download (208kB) [error in script]

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 - Journal article
Szerző:
Szerző neve
Email
MTMT azonosító
ORCID azonosító
Közreműködés
Kovásznai, Gergely
NEM RÉSZLETEZETT
NEM RÉSZLETEZETT
NEM RÉSZLETEZETT
Szerző
Kusper, Gábor
NEM RÉSZLETEZETT
NEM RÉSZLETEZETT
NEM RÉSZLETEZETT
Szerző
Kapcsolódó URL-ek:
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 Tétel nézet