Advertisement

Logisches Denken wird automatisch

  • Klaus MainzerEmail author
Chapter
Part of the Technik im Fokus book series (TECHNIK)

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. \( \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.

Literatur

  1. 1.
    Robinson JA (1965) A machine oriented logic based on the resolution principle. Journal of the Association for Computing Machinery 12:23–41CrossRefGoogle Scholar
  2. 2.
    Richter MM (1978) Logikkalküle. Teubner, Stuttgart, S 185CrossRefGoogle Scholar
  3. 3.
    Schöning U (1987) Logik für Informatiker. B.I. Wissenschaftsverlag, Mannheim, S 85Google Scholar
  4. 4.
    Kowalski B (1979) Logic for Problem Solving. North-Holland: New York.Google Scholar
  5. 5.
    Hanus M (1986) Problemlösen in PROLOG. Vieweg+Teubner, StuttgartGoogle Scholar
  6. 6.
    Schefe P (1987) Informatik – Eine konstruktive Einführung. LISP, PROLOG und andere Konzepte der Programmierung. B.I. Wissenschaftsverlag, Mannheim, S 285Google Scholar
  7. 7.
    Church A (1941) The Calculi of Lambda-Conversion. Library of America, Princeton (repr. New York 1965)Google Scholar
  8. 8.
    McCarthy J et al (1960) LISP 1 Programmer’s Manual. MIT Computer Center and Research Lab. Electronics, Cambridge (Mass.)Google Scholar
  9. 9.
    Stoyan H, Goerz G (1984) LISP – Eine Einführung in die Programmierung. Springer, BerlinGoogle Scholar
  10. 10.
    Hermes H (1978) Aufzählbarkeit, Entscheidbarkeit, Berechenbarkeit. Einführung in die Theorie der rekursiven Funktionen, 3. Aufl. Springer, Berlin (1. Aufl. 1961)CrossRefGoogle Scholar
  11. 11.
    Brauer W, Indermark K (1968) Algorithmen, rekursive Funktionen und formale Sprachen. B.I. Wissenschaftsverlag, MannheimGoogle Scholar
  12. 12.
    Chaitin G (1998) The Limits of Mathematics. Springer, SingaporeGoogle Scholar
  13. 13.
    Gentzen G (1938) Die gegenwärtige Lage in der mathematischen Grundlagenforschung. Deutsche Mathematik 3:260Google Scholar
  14. 14.
    Shoenfield JR (1967) Mathematical Logic. Addison Wesley, Reading (Mass.)Google Scholar
  15. 15.
    Arora S, Barak B (2009) Computational Complexity. A Modern Approach. Cambridge University Press, CambridgeCrossRefGoogle Scholar
  16. 16.
    Wegener I (2003) Komplexitätstheorie. Grenzen der Effizienz von Algorithmen. Springer, BerlinGoogle Scholar
  17. 17.
    Aigner M, Ziegler GM (2001) Proofs from The Book, 2. Aufl. Springer, Berlin, S 3Google Scholar
  18. 18.
    Feferman S (1996) Kreisel’s „unwinding“ Program. In: Odifreddi P (Hrsg) Kreisleriana. About and Around Georg Kreisel, Review of Modern Logic, S 247–273Google Scholar
  19. 19.
    Kohlenbach U (2008) Applied Proof Theory: Proof Interpretations and Their Use in Mathematics. Springer, Berlin (Chapter 2)Google Scholar
  20. 20.
    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–157CrossRefGoogle Scholar
  21. 21.
    Schwichtenberg H, Wainer SS (2012) Proofs and Computations. Cambridge University Press, Cambridge (Chapter 7)Google Scholar
  22. 22.
    Mayr E, Prömel H, Steger A (Hrsg) (1998) Lectures on Proof Verification and Approximation Algorithms. Lecture Notes in Computer Science, Bd. 1967. Springer, BerlinGoogle Scholar

Copyright information

© Springer-Verlag GmbH Deutschland, ein Teil von Springer Nature 2019

Authors and Affiliations

  1. 1.Technische Universität MünchenMünchenDeutschland

Personalised recommendations