Journal of the ACM · 1974 · 70 citations · 12 references
HumanitiesComputer ScienceArtificial IntelligenceLogicTheory Of ComputationAutomated ReasoningDeductive SystemsMathematical LogicPredicate LogicProof TheoryTheorem ProvingAutomated Theorem ProvingAutomatic Theorem ProvingFormal Proof SystemsProof AutomationProof SearchProof SystemsResolution Theorem Proving
A deductive system is described which combines aspects of resolution (e.g. unification and the use of Skolem functions) with that of natural deduction and whose performance compares favorably with the best predicate calculus theorem provers.
12
Linear resolution with selection function
Robert Kowalski, D. Brian Kuehner · Artificial Intelligence · 1971 · 256 citations
Splitting and reduction heuristics in automatic theorem proving
W. W. Bledsoe · Artificial Intelligence · 1971 · 103 citations