Menu_Home Home   Menu_Latest Latest   Menu_Search Advanced Search   Menu_Browse_by_Year By Year   Menu_Browse_by_Division By Division
Screen decoration graphicsLogo

Stratified resolution

Degtyarev, Anatoli and Nieuwenhuis, Robert and Voronkov, Andrei (2003) Stratified resolution. Journal of Symbolic Computation, 36 (1-2). pp. 79-99.

[img]PDF - Repository staff only - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader


We introduce a calculus of stratified resolution, in which special attention is paid to clauses that "define" relations. If such clauses are discovered in the initial set of clauses, they are treated using the rule of definition unfolding, i.e. the rule that replaces defined relations by their definitions. Stratified resolution comes with a powerful notion of redundancy: a clause to which definition unfolding has been applied can be removed from the search space. To prove the completeness of stratified resolution with redundancies, we use a novel combination of Bachmair and Ganzingerâ??s model construction technique and a hierarchical construction of orderings and least fixpoints.

Item Type:Article
ID Code:882
Deposited By:Dr Anatoli Degtyarev
Deposited On:07 Nov 2007 15:54
Last Modified:07 Nov 2007 16:02

Repository Staff Only: item control page