PROOF NORMALIZATION FOR RESOLUTION AND PARAMODULATION

被引：0

|

作者：

BACHMAIR, L

机构：

来源：

LECTURE NOTES IN COMPUTER SCIENCE | 1989年 / 355卷

关键词：

D O I：

暂无

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

引用

收藏

页码：15 / 28

页数：14

相关论文

共 50 条

[1] GENERALIZED RESOLUTION USING PARAMODULATION
刘叙华
安直
ScienceBulletin, 1986, (21) : 1441 - 1444
[2] INDUCTIVE PROOFS BY RESOLUTION AND PARAMODULATION
PADAWITZ, P
LECTURE NOTES IN COMPUTER SCIENCE, 1989, 351 : 352 - 368
[3] GENERALIZED RESOLUTION USING PARAMODULATION
LIU, XH
AN, Z
KEXUE TONGBAO, 1986, 31 (21): : 1441 - 1444
[4] ORDERED PARAMODULATION AND RESOLUTION AS DECISION PROCEDURE
FERMULLER, C
SALZER, G
LOGIC PROGRAMMING AND AUTOMATED REASONING, 1993, 698 : 122 - 133
[5] USING FORCING TO PROVE COMPLETENESS OF RESOLUTION AND PARAMODULATION
PAIS, J
PETERSON, GE
JOURNAL OF SYMBOLIC COMPUTATION, 1991, 11 (1-2) : 3 - 19
[6] Proof normalization modulo
Dowek, G
Werner, B
JOURNAL OF SYMBOLIC LOGIC, 2003, 68 (04) : 1289 - 1316
[7] FORMULA DATABASES FOR HIGH-PERFORMANCE RESOLUTION PARAMODULATION SYSTEMS
BUTLER, RM
OVERBEEK, RA
JOURNAL OF AUTOMATED REASONING, 1994, 12 (02) : 139 - 156
[8] WORST CASE EXPONENTIAL LOWER BOUNDS FOR INPUT RESOLUTION WITH PARAMODULATION
STATMAN, R
SIAM JOURNAL ON COMPUTING, 1980, 9 (01) : 104 - 110
[9] Formula databases for high-performance resolution/paramodulation systems
Butler, Ralph M., 1600, Kluwer Academic Publishers, Dordrecht, Netherlands (12):
[10] Normalization proof for Peano Arithmetic
Siders, Annika
ARCHIVE FOR MATHEMATICAL LOGIC, 2015, 54 (7-8) : 921 - 940

← 1 2 3 4 5 →