Stratified resolution

被引：6

作者：

Degtyarev, A

Nieuwenhuis, R

Voronkov, A

机构：

[1] Univ Manchester, Dept Comp Sci, Manchester M13 9PL, Lancs, England

[2] Univ Liverpool, Dept Comp Sci, Liverpool L69 3BX, Merseyside, England

[3] Tech Univ Catalonia, LSI, Barcelona, Spain

来源：

JOURNAL OF SYMBOLIC COMPUTATION | 2003年 / 36卷 / 1-2期

关键词：

automated theorem proving; first-order logic; ordered resolution with selection; definition unfolding; redundancy elimination;

D O I：

10.1016/S0747-7171(03)00036-1

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

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. (C) 2003 Elsevier Science Ltd. All rights reserved.

引用

页码：79 / 99

页数：21

共 18 条

[1]

Apt K. R., 1988, FDN DEDUCTIVE DATABA, P89

[2]

Apt K.R., 1990, HDB THEOR COMPUT SCI, P493

[3]

BACHMAIR L, 1991, ICLP 91 LOGIC PROGRA, P645

[4]

Bachmair L., 2001, HDB AUTOMATED REASON, VI, P19, DOI DOI 10.1016/B978-044450813-3/50004-7

[5]

Comon H., 1990, International Journal of Foundations of Computer Science, V1, P387, DOI 10.1142/S0129054190000278

[6]

Degtyarev A, 2000, LECT NOTES ARTIF INT, V1831, P365

[7]

DENIVELLE H, 1996, THESIS TU DELFT

[8]

GANZINGER H, 2001, SATURATE SYSTEM

[9]

JOUANNAUD JP, 1991, LECT NOTES COMPUT SC, V510, P455

[10] A decision procedure for the existential theory of term algebras with the Knuth-Bendix ordering [J].

Korovin, K ;

Voronkov, A .

15TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 2000, :291-302

← 1 2 →