Skip to main content
Top

2020 | OriginalPaper | Chapter

3. Logical Thinking Becomes Automatic

Author : Klaus Mainzer

Published in: Artificial intelligence - When do machines take over?

Publisher: Springer Berlin Heidelberg

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

In the first phase of AI research, the search for general problem-solving methods was successful at least in formal logic. A mechanical procedure was given to prove the logical truth of formulas. The procedure could also be carried out by a computer program and introduced automatic proving in computer science.
The basic idea is easy to understand. In algebra, letters x, y, z… are used by arithmetic operations such as add (+) or subtract (−). The letters serve as spaces (variables) to insert numbers. In formal logic, propositions are represented by variables A, B, C…, which are connected by logical connectives such as (∧), “or” (∨)′ “if-then” (→), “not” (¬). The propositional variables serve as blanks to use statements that are either true or false. For example, the logical formula A ∧ B, by using the true statements 1 + 3 = 4 for A and 4 = 2 + 2 for B, is transformed into the true statement 1 + 3 = 4 ∧ 4 = 2 + 2. In arithmetic, this leads to the true conclusion 1 + 3 = 4 ∧ 4 = 2 + 2→1 + 3 = 2 + 2. But, in general, the conclusion A ∧ B → C is not true? On the other hand, the conclusion A ∧ B → A logically generally valid, since for the insertion of any true or false statements for A and B there is always a true overall statement.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Literature
1.
go back to reference Robinson JA (1965) A machine oriented logic based on the resolution principle. J Assoc Comput Mach 12:23–41 CrossRef Robinson JA (1965) A machine oriented logic based on the resolution principle. J Assoc Comput Mach 12:23–41 CrossRef
3.
go back to reference Schöning U (1987) Logic for computer scientists. B.I. Wissenschaftsverlag, Mannheim, p 85 Schöning U (1987) Logic for computer scientists. B.I. Wissenschaftsverlag, Mannheim, p 85
4.
go back to reference Kowalski B (1979) Logic for problem solving. North-Holland, New York Kowalski B (1979) Logic for problem solving. North-Holland, New York
5.
go back to reference Hanus M (1986) Problem solving in PROLOG. Vieweg + Teubner, Stuttgart, Germany Hanus M (1986) Problem solving in PROLOG. Vieweg + Teubner, Stuttgart, Germany
6.
go back to reference Schefe P (1987) Computer Science—a constructive introduction. LISP, PROLOG and other programming concepts. B.I. Wissenschaftsverlag, Mannheim, p 285 Schefe P (1987) Computer Science—a constructive introduction. LISP, PROLOG and other programming concepts. B.I. Wissenschaftsverlag, Mannheim, p 285
7.
go back to reference Church A (1941) The Calculi of lambda-conversion. Library of America, Princeton (repr. New York 1965) Church A (1941) The Calculi of lambda-conversion. Library of America, Princeton (repr. New York 1965)
8.
go back to reference McCarthy J et al (1960) LISP 1 programmer’s manual. MIT Computer Center and Research Lab. Electronics, Cambridge (Mass.) McCarthy J et al (1960) LISP 1 programmer’s manual. MIT Computer Center and Research Lab. Electronics, Cambridge (Mass.)
9.
go back to reference Stoyan H, Goerz G (1984) LISP—an introduction to programming. Springer, Berlin Stoyan H, Goerz G (1984) LISP—an introduction to programming. Springer, Berlin
10.
go back to reference Hermes H (1978) Enumerability, decidability, computability. Introduction to the theory of recursive functions, 3rd edn. Springer, Berlin (1st ed. 1961) Hermes H (1978) Enumerability, decidability, computability. Introduction to the theory of recursive functions, 3rd edn. Springer, Berlin (1st ed. 1961)
11.
go back to reference Brauer W, Indermark K (1968) Algorithms, recursive functions and formal languages. B.I. Wissenschaftsverlag, Mannheim Brauer W, Indermark K (1968) Algorithms, recursive functions and formal languages. B.I. Wissenschaftsverlag, Mannheim
12.
go back to reference Chaitin G (1998) The limits of mathematics. Springer, Singapore Chaitin G (1998) The limits of mathematics. Springer, Singapore
13.
go back to reference Gentzen G (1938) The present situation in mathematical foundational research. Ger Math 3:260 Gentzen G (1938) The present situation in mathematical foundational research. Ger Math 3:260
14.
go back to reference Shoenfield JR (1967) Mathematical logic. Addison Wesley, Reading (Mass.) Shoenfield JR (1967) Mathematical logic. Addison Wesley, Reading (Mass.)
15.
go back to reference Arora S, Barak B (2009) Computational complexity. A modern approach. Cambridge University Press, Cambridge CrossRef Arora S, Barak B (2009) Computational complexity. A modern approach. Cambridge University Press, Cambridge CrossRef
16.
go back to reference Wegener I (2003) Complexity theory. Limits of the efficiency of algorithms. Springer, Berlin Wegener I (2003) Complexity theory. Limits of the efficiency of algorithms. Springer, Berlin
17.
go back to reference Aigner M, Ziegler GM (2001) Proofs from The book, 2nd edn. Springer, Berlin, p 3 CrossRef Aigner M, Ziegler GM (2001) Proofs from The book, 2nd edn. Springer, Berlin, p 3 CrossRef
18.
go back to reference Feferman S (1996) Kreisel’s “unwinding” program. In: Odifreddi P (ed) Kreisleriana. About and Around Georg Kreisel, Review of Modern Logic, pp 247–273 Feferman S (1996) Kreisel’s “unwinding” program. In: Odifreddi P (ed) Kreisleriana. About and Around Georg Kreisel, Review of Modern Logic, pp 247–273
19.
go back to reference Kohlenbach U (2008) Applied proof theory: Proof interpretations and their use in mathematics. Springer, Berlin (Chapter 2) Kohlenbach U (2008) Applied proof theory: Proof interpretations and their use in mathematics. Springer, Berlin (Chapter 2)
20.
go back to reference Schwichtenberg H (2006) Minlog. In: Wiedijk F (ed) The seventeen provers of the world. Lecture notes in artificial intelligence, vol 3600. Springer, Berlin, pp 151–157 CrossRef Schwichtenberg H (2006) Minlog. In: Wiedijk F (ed) The seventeen provers of the world. Lecture notes in artificial intelligence, vol 3600. Springer, Berlin, pp 151–157 CrossRef
21.
go back to reference Schwichtenberg H, Wainer SS (2012) Proofs and computations. Cambridge University Press, Cambridge (Chapter 7) Schwichtenberg H, Wainer SS (2012) Proofs and computations. Cambridge University Press, Cambridge (Chapter 7)
22.
go back to reference Mayr E, Prömel H, Steger A (eds) (1998) Lectures on proof verification and approximation algorithms. Lecture notes in computer science, vol 1967. Springer, Berlin Mayr E, Prömel H, Steger A (eds) (1998) Lectures on proof verification and approximation algorithms. Lecture notes in computer science, vol 1967. Springer, Berlin
23.
go back to reference Howard WA (1969) The formulae-as-types notion of construction. In: Seldin JP, Hindley JR (eds) To H.B. Curry: essays on combinatory logic, lambda calculus and formalism. Academic Press, Boston, pp 479–490 Howard WA (1969) The formulae-as-types notion of construction. In: Seldin JP, Hindley JR (eds) To H.B. Curry: essays on combinatory logic, lambda calculus and formalism. Academic Press, Boston, pp 479–490
24.
go back to reference Coquand T, Huet G (1988) The calculus of constructions. Inf Comput 76(2–3):95–120 CrossRef Coquand T, Huet G (1988) The calculus of constructions. Inf Comput 76(2–3):95–120 CrossRef
25.
go back to reference Bertot Y, Castéran P (2004) Interactive theorem proving and program development. Coq’Art: the calculus of inductive constructions. Springer, New York CrossRef Bertot Y, Castéran P (2004) Interactive theorem proving and program development. Coq’Art: the calculus of inductive constructions. Springer, New York CrossRef
26.
go back to reference Coupet-Grimal S, Jakubiec L (1996) Coq and hardware verification: a Case Study. TPHOLs ‚96, LCNS 1125:125–139 Coupet-Grimal S, Jakubiec L (1996) Coq and hardware verification: a Case Study. TPHOLs ‚96, LCNS 1125:125–139
27.
go back to reference Mainzer K, Schuster P, Schwichtenberg H (2018) Proof and computation. Digitization in mathematics, computer science, and philosophy. World Scientific Publisher, Singapore CrossRef Mainzer K, Schuster P, Schwichtenberg H (2018) Proof and computation. Digitization in mathematics, computer science, and philosophy. World Scientific Publisher, Singapore CrossRef
28.
go back to reference Mainzer K (2018) The digital and the real world. Computational foundations of mathematics, science, technology, and philosophy. World Scientific Publisher, Singapore CrossRef Mainzer K (2018) The digital and the real world. Computational foundations of mathematics, science, technology, and philosophy. World Scientific Publisher, Singapore CrossRef
Metadata
Title
Logical Thinking Becomes Automatic
Author
Klaus Mainzer
Copyright Year
2020
Publisher
Springer Berlin Heidelberg
DOI
https://doi.org/10.1007/978-3-662-59717-0_3

Premium Partners