Zusammenfassung
In der ersten Phase der KI‐Forschung war die Suche nach allgemeinen Problemlösungsverfahren wenigstens in der formalen Logik erfolgreich. Dort wurde ein mechanisches Verfahren angegeben, um die logische Allgemeingültigkeit von Formeln zu beweisen. Das Verfahren konnte auch von einem Computerprogramm ausgeführt werden und leitete in der Informatik das automatische Beweisen ein.
Der Grundgedanke ist einfach zu verstehen. In der Algebra werden Buchstaben x, y, z, … durch Rechenoperationen wie z. B. Addieren (+) oder Subtrahieren (−) verbunden. Die Buchstaben dienen als Leerstellen (Variablen), um Zahlen einzusetzen. In der formalen Logik werden Aussagen durch Variablen A, B, C, … bezeichnet, die durch logische Junktoren wie z. B. „und“ (\( \wedge \)), „oder“ (\( \vee \))‚ „wenn‐dann“ (\( \rightarrow \)), „nicht“ (\( \lnot \)) verbunden werden. Die Aussagenvariablen dienen als Leerstellen, um Aussagen einzusetzen, die entweder wahr oder falsch sind. So ist z. B. A \( \wedge \) B eine logische Formel, die durch Einsetzung der wahren Aussagen 1 + 3 = 4 für A und 4 = 2 + 2 für B in die wahre Aussage 1 + 3 = 4 \( \wedge \) 4 = 2 + 2 übergeht. In der Arithmetik ergibt sich daraus der wahre Schluss 1 + 3 = 4 \( \wedge \) 4 = 2 + 2 \( \rightarrow \) 1 + 3 = 2 + 2. Allgemein ist aber der Schluss A \( \wedge \) B \( \rightarrow \) C nicht wahr. Demgegenüber ist der Schluss A \( \wedge \) B \( \rightarrow \) A logisch allgemeingültig, da für die Einsetzung von beliebigen wahren oder falschen Aussagen für A und B sich immer eine wahre Gesamtaussage ergibt.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Literatur
Robinson JA (1965) A machine oriented logic based on the resolution principle. Journal of the Association for Computing Machinery 12:23–41
Richter MM (1978) Logikkalküle. Teubner, Stuttgart, S 185
Schöning U (1987) Logik für Informatiker. B.I. Wissenschaftsverlag, Mannheim, S 85
Kowalski B (1979) Logic for Problem Solving. North-Holland: New York.
Hanus M (1986) Problemlösen in PROLOG. Vieweg+Teubner, Stuttgart
Schefe P (1987) Informatik – Eine konstruktive Einführung. LISP, PROLOG und andere Konzepte der Programmierung. B.I. Wissenschaftsverlag, Mannheim, S 285
Church A (1941) The Calculi of Lambda-Conversion. Library of America, Princeton (repr. New York 1965)
McCarthy J et al (1960) LISP 1 Programmer’s Manual. MIT Computer Center and Research Lab. Electronics, Cambridge (Mass.)
Stoyan H, Goerz G (1984) LISP – Eine Einführung in die Programmierung. Springer, Berlin
Hermes H (1978) Aufzählbarkeit, Entscheidbarkeit, Berechenbarkeit. Einführung in die Theorie der rekursiven Funktionen, 3. Aufl. Springer, Berlin (1. Aufl. 1961)
Brauer W, Indermark K (1968) Algorithmen, rekursive Funktionen und formale Sprachen. B.I. Wissenschaftsverlag, Mannheim
Chaitin G (1998) The Limits of Mathematics. Springer, Singapore
Gentzen G (1938) Die gegenwärtige Lage in der mathematischen Grundlagenforschung. Deutsche Mathematik 3:260
Shoenfield JR (1967) Mathematical Logic. Addison Wesley, Reading (Mass.)
Arora S, Barak B (2009) Computational Complexity. A Modern Approach. Cambridge University Press, Cambridge
Wegener I (2003) Komplexitätstheorie. Grenzen der Effizienz von Algorithmen. Springer, Berlin
Aigner M, Ziegler GM (2001) Proofs from The Book, 2. Aufl. Springer, Berlin, S 3
Feferman S (1996) Kreisel’s „unwinding“ Program. In: Odifreddi P (Hrsg) Kreisleriana. About and Around Georg Kreisel, Review of Modern Logic, S 247–273
Kohlenbach U (2008) Applied Proof Theory: Proof Interpretations and Their Use in Mathematics. Springer, Berlin (Chapter 2)
Schwichtenberg H (2006) Minlog. In: Wiedijk F (Hrsg) The Seventeen Provers of the World. Lecture Notes in Artificial Intelligence, Bd. 3600. Springer, Berlin, S 151–157
Schwichtenberg H, Wainer SS (2012) Proofs and Computations. Cambridge University Press, Cambridge (Chapter 7)
Mayr E, Prömel H, Steger A (Hrsg) (1998) Lectures on Proof Verification and Approximation Algorithms. Lecture Notes in Computer Science, Bd. 1967. Springer, Berlin
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
Copyright information
© 2019 Springer-Verlag GmbH Deutschland, ein Teil von Springer Nature
About this chapter
Cite this chapter
Mainzer, K. (2019). Logisches Denken wird automatisch. In: Künstliche Intelligenz – Wann übernehmen die Maschinen?. Technik im Fokus. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-58046-2_3
Download citation
DOI: https://doi.org/10.1007/978-3-662-58046-2_3
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-58045-5
Online ISBN: 978-3-662-58046-2
eBook Packages: Computer Science and Engineering (German Language)