Skip to main content
SpringerLink
Log in

The Resolution Principle

  • Chapter
Book cover Handbook of Philosophical Logic

Part of the book series: Handbook of Philosophical Logic ((HALO,volume 12))

  • 849 Accesses

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 169.00
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 219.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 219.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Bibliography

  1. W. Ackermann.:Uber die Erfüllbarkeit gewisser Zählausdrücke. Mathematische Annalen, 100:638–649, 1928.

    Article  ISI  Google Scholar 

  2. O. Arieli and A. Avron. The value of four values. Artificial Intelligence, 102:97–141, 1998.

    Article  ISI  Google Scholar 

  3. F. Baader and W. Snyder. Unification theory. In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, volume I, chapter 8, pages 445–532. Elsevier Science, 2001.

    Google Scholar 

  4. M. Baaz and C.G. Fermüller. Resolution-based theorem proving for many-valued logics. Journal of Symbolic Computation, 19(4):353–391, April 1995.

    Article  ISI  Google Scholar 

  5. M. Baaz and A. Leitsch. Complexity of resolution proofs and function introduction. Annals of Pure and Applied Logic, 57:181–215, 1992.

    Article  ISI  Google Scholar 

  6. M. Baaz and A. Leitsch. On skolemization and proof complexity. Fundamenta Informaticae, 20:353–379, 1994.

    Google Scholar 

  7. M. Baaz and A. Leitsch. Cut normal forms and proof complexity. Annals of Pure and Applied Logic, 97:127–177, 1999.

    Article  ISI  Google Scholar 

  8. M. Baaz and A. Leitsch. Cut-elimination and redundancy-elimination by resolution. J. Symbolic Computation, 29:149–176, 2000.

    Google Scholar 

  9. [Baaz et al., 1994]_M. Baaz, C.G. Fermüller, and A. Leitsch. A non-elementary speed-up in proof length by structural clause form transformation. In Proc. LICS, pages 213–219, 1994.

    Google Scholar 

  10. [Baaz et al., 1996]_M. Baaz, C.G. Fermüller, G. Salzer, and R. Zach. MUltlog 1.0: Towards an expert system for many-valued logics. In 13th Int. Conf. on Automated Deduction (CADE’96), volume 1104 of Lecture Notes in Artificial Intelligence, pages 226–230. Springer, 1996.

    Google Scholar 

  11. [Baaz et al., 1998]_M. Baaz, C.G. Fermüller, G. Salzer, and R. Zach. Labeled calculi and finite-valued logics. Studia Logica, 61(1):7–13, 1998.

    Google Scholar 

  12. [Baaz et al., 2001a]_M. Baaz, U. Egly, and A. Leitsch. Normal form transformations. In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, volume I, chapter 5, pages 273–333. Elsevier Science, 2001.

    Google Scholar 

  13. [Baaz et al., 2001b]_M. Baaz, C.G. Fermüller, and G. Salzer. Automated deduction for many-valued logics. In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, volume II, chapter 20, pages 1355–1402. Elsevier Science, 2001.

    Google Scholar 

  14. [Baaz et al., 2001c]_M. Baaz, C.G. Fermüller, and G. Salzer. Automated deduction for many-valued logics. In John Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning (in 2 volumes), volume 2, pages 1356–1402. Elsevier and MIT Press, 2001.

    Google Scholar 

  15. L. Bachmair and H. Ganzinger. Rewrite-based equational theorem proving with selection and simplification. Journal of Logic and Computation, 4:1–31, 1994.

    Google Scholar 

  16. L. Bachmair and H. Ganzinger. Resolution theorem proving. In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, volume I, chapter 2, pages 19–99. Elsevier Science, 2001.

    Google Scholar 

  17. N.D. Belnap Jr. A useful four-valued logic. In J. Micheal Dunn and George Epstein, editors, Modern uses of multiple-valued logic, pages 8–37. Reidel, Dordrecht, 1977.

    Google Scholar 

  18. W. Bernays and M. Schönfinkel. Zum Entscheidungsproblem der mathematischen Logik. Mathematische Annalen, 99:342–372, 1928.

    Article  ISI  Google Scholar 

  19. G. Boole. An investigation on the laws of thought. Dover Publications, 1958.

    Google Scholar 

  20. [Börger et al., 1997]_E. Börger, E. Grädel, and Y. Gurevich. The Classical Decision Problem. Perspectives in Mathematical Logic. Springer, 1997.

    Google Scholar 

  21. A. Church. A note on the Entscheidungsproblem. Journal of Symbolic Logic, 1:40–44, 1936.

    Google Scholar 

  22. M. Davis and H. Putnam. A Computing Procedure for Quantification Theory. Journal of the ACM, 7(3):201–215, July 1960.

    Article  ISI  Google Scholar 

  23. N. Dershowitz and D.A. Plaisted. Rewriting. In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, volume I, chapter 9, pages 535–610. Elsevier Science, 2001.

    Google Scholar 

  24. E. Eder. Relative complexities of first-order calculi. Vieweg, 1992.

    Google Scholar 

  25. U. Egly and T. Rath. On the practical value of different definitional translations to normal form. In Proc. of CADE-13, volume 1104 of Lecture Notes in Artificial Intelligence, pages 403–417. Springer, 1996.

    Google Scholar 

  26. C.G. Fermüller and A. Leitsch. Hyperresolution and automated model building. Journal of Logic and Computation, 6(2):173–203, 1996.

    Google Scholar 

  27. [Fermüller et al., 1993]_C.G. Fermüller, A. Leitsch, T. Tammet, and N. Zamov. Resolution Methods for the Decision Problem, volume 679 of Lecture Notes in Artificial Intelligence. Springer, 1993.

    Google Scholar 

  28. [Fermüller et al., 2001]_C.G. Fermüller, A. Leitsch, U. Hustadt, and T. Tammet. Resolution decision procedures. In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, volume II, chapter 25, pages 1791–1849. Elsevier Science, 2001.

    Google Scholar 

  29. G. Frege. Begriffsschrift, eine der arithmetischen nachgebildete Formelsprachedes reinen Denkens. In J. van Heijenoort, editor, From Frege to Gödel: A sourcebook in mathematical logic 1879-1931. Harvard University Press, 1967.

    Google Scholar 

  30. H. Gelernter. Realization of a geometry theorem proving machine. In Proceedings of the International Conference on Information Processing, pages 273–282, June 1959.

    Google Scholar 

  31. G. Gentzen. DeUntersuchungen über das logische Schließen. Mathematische Zeitschrift, 39:405–431, 1934.

    ISI  Google Scholar 

  32. G. Gentzen. Untersuchungen über das logische Schließen I-II. Mathematische Zeitschrift, 39:176–210 and 405-431, 1934-35.

    ISI  Google Scholar 

  33. P.C. Gilmore. A proof method for quantification theory: its justification and realization. IBM J. Res. Dev., pages 28–35, 1960.

    Google Scholar 

  34. K. Gödel. Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme. Monatshefte für Mathematik und Physik, 38:175–198, 1931.

    Google Scholar 

  35. K. Gödel. Ein Spezialfall des Entscheidungsproblems der theoretischen Logik. Ergebnisse Mathematischer Kolloquien, 2:27–28, 1932.

    Google Scholar 

  36. K. Gödel. Zum intuitionistischen Aussagenkalkül. Anzeiger der Akademie der Wissenschaften in Wien, 69:65–66, 1932.

    Google Scholar 

  37. R. Hähnle. Commodious axiomatization of quantifiers in multiple-valued logic. Studia Logica, 61(1):101–121, 1998.

    Google Scholar 

  38. R. Hähnle. Tableaux and related methods. In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, volume 1, pages 101–178. Elsevier, 2001.

    Google Scholar 

  39. J. Herbrand. Sur le problème fondamental de la logique mathématique. Sprawozdania z posiedzen Towarzysta Naukowego Warszawskiego, Wydzial III, 24:12–56, 1931.

    Google Scholar 

  40. D. Hilbert and W. Ackermann. Grundzüge der theoretischen Logik. Springer, Berlin, 1928.

    Google Scholar 

  41. D. Hilbert and P. Bernays. Grundlagen der Mathematik. Springer, 1970.

    Google Scholar 

  42. W. Joyner. Automated Theorem Proving and the Decision Problem. PhD thesis, Harvard University, 1973.

    Google Scholar 

  43. W.H. Joyner. Resolution strategies as decision procedures. Journal of the ACM, 23: 398–417, 1976.

    ISI  Google Scholar 

  44. G.W. Leibniz. Calculus ratiocinator. In Preussische Akademie der Wissenschaften, editor, Sämtliche Schriften und Briefe. Reichel, Darmstadt, 1923.

    Google Scholar 

  45. A. Leitsch. The resolution calculus. Springer. Texts in Theoretical Computer Science, 1997.

    Google Scholar 

  46. D.W. Loveland. A linear format for resolution. In Proc. IRIA Symposium on Automatic Demonstration, volume 125 of Lecture Notes in Mathematics, pages 147–162. Springer, 1970.

    Google Scholar 

  47. L. Löwenheim. Über Möglichkeiten im Relativkalkül. Mathematische Annalen, 68:169–207, 1915.

    Google Scholar 

  48. J. Lukasiewicz. Philosophische Bemerkungen zu mehrwertigen Systemen des Aussagenkalküls. Comptes rendus des séances de la Société des Sciences et des Lettres de Varsovie Cl. III, 23:51–77, 1930.

    Google Scholar 

  49. A. Martelli and U. Montanari. Unification in linear time and space: a structured presentation. Technical Report B76-16, Istituto di elaborazione della informazione, 1976.

    Google Scholar 

  50. S.Y. Maslov. The inverse method for establishing deducibility for logical calculi. Proc. Steklov Inst. Math., 98:25–96, 1968.

    Google Scholar 

  51. W. McCune. Solution of the Robbins problem. Journal of Automated Reasoning, 19(3): 263–276, 1997.

    Article  ISI  Google Scholar 

  52. G. Mints. Gentzen-type systems and resolution rule, part I: Propositional logic. In P. Martin-Löf and G. Mints, editors, Proceedings Int. Conf. on Computer Logic, COLOG’88, Tallinn, USSR, 12-16 Dec 1988, volume 417 of Lecture Notes in Computer Science, pages 198–231. Springer-Verlag, Berlin, 1990.

    Google Scholar 

  53. G. Mints. Gentzen-type systems and resolution rule, part II: Predicate logic. In J. Oikkonen and J. Väänänen, editors, Proceedings ASL Summer Meeting, Logic Colloquium’ 90, Helsinki, Finland, 15-22 July 1990, volume 2 of Lecture Notes in Logic, pages 163–190. Springer-Verlag, Berlin, 1993.

    Google Scholar 

  54. [Ohlbach et al., 2001]_H.J. Ohlbach, A. Nonnengart, M. de Rijke, and D. Gabbay. Encoding two-valued nonclassical logics in classical logic. In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, volume II, chapter 21, pages 1403–1486. Elsevier Science, 2001.

    Google Scholar 

  55. V.P. Orevkov. Lower bounds for increasing complexity of derivations after cut elimination. Journal of Soviet Mathematics, 20:2337–2350, 1982.

    Google Scholar 

  56. R. Pichler. Algorithms on atomic representations of Herbrand models. In Proc. of JELIA’98, pages 199–215. Springer, LNAI 1489, 1998.

    Google Scholar 

  57. J.A. Robinson. Automatic deduction with hyperresolution. Intern. Journal of Computer Math., 1:227–234, 1965.

    Google Scholar 

  58. J.A. Robinson. A machine-oriented logic based on the resolution principle. J. Assoc. Comput. Mach., 12:23–41, 1965.

    Google Scholar 

  59. G. Rousseau. Sequents in many valued logic I. Fundamenta Mathematicæ, LX: 23–33, 1967.

    Google Scholar 

  60. G. Salzer. Optimal axiomatizations for multiple-valued operators and quantifiers based on semilattices. In Michael McRobbie and John Slaney, editors, Proc. 13th Conference on Automated Deduction, New Brunswick/NJ, USA, volume 1104 of LNCS, pages 688–702. Springer-Verlag, 1996.

    Google Scholar 

  61. J.R. Slagle. Automatic theorem proving with renamable and semantic resolution. Journal of the ACM, 14(4):687–697, October 1967.

    Article  ISI  Google Scholar 

  62. V. Sofronie-Stokkermans. Resolution-based theorem proving for SHn-logics. In Ricardo Caferra and Gernot Salzer, editors, Int. Workshop on First-Order Theorem Proving (FTP’ 98), Technical Report E1852-GS-981, pages 224–233. Technische Universitat Wien, Austria, 1998.

    Google Scholar 

  63. R. Statman. Lower bounds on Herbrand’s theorem. Proc. of the Amer. Math. Soc., 75:104–107, 1979.

    Google Scholar 

  64. M. Takahashi. Many-valued logics of extended Gentzen style I. Science Reports of the Tokyo Kyoiku Daigaku, Section A, 9(231):95–116, 1967.

    Google Scholar 

  65. G. Takeuti. Proof Theory. North-Holland, second edition, 1987.

    Google Scholar 

  66. A. Turing. On computable numbers with an application to the Entscheidungsproblem. Proc. of the London Math. Soc., Ser. 2(42):230–265, 1936/37.

    Google Scholar 

Download references

Authors
  1. Alexander Leitsch
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Christian Fermüller
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. King’s College, London, UK

    D.M. Gabbay

  2. Centrum für Informations- und Sprachverarbeitung, Ludwig-Maximilians-Universität, München, Germany

    F. Guenthner

Rights and permissions

Reprints and permissions

Copyright information

© 2005 Springer

About this chapter

Cite this chapter

Leitsch, A., Fermüller, C. (2005). The Resolution Principle. In: Gabbay, D., Guenthner, F. (eds) Handbook of Philosophical Logic. Handbook of Philosophical Logic, vol 12. Springer, Dordrecht. https://doi.org/10.1007/1-4020-3092-4_2

Download citation

Publish with us

Policies and ethics

Search

Navigation