Resolution (logic) (English Wikipedia)

Analysis of information sources in references of the Wikipedia article "Resolution (logic)" in English language version.

refsWebsite

Global rank English rank

2^nd place

2^nd place

4semanticscholar.org

11^th place

8^th place

3books.google.com

3^rd place

3^rd place

3,753^rd place

2,311^th place

833^rd place

567^th place

1zentralblatt-math.org

low place

low place

low place

low place

books.google.com

Leitsch 1997, p. 11 "Before applying the inference method itself, we transform the formulas to quantifier-free conjunctive normal form." Leitsch, Alexander (1997). The Resolution Calculus. Texts in Theoretical Computer Science. An EATCS Series. Springer. ISBN 978-3-642-60605-2.
Arís, Enrique P.; González, Juan L.; Rubio, Fernando M. (2005). Lógica Computacional. Ediciones Paraninfo, S.A. ISBN 9788497321822.
Nieuwenhuis, Robert; Rubio, Alberto (2001). "7. Paramodulation-Based Theorem Proving" (PDF). In Robinson, Alan J.A.; Voronkov, Andrei (eds.). Handbook of Automated Reasoning. Elsevier. pp. 371–444. ISBN 978-0-08-053279-0.

cmi.ac.in

Nieuwenhuis, Robert; Rubio, Alberto (2001). "7. Paramodulation-Based Theorem Proving" (PDF). In Robinson, Alan J.A.; Voronkov, Andrei (eds.). Handbook of Automated Reasoning. Elsevier. pp. 371–444. ISBN 978-0-08-053279-0.

doi.org

Davis, Martin; Putnam, Hilary (1960). "A Computing Procedure for Quantification Theory". J. ACM. 7 (3): 201–215. doi:10.1145/321033.321034. S2CID 31888376. Here: p. 210, "III. Rule for Eliminating Atomic Formulas".
Robinson 1965 Robinson, J. Alan (1965). "A Machine-Oriented Logic Based on the Resolution Principle". Journal of the ACM. 12 (1): 23–41. doi:10.1145/321250.321253. S2CID 14389185.
Manna, Zohar; Waldinger, Richard (January 1980). "A Deductive Approach to Program Synthesis". ACM Transactions on Programming Languages and Systems. 2: 90–121. doi:10.1145/357084.357090. S2CID 14770735.
Murray, N.V. (1982). "Completely Non-Clausal Theorem Proving". Artificial Intelligence. 18: 67–85. doi:10.1016/0004-3702(82)90011-x.
Traugott, J. (1986). "Nested Resolution". 8th International Conference on Automated Deduction. CADE 1986. LNCS. Vol. 230. Springer. pp. 394–403. doi:10.1007/3-540-16780-3_106. ISBN 978-3-540-39861-5.
Schmerl, U.R. (1988). "Resolution on Formula-Trees". Acta Informatica. 25 (4): 425–438. doi:10.1007/bf02737109. S2CID 32702782. Summary

dtic.mil

apps.dtic.mil

Manna, Zohar; Waldinger, Richard (January 1980). "A Deductive Approach to Program Synthesis". ACM Transactions on Programming Languages and Systems. 2: 90–121. doi:10.1145/357084.357090. S2CID 14770735.

semanticscholar.org

api.semanticscholar.org

Davis, Martin; Putnam, Hilary (1960). "A Computing Procedure for Quantification Theory". J. ACM. 7 (3): 201–215. doi:10.1145/321033.321034. S2CID 31888376. Here: p. 210, "III. Rule for Eliminating Atomic Formulas".
Robinson 1965 Robinson, J. Alan (1965). "A Machine-Oriented Logic Based on the Resolution Principle". Journal of the ACM. 12 (1): 23–41. doi:10.1145/321250.321253. S2CID 14389185.
Manna, Zohar; Waldinger, Richard (January 1980). "A Deductive Approach to Program Synthesis". ACM Transactions on Programming Languages and Systems. 2: 90–121. doi:10.1145/357084.357090. S2CID 14770735.
Schmerl, U.R. (1988). "Resolution on Formula-Trees". Acta Informatica. 25 (4): 425–438. doi:10.1007/bf02737109. S2CID 32702782. Summary

syr.edu

surface.syr.edu

Murray, Neil V. (February 1979). A Proof Procedure for Quantifier-Free Non-Clausal First Order Logic (Technical report). Electrical Engineering and Computer Science, Syracuse University. 39. (Cited from Manna, Waldinger, 1980 as: "A Proof Procedure for Non-Clausal First-Order Logic", 1978)

zentralblatt-math.org

Schmerl, U.R. (1988). "Resolution on Formula-Trees". Acta Informatica. 25 (4): 425–438. doi:10.1007/bf02737109. S2CID 32702782. Summary