Advertisement

Kanger’s Choices in Automated Reasoning

  • Anatoli Degtyarev
  • Andrei Voronkov
Part of the Synthese Library book series (SYLI, volume 304)

Abstract

Automated deduction, or automated theorem proving is a branch of science that deals with automatic search for a proof. The contribution of Kanger to automated deduction is well-recognized. His monograph [1957] introduced a calculus LC, which was one of the first calculi intended for automated proof-search. His article [1963] was later republished as [Kanger 1983] in the collection of “classical papers on computational logic”. [1963] (and also [1959]) calculi used some interesting features that have not been noted for a number of years, and the importance of which in the area of automated deduction has been recognized only much later.

Keywords

Decision Procedure Theorem Prove Inverse Method Automate Reasoning Proof Theory 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Ackermann, W. [1954], Solvable Cases of the Decision Problem, North-Holland.Google Scholar
  2. Bachmair, L. & Ganzinger, H. [1999], ‘A theory of resolution’, in A. Robinson & A. Voronkov (eds.), Handbook of Automated Reasoning, Elsevier Science and MIT Press. To appear.Google Scholar
  3. Benanav, D. [1990], ‘Simultaneous paramodulation’, in M. Stickel (ed.), Proc. 10th Int. Conf. on Automated Deduction, Vol. 449 of Lecture Notes in Artificial Intelligence, pp. 442–455.Google Scholar
  4. Beth, E. [1955], ‘Semantic entailment and formal derivability’, Mededelinger der Koninklijke Nederlandse Akademie van Wetenschappen, Afd. Letterkunde, Nieuwe Reeks 18 (13).Google Scholar
  5. Beth, E. [1959], The Foundation of Mathematics, North-Holland Publ. Co., Amsterdam.Google Scholar
  6. Davis, M. & Putnam, H. [1960], ‘A computing procedure for quantification theory’, Journal of the Association for Computing Machinery 7 (3). Reprinted as Davis & Putnam [1983].Google Scholar
  7. Davis, M. & Putnam, H. [1983], ‘A computing procedure for quantification theory’, in J. Siekmann & G. Wrightson (eds.), Automation of Reasoning. Classical Papers on Computational Logic, Vol. 1, Springer Verlag, pp. 125–150. Originally appeared as Davis & Putnam [1960].Google Scholar
  8. Degtyarev, A., Gurevich, Y., Narendran, P., Veanes, M. & Voronkov, A. [1998], ‘The decidability of simultaneous rigid E-unification with one variable’, in T. Nipkow (ed.), Rewriting Techniques and Applications, RTA’98, Vol. 1379 of Lecture Notes in Computer Science, Springer Verlag, pp. 181–195.Google Scholar
  9. Degtyarev, A., Gurevich, Y. & Voronkov, A. [1996], ‘Herbrand’s theorem and equational reasoning: Problems and solutions’, in Bulletin of the European Association for Theoretical Computer Science, Vol. 60, pp. 78–95. The “Logic in Computer Science” column.Google Scholar
  10. Degtyarev, A. & Voronkov, A. [1996a], ‘Equality elimination for the tableau method’, in J. Calmet & C. Limongelli (eds.), Design and Implementation of Symbolic Computation Systems. International Symposium, DISCO’96, Vol. 1128 of Lecture Notes in Computer Science, Karlsruhe, Germany, pp. 46–60.CrossRefGoogle Scholar
  11. Degtyarev, A. & Voronkov, A. [1996b], ‘The undecidability of simultaneous rigid E-unification’, Theoretical Computer Science 166 (1–2), 291–300.CrossRefGoogle Scholar
  12. Degtyarev, A. & Voronkov, A. [1998a], Equality reasoning in sequent-based calculi, Technical Report MPI-I-98-2-011, Max-Planck Institut für Informatik, Saarbrücken.Google Scholar
  13. Degtyarev, A. & Voronkov, A. [1998b], ‘What you always wanted to know about rigid E-unification’, Journal of Automated Reasoning 20 (1), 47–80.CrossRefGoogle Scholar
  14. Degtyarev, A. & Voronkov, A. [1999], ‘Equality reasoning in sequent-based calculi’, in A. Robinson & A. Voronkov (eds.), Handbook of Automated Reasoning, Elsevier Science and MIT Press. To appear.Google Scholar
  15. Fermüller, D., Leitsch, A., Tammet, T. & Zamov, N. [1993], Resolution Methods for the Decision Problem, Vol. 679 of Lecture Notes in Computer Science, Springer Verlag.Google Scholar
  16. Fitting, M. [1996], First Order Logic and Automated Theorem Proving, 2nd ed., Springer Verlag, New York. 1st edition appeared in 1990.CrossRefGoogle Scholar
  17. Gallier, J., Narendran, P., Plaisted, D. & Snyder, W. [1988], ‘Rigid E-unification in NP-complete’, in Proc. IEEE Conference on Logic in Computer Science (LICS), IEEE Computer Society Press, pp. 338–346.Google Scholar
  18. Gallier, J., Narendran, P., Raatz, S. & Snyder, W. [1992], ‘Theorem proving using equational matings and rigid E-unification’, Journal of the Association for Computing Machinery 39 (2), 377–429.CrossRefGoogle Scholar
  19. Gallier, J., Raatz, S. & Snyder, W. [1987], ‘Theorem proving using rigid E-unification: Equational matings’, in Proc. IEEE Conference on Logic in Computer Science (LICS), IEEE Computer Society Press, pp. 338–346.Google Scholar
  20. Gentzen, G. [1934], ‘Untersuchungen über das logische Schließen’, Mathematical Zeitschrift 39, 176–210, 405–431. Translated as Gentzen [1969].CrossRefGoogle Scholar
  21. Gentzen, G. [1936], ‘Die Wiederspruchsfreiheit der reinen Zahlentheorie’, Mathematische Annalen 112, 493–565.CrossRefGoogle Scholar
  22. Gentzen, G. [1969], ‘Investigations into logical deduction’, in M. Szabo (ed.), The Collected Papers of Gerhard Gentzen, North-Holland, Amsterdam, pp. 68–131. Originally appeared as Gentzen [1934].Google Scholar
  23. Gilmore, P. [1960], ‘A proof method for quantification theory: its justification and realization’, IBM J. of Research and Development 4, 28–35. Reprinted as Gilmore [1983].CrossRefGoogle Scholar
  24. Gilmore, P. [1983], ‘A proof method for quantification theory: its justification and realization’, in J. Siekmann & G. Wrightson (eds.), Automation of Reasoning. Classical Papers on Google Scholar
  25. Computational Logic, Vol. 1, Springer Verlag, pp. 151-158. Originally published as Gilmore [1960].Google Scholar
  26. Girard, J.-Y. [1987], Proof Theory and Logical Complexity, Studies in Proof Theory, Bibliopolis, Napoly.Google Scholar
  27. Gödel, K. [1930], ‘Die Vollständigkeit der axiome des logischen funktionenkalküls’, Monatshefte für Mathematik und Physik 37, 349–360.CrossRefGoogle Scholar
  28. Goubault, J. [1994], ‘Rigid E-unifiability is DEXPTIME-complete’, in Proc. IEEE Conference on Logic in Computer Science (LICS), IEEE Computer Society Press.Google Scholar
  29. Hintikka, K. [1955], ‘Form and content in quantification theory’, Acta Philosophica Fennica 8, 7–55.Google Scholar
  30. Joyner jr, W. [1976], ‘Resolution strategies as decision procedures’, Journal of the Association for Computing Machinery 23, 398–417.CrossRefGoogle Scholar
  31. Kallick, B. [1968], ‘A decision procedure based on the resolution method’, in IFIP’68, North-Holland, pp. 365-377.Google Scholar
  32. Kanger, S. [1957], Provability in Logic, Vol. 1 of Studies in Philosophy, Almqvist and Wicksell, Stockholm.Google Scholar
  33. Kanger, S. [1959], Handbook in logic, Stockholm.Google Scholar
  34. Kanger, S. [1963], ‘A simplified proof method for elementary logic’, in P. Braffort & D. Hirschberg (eds.), Computer Programming and Formal Systems, North-Holland, pp. 87-94. Reprinted as Kanger [1983].Google Scholar
  35. Kanger, S. [1983], ‘A simplified proof method for elementary logic’, in J. Siekmann & G. Wrightson (eds.), Automation of Reasoning. Classical Papers on Computational Logic, Vol. 1, Springer Verlag, pp. 364-371. Originally published as Kanger [1983].Google Scholar
  36. Ketonen, O. [1944], ‘Untersuchungen zum Prädikatenkalkül’, Annales Academia Scientiarum Fennicae 23. Ser. A, I Mathematixa-physica.Google Scholar
  37. Kleene, S. [1952], Introduction to Metamathematics, Van Nostrand P.C., Amsterdam.Google Scholar
  38. Kleene, S. [1967], Mathematical Logic, John Wiley and Sons.Google Scholar
  39. Knuth, D. & Bendix, P. [1970], ‘Simple word problems in universal algebras’, in J. Leech (ed.), Computational Problems in Abstract Algebra, Pergamon Press, Oxford, pp. 263–297.Google Scholar
  40. Leitsch, A., Fermüller, C. & Tammet, T. [1999], ‘Resolution decision procedures’, in A. Robinson & A. Voronkov (eds.), Handbook of Automated Reasoning, Elsevier Science and MIT Press. To appear.Google Scholar
  41. Lifschitz, V. [1967], ‘A normal form of derivations in predicate calculus with equality and function symbols (in Russian)’, Zapiski Nauchnyh Seminarov LOMI 4, 58–64. English Translation in: Seminars in Mathematics: Steklov Math. Inst. 4, Consultants Bureau, NY-London, 1969.Google Scholar
  42. Maslov, S. [1964], ‘The inverse method of establishing deducibility in the classical predicate calculus’, Soviet Mathematical Doklady 5, 1420–1424.Google Scholar
  43. Maslov, S. [1968], ‘The inverse method of establishing deducibility of logical calculi (in Russian)’, in Collected Works of MIAN, Vol. 98, Nauka, Moscow, pp. 26–87.Google Scholar
  44. Maslov, S. [1971], ‘The generalization of the inverse method to predicate calculus with equality (in Russian)’, Zapiski Nauchnyh Seminarov LOMI 20, 80–96. English translation in: Journal of Soviet Mathematics 1, no. 1.Google Scholar
  45. Maslov, S. & Mints, G. [1983], ‘The proof-search theory and the inverse method (in Russian)’, in M.G. (ed.), Mathematical Logic and Automatic Theorem Proving, Nauka, Moscow, pp. 291–314.Google Scholar
  46. Maslov, S., Mints, G. & Orevkov, V. [1983], ‘Mechanical proof-search and the theory of logical deduction in the USSR’, in J. Siekmann & G. Wrightson (eds.), Automation of Reasoning (Classical papers on Computational Logic), Vol. 1, Springer Verlag, pp. 29–38.Google Scholar
  47. Matulis, V. [1962], ‘Two variants of classical predicate calculus without structure rules (in Russian)’, Soviet Mathematical Doklady 147 (5), 1029–1031.Google Scholar
  48. Mints, G., Degtyarev, A., Tammet, T. & Voronkov, A. [1999], ‘The inverse method’, in A. Robinson & A. Voronkov (eds.), Handbook of Automated Reasoning, Elsevier Science and MIT Press. To appear.Google Scholar
  49. Nelson G. & Oppen D. [1980] ‘Fast decision procedures based on congruence closure’ Journal of the Association for Computing Machinery 27(2) 356–364CrossRefGoogle Scholar
  50. Norgela, S. [1974], ‘On the size of derivations under minus-normalization (in Russian)’, in V. Smirnov (ed.), The Theory of Logical Inference, Institute of Philosophy, Moscow.Google Scholar
  51. Orevkov, V. [1969], ‘On nonlengthening applications of equality rules (in Russian)‘, Zapiski Nauchnyh Seminarov LOMI 16, 152–156. English translation in: Seminars in Mathematics: Steklov Math. Inst. 16, Consultants Bureau, NY-London, 1971, pp. 77–79.Google Scholar
  52. Plaisted, D. [1995], Special cases and substitutes for rigid E-unification, Technical Report MPI-I-95-2-010, Max-Planck-Institut für Informatik.Google Scholar
  53. Prawitz, D. [1960], ‘An improved proof procedure’, Theoria 26, 102–139. Reprinted as Prawitz [1983].CrossRefGoogle Scholar
  54. Prawitz, D. [1983], ‘An improved proof procedure’, in J. Siekmann & G. Wrightson (eds.), Automation of Reasoning. Classical Papers on Computational Logic, Vol. 1, Springer Verlag, pp. 162–201. Originally appeared as Prawitz [1960].Google Scholar
  55. Prawitz, D., Prawitz, H. & Voghera, N. [1960], ‘A mechanical proof procedure and its realization in an electronic computer’, Jou rnal of the Association for Computing Machinery 7 (2). Reprinted as Prawitz, Prawitz & Voghera [1983].Google Scholar
  56. Prawitz, D., Prawitz, H. & Voghera, N. [1983], ‘A mechanical proof procedure and its realization in an electronic computer’, in J. Siekmann & G. Wrightson (eds.), Automation of Reasoning. Classical Papers on Computational Logic, Vol. 1, Springer Verlag, pp. 162–201. Originally appeared as Prawitz et al. [1960].Google Scholar
  57. Quine, W. [1955], ‘A proof procedure for quantification theory’, Journal of Symbolic Logic 20, 141–149.CrossRefGoogle Scholar
  58. Robinson, G. & Wos, L. [1969], ‘Paramodulation and theorem-proving in first order theories with equality’, in B. Meltzer & D. Michie (eds.), Machine Intelligence, Vol. 4, Edinburgh University Press, pp. 135–150.Google Scholar
  59. Robinson, J. [1965], ‘A machine-oriented logic based on the resolution principle’, Journal of the Association for Computing Machinery 12 (1), 23–41.CrossRefGoogle Scholar
  60. Schü;tte, K. [1956], ‘Ein System des verknüpfenden Schliessens’, Archiv für Mathematische Logik und Grundlagenforschung 2, 34–67.Google Scholar
  61. Shostak, R. [1978], ‘An algorithm for reasoning about equality’, Communications of the ACM 21, 583–585.CrossRefGoogle Scholar
  62. Smullyan, R. [1968], First-Order Logic, Springer Verlag.Google Scholar
  63. Veanes, M. [1997a], On Simultaneous Rigid E-Unification, PhD thesis, Uppsala University.Google Scholar
  64. Veanes, M. [1997b], ‘The undecidability of simultaneous rigid E-unification with two variables’, in G. Gottlob, A. Leitsch & D. Mundici (eds.), Computational Logic and Proof Theory. 5th Kurt Gödel Colloquium, KGC-97, Vol. 1289 of Lecture Notes in Computer Science, Vienna, Austria, pp. 305–318.Google Scholar
  65. Voronkov, A. [1988], ‘A proof search method for first order logic’, in Preliminary Proceedings of COLOG-88, Vol. 2, Tallinn, pp. 104–118.Google Scholar
  66. Voronkov, A. [1992], ‘Theorem proving in non-standard logics based on the inverse method’, in D. Kapur (ed.), 11th International Conference on Automated Deduction, Vol. 607 of Lecture Notes in Artificial Intelligence, Springer Verlag, Saratoga Springs, NY, USA, pp. 648–662.Google Scholar
  67. Voronkov, A. [1998a], ‘Herbrand’s theorem, automated reasoning and semantic tableaux’, in Proc. IEEE Conference on Logic in Computer Science (LICS), IEEE Computer Society Press, pp. 252–263.Google Scholar
  68. Voronkov, A. [1998b], Simultaneous rigid E-unification and other decision problems related to Herbrand’s theorem, UPMAIL Technical Report 152, Uppsala University, Computing Science Department. To appear in Theoretical Computer Science.Google Scholar
  69. Wang, H. [1960], ‘Towards mechanical mathematics’, IBM J. of Research and Development 4, 2–22. Reprinted as Wang [1983].Google Scholar
  70. Wang, H. [1983], ‘Towards mechanical mathematics’, in J. Siekmann & G. Wrightson (eds.), Automation of Reasoning. Classical Papers on Computational Logic, Vol. 1, Springer Verlag, pp. 244–264. Originally published as Wang [1960].Google Scholar
  71. Wos, L., Robinson, G., Carson, D. & Shalla, L. [1967], ‘The concept of demodulation in theorem proving’, Journal of the Association for Computing Machinery 14, 698–709.CrossRefGoogle Scholar

Copyright information

© Springer Science+Business Media Dordrecht 2001

Authors and Affiliations

  • Anatoli Degtyarev
    • 1
  • Andrei Voronkov
    • 1
  1. 1.Computing Science DepartmentUppsala UniversitySweden

Personalised recommendations