HUMAN ORIENTED LOGIC FOR AUTOMATIC THEOREM-PROVING

[1] ALLEN J, 1970, MACHINE INTELLIGENCE, P321

[2] SPLITTING AND REDUCTION HEURISTICS IN AUTOMATIC THEOREM PROVING [J]. ARTIFICIAL INTELLIGENCE, 1971, 2 (01) : 55 - 77

[3] COMPUTER PROOFS OF LIMIT THEOREMS [J]. ARTIFICIAL INTELLIGENCE, 1972, 3 (02) : 27 - 60

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

[5] THEOREM PROVING WITH VARIABLE-CONSTRAINED RESOLUTION [J]. INFORMATION SCIENCES, 1972, 4 (03) : 217 - &

[6] CHINTHAYAMMA, 1969, NOTICES AM MATH SOC, V16, pT69

[7] UTILITY OF INDEPENDENT SUBGOALS IN THEOREM PROVING [J]. INFORMATION AND CONTROL, 1971, 18 (03): : 237 - &

[8] KLEENE SC, 1952, INTRO METAMATHEMATIC

[9] LINEAR RESOLUTION WITH SELECTION FUNCTION [J]. ARTIFICIAL INTELLIGENCE, 1971, 2 (3-4) : 227 - 260

[10] UNIFYING VIEW OF SOME LINEAR HERBRAND PROCEDURES [J]. JOURNAL OF THE ACM, 1972, 19 (02) : 366 - &

[1] ALLEN J, 1970, MACHINE INTELLIGENCE, P321

[2] SPLITTING AND REDUCTION HEURISTICS IN AUTOMATIC THEOREM PROVING [J]. ARTIFICIAL INTELLIGENCE, 1971, 2 (01) : 55 - 77

[3] COMPUTER PROOFS OF LIMIT THEOREMS [J]. ARTIFICIAL INTELLIGENCE, 1972, 3 (02) : 27 - 60

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

[5] THEOREM PROVING WITH VARIABLE-CONSTRAINED RESOLUTION [J]. INFORMATION SCIENCES, 1972, 4 (03) : 217 - &

[6] CHINTHAYAMMA, 1969, NOTICES AM MATH SOC, V16, pT69

[7] UTILITY OF INDEPENDENT SUBGOALS IN THEOREM PROVING [J]. INFORMATION AND CONTROL, 1971, 18 (03): : 237 - &

[8] KLEENE SC, 1952, INTRO METAMATHEMATIC

[9] LINEAR RESOLUTION WITH SELECTION FUNCTION [J]. ARTIFICIAL INTELLIGENCE, 1971, 2 (3-4) : 227 - 260

[10] UNIFYING VIEW OF SOME LINEAR HERBRAND PROCEDURES [J]. JOURNAL OF THE ACM, 1972, 19 (02) : 366 - &