COMPLETENESS OF LINEAR REFUTATION FOR THEORIES WITH EQUALITY

[1] A LINEAR FORMAT FOR RESOLUTION WITH MERGING AND A NEW TECHNIQUE FOR ESTABLISHING COMPLETENESS [J]. JOURNAL OF THE ACM, 1970, 17 (03) : 525 - &

[2] UNIT PROOF AND INPUT PROOF IN THEOREM PROVING [J]. JOURNAL OF THE ACM, 1970, 17 (04) : 698 - &

[3] CHANG CWJ, TO BE PUBLISHED

[4] DARLINGTON JL, 1968, MACHINE INTELLIGENCE, V3, P77

[5] Ernst G, 1969, GPS CASE STUDY GEN P

[6] Robinson G., 1969, MACH INTELL, V4, P135

[7] A MACHINE-ORIENTED LOGIC BASED ON RESOLUTION PRINCIPLE [J]. JOURNAL OF THE ACM, 1965, 12 (01) : 23 - &

[8] EXPERIMENTS WITH A MULTIPURPOSE THEOREM-PROVING HEURISTIC PROGRAM [J]. JOURNAL OF THE ACM, 1968, 15 (01) : 85 - &

[9] SLAGLE JR, TO BE PUBLISHED

[10] WOS LR, 1970, 1968 P IRIA S AUT DE, P276

[1] A LINEAR FORMAT FOR RESOLUTION WITH MERGING AND A NEW TECHNIQUE FOR ESTABLISHING COMPLETENESS [J]. JOURNAL OF THE ACM, 1970, 17 (03) : 525 - &

[2] UNIT PROOF AND INPUT PROOF IN THEOREM PROVING [J]. JOURNAL OF THE ACM, 1970, 17 (04) : 698 - &

[3] CHANG CWJ, TO BE PUBLISHED

[4] DARLINGTON JL, 1968, MACHINE INTELLIGENCE, V3, P77

[5] Ernst G, 1969, GPS CASE STUDY GEN P

[6] Robinson G., 1969, MACH INTELL, V4, P135

[7] A MACHINE-ORIENTED LOGIC BASED ON RESOLUTION PRINCIPLE [J]. JOURNAL OF THE ACM, 1965, 12 (01) : 23 - &

[8] EXPERIMENTS WITH A MULTIPURPOSE THEOREM-PROVING HEURISTIC PROGRAM [J]. JOURNAL OF THE ACM, 1968, 15 (01) : 85 - &

[9] SLAGLE JR, TO BE PUBLISHED

[10] WOS LR, 1970, 1968 P IRIA S AUT DE, P276