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]](http://publikacio.uni-eszterhazy.hu/style/images/fileicons/text.png) |
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 |
 |
Tétel nézet |
