Loading...
Please wait, while we are loading the content...
Similar Documents
The Birth of Prolog Aaron Bembenek October 2016 1 A Machine-Oriented Logic Based on the Resolution Principle
| Content Provider | Semantic Scholar |
|---|---|
| Author | Bembenek, Aaron |
| Copyright Year | 2016 |
| Abstract | @article{Robinson:1965, author = {Robinson, J. A.}, title = {A Machine-Oriented Logic Based on the Resolution Principle}, journal = {J. ACM}, volume = {12}, number = {1}, month = jan, year = {1965}, pages = {23--41}, publisher = {ACM}, address = {New York, NY, USA}, } Summary: Robinson presents the resolution principle, an inference principle that can be used to determine the unsatisfiability of a sentence in first-order logic that is especially well-suited for automation. He observes that existing automated theorem proving techniques run into avoidable combinatorial problems because they depend on simple inference principles that were originally designed for human comprehension and are not a good fit for automation. He proposes instead the resolution principle, a generalization of the cut rule that allows inferences that are not necessarily intuitive, but does not suffer the combinatorial issues encountered by previous methods. While a resolution rule for propositional logic had been presented earlier in Davis and Putnam [1960], Robinson’s contribution is generalizing resolution to the first-order setting, which he accomplishes by giving an algorithm for finding the most general unifying substitution of a set of literals. Robinson concludes his paper with some “search principles,” improvements to the resolution principle that in some cases quicken the convergence of resolution or even help resolution converge when it would not otherwise. An alternative title for this paper could be “Resolution: A Logical Inference Principle for Efficient, Automated Theorem Proving.” Evaluation: Lloyd [1984] describes Robinson’s paper as a “landmark paper.” It led to intense research activity on refinements and variations of resolution in the late 1960s, as well as a line of research pushing back against |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | http://www.seas.harvard.edu/courses/cs252/2016fa/10.pdf |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
