Skip to main content
SpringerLink
Log in

Kanger’s Choices in Automated Reasoning

  • Chapter
Collected Papers of Stig Kanger with Essays on His Life and Work

Part of the book series: Synthese Library ((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.

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 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 109.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.

References

  • Ackermann, W. [1954], Solvable Cases of the Decision Problem, North-Holland.

    Google Scholar 

  • 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 

  • 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 

  • Beth, E. [1955], ‘Semantic entailment and formal derivability’, Mededelinger der Koninklijke Nederlandse Akademie van Wetenschappen, Afd. Letterkunde, Nieuwe Reeks 18 (13).

    Google Scholar 

  • Beth, E. [1959], The Foundation of Mathematics, North-Holland Publ. Co., Amsterdam.

    Google Scholar 

  • 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 

  • 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 

  • 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 

  • 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 

  • 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.

    Chapter  Google Scholar 

  • Degtyarev, A. & Voronkov, A. [1996b], ‘The undecidability of simultaneous rigid E-unification’, Theoretical Computer Science 166 (1–2), 291–300.

    Article  Google Scholar 

  • 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 

  • Degtyarev, A. & Voronkov, A. [1998b], ‘What you always wanted to know about rigid E-unification’, Journal of Automated Reasoning 20 (1), 47–80.

    Article  Google Scholar 

  • 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 

  • 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 

  • Fitting, M. [1996], First Order Logic and Automated Theorem Proving, 2nd ed., Springer Verlag, New York. 1st edition appeared in 1990.

    Book  Google Scholar 

  • 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 

  • 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.

    Article  Google Scholar 

  • 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 

  • Gentzen, G. [1934], ‘Untersuchungen über das logische Schließen’, Mathematical Zeitschrift 39, 176–210, 405–431. Translated as Gentzen [1969].

    Article  Google Scholar 

  • Gentzen, G. [1936], ‘Die Wiederspruchsfreiheit der reinen Zahlentheorie’, Mathematische Annalen 112, 493–565.

    Article  Google Scholar 

  • 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 

  • 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].

    Article  Google Scholar 

  • 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 

  • Computational Logic, Vol. 1, Springer Verlag, pp. 151-158. Originally published as Gilmore [1960].

    Google Scholar 

  • Girard, J.-Y. [1987], Proof Theory and Logical Complexity, Studies in Proof Theory, Bibliopolis, Napoly.

    Google Scholar 

  • Gödel, K. [1930], ‘Die Vollständigkeit der axiome des logischen funktionenkalküls’, Monatshefte für Mathematik und Physik 37, 349–360.

    Article  Google Scholar 

  • 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 

  • Hintikka, K. [1955], ‘Form and content in quantification theory’, Acta Philosophica Fennica 8, 7–55.

    Google Scholar 

  • Joyner jr, W. [1976], ‘Resolution strategies as decision procedures’, Journal of the Association for Computing Machinery 23, 398–417.

    Article  Google Scholar 

  • Kallick, B. [1968], ‘A decision procedure based on the resolution method’, in IFIP’68, North-Holland, pp. 365-377.

    Google Scholar 

  • Kanger, S. [1957], Provability in Logic, Vol. 1 of Studies in Philosophy, Almqvist and Wicksell, Stockholm.

    Google Scholar 

  • Kanger, S. [1959], Handbook in logic, Stockholm.

    Google Scholar 

  • 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 

  • 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 

  • Ketonen, O. [1944], ‘Untersuchungen zum Prädikatenkalkül’, Annales Academia Scientiarum Fennicae 23. Ser. A, I Mathematixa-physica.

    Google Scholar 

  • Kleene, S. [1952], Introduction to Metamathematics, Van Nostrand P.C., Amsterdam.

    Google Scholar 

  • Kleene, S. [1967], Mathematical Logic, John Wiley and Sons.

    Google Scholar 

  • 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 

  • 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 

  • 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 

  • Maslov, S. [1964], ‘The inverse method of establishing deducibility in the classical predicate calculus’, Soviet Mathematical Doklady 5, 1420–1424.

    Google Scholar 

  • 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 

  • 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 

  • 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 

  • 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 

  • Matulis, V. [1962], ‘Two variants of classical predicate calculus without structure rules (in Russian)’, Soviet Mathematical Doklady 147 (5), 1029–1031.

    Google Scholar 

  • 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 

  • Nelson G. & Oppen D. [1980] ‘Fast decision procedures based on congruence closure’ Journal of the Association for Computing Machinery 27(2) 356–364

    Article  Google Scholar 

  • 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 

  • 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 

  • 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 

  • Prawitz, D. [1960], ‘An improved proof procedure’, Theoria 26, 102–139. Reprinted as Prawitz [1983].

    Article  Google Scholar 

  • 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 

  • 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 

  • 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 

  • Quine, W. [1955], ‘A proof procedure for quantification theory’, Journal of Symbolic Logic 20, 141–149.

    Article  Google Scholar 

  • 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 

  • Robinson, J. [1965], ‘A machine-oriented logic based on the resolution principle’, Journal of the Association for Computing Machinery 12 (1), 23–41.

    Article  Google Scholar 

  • Schü;tte, K. [1956], ‘Ein System des verknüpfenden Schliessens’, Archiv für Mathematische Logik und Grundlagenforschung 2, 34–67.

    Google Scholar 

  • Shostak, R. [1978], ‘An algorithm for reasoning about equality’, Communications of the ACM 21, 583–585.

    Article  Google Scholar 

  • Smullyan, R. [1968], First-Order Logic, Springer Verlag.

    Google Scholar 

  • Veanes, M. [1997a], On Simultaneous Rigid E-Unification, PhD thesis, Uppsala University.

    Google Scholar 

  • 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 

  • 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 

  • 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 

  • 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 

  • 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 

  • Wang, H. [1960], ‘Towards mechanical mathematics’, IBM J. of Research and Development 4, 2–22. Reprinted as Wang [1983].

    Google Scholar 

  • 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 

  • 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.

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computing Science Department, Uppsala University, Sweden

    Anatoli Degtyarev & Andrei Voronkov

Authors
  1. Anatoli Degtyarev
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Andrei Voronkov
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Boston University, Boston, USA

    Ghita Holmström-Hintikka

  2. Umeå University, Umeå, Sweden

    Sten Lindström

  3. Uppsala University, Uppsala, Sweden

    Rysiek Sliwinski

Rights and permissions

Reprints and permissions

Copyright information

© 2001 Springer Science+Business Media Dordrecht

About this chapter

Cite this chapter

Degtyarev, A., Voronkov, A. (2001). Kanger’s Choices in Automated Reasoning. In: Holmström-Hintikka, G., Lindström, S., Sliwinski, R. (eds) Collected Papers of Stig Kanger with Essays on His Life and Work. Synthese Library, vol 304. Springer, Dordrecht. https://doi.org/10.1007/978-94-010-0630-9_4

Download citation

  • DOI: https://doi.org/10.1007/978-94-010-0630-9_4

  • Publisher Name: Springer, Dordrecht

  • Print ISBN: 978-1-4020-0112-3

  • Online ISBN: 978-94-010-0630-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation