DE
Published in:

2020 | OriginalPaper | Chapter

# 3. Logical Thinking Becomes Automatic

Author : Klaus Mainzer

Publisher: Springer Berlin Heidelberg

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

search-config

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

### 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
• 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
• 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
• Finance + Banking
• Management + Führung
• Marketing + Vertrieb
• Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Literature
1.
Robinson JA (1965) A machine oriented logic based on the resolution principle. J Assoc Comput Mach 12:23–41 CrossRef
2.
Richter MM (1978) Logikkalküle. Teubner, Stuttgart, p 185 CrossRef
3.
Schöning U (1987) Logic for computer scientists. B.I. Wissenschaftsverlag, Mannheim, p 85
4.
Kowalski B (1979) Logic for problem solving. North-Holland, New York
5.
Hanus M (1986) Problem solving in PROLOG. Vieweg + Teubner, Stuttgart, Germany
6.
Schefe P (1987) Computer Science—a constructive introduction. LISP, PROLOG and other programming concepts. B.I. Wissenschaftsverlag, Mannheim, p 285
7.
Church A (1941) The Calculi of lambda-conversion. Library of America, Princeton (repr. New York 1965)
8.
McCarthy J et al (1960) LISP 1 programmer’s manual. MIT Computer Center and Research Lab. Electronics, Cambridge (Mass.)
9.
Stoyan H, Goerz G (1984) LISP—an introduction to programming. Springer, Berlin
10.
Hermes H (1978) Enumerability, decidability, computability. Introduction to the theory of recursive functions, 3rd edn. Springer, Berlin (1st ed. 1961)
11.
Brauer W, Indermark K (1968) Algorithms, recursive functions and formal languages. B.I. Wissenschaftsverlag, Mannheim
12.
Chaitin G (1998) The limits of mathematics. Springer, Singapore
13.
Gentzen G (1938) The present situation in mathematical foundational research. Ger Math 3:260
14.
15.
Arora S, Barak B (2009) Computational complexity. A modern approach. Cambridge University Press, Cambridge CrossRef
16.
Wegener I (2003) Complexity theory. Limits of the efficiency of algorithms. Springer, Berlin
17.
Aigner M, Ziegler GM (2001) Proofs from The book, 2nd edn. Springer, Berlin, p 3 CrossRef
18.
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.
Kohlenbach U (2008) Applied proof theory: Proof interpretations and their use in mathematics. Springer, Berlin (Chapter 2)
20.
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.
Schwichtenberg H, Wainer SS (2012) Proofs and computations. Cambridge University Press, Cambridge (Chapter 7)
22.
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.
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.
Coquand T, Huet G (1988) The calculus of constructions. Inf Comput 76(2–3):95–120 CrossRef
25.
Bertot Y, Castéran P (2004) Interactive theorem proving and program development. Coq’Art: the calculus of inductive constructions. Springer, New York CrossRef
26.
Coupet-Grimal S, Jakubiec L (1996) Coq and hardware verification: a Case Study. TPHOLs ‚96, LCNS 1125:125–139
27.
Mainzer K, Schuster P, Schwichtenberg H (2018) Proof and computation. Digitization in mathematics, computer science, and philosophy. World Scientific Publisher, Singapore CrossRef
28.
Mainzer K (2018) The digital and the real world. Computational foundations of mathematics, science, technology, and philosophy. World Scientific Publisher, Singapore CrossRef