Skip to main content

2014 | OriginalPaper | Buchkapitel

5. A Proof and Some Representations

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

Hilbert defined proofs as derivations from axioms via the modus ponens rule and variable instantiation (this definition has a certain parallel to the ‘recognise-act cycle’ in artificial intelligence). A pre-defined set of rules is applied to an initial state until a goal state is reached. Although this definition is very powerful and it can be argued that nothing else is needed, the nature of proof turns out to be much more diverse, for instance, changes in representation are frequently done. We will explore some aspects of this by McCarthy’s ‘mutilated checkerboard’ problem and discuss the tension between the complexity and the power of mechanisms for finding proofs.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Literatur
Zurück zum Zitat Ayer AJ (1936) Language, truth and logic, 2nd edn. Victor Gollancz Ltd, London Ayer AJ (1936) Language, truth and logic, 2nd edn. Victor Gollancz Ltd, London
Zurück zum Zitat Bancerek G (1995) The mutilated chessboard problem—checked by MIZAR. In: Matuszewski R (ed) The QED Workshop II, Warsaw University, pp 37–38 Bancerek G (1995) The mutilated chessboard problem—checked by MIZAR. In: Matuszewski R (ed) The QED Workshop II, Warsaw University, pp 37–38
Zurück zum Zitat Feynman RP (1985) Surely you’re joking Mr. Feynman, Vintage, London Feynman RP (1985) Surely you’re joking Mr. Feynman, Vintage, London
Zurück zum Zitat Hardy G (1940) A mathematician’s apology. Cambridge University Press, London Hardy G (1940) A mathematician’s apology. Cambridge University Press, London
Zurück zum Zitat Herbrand J (1930) Recherches sur la théorie de la démonstration. Sci Lett Varsovie, Classe III Sci Math Phys 33 Herbrand J (1930) Recherches sur la théorie de la démonstration. Sci Lett Varsovie, Classe III Sci Math Phys 33
Zurück zum Zitat Jamnik M, Kerber M, Pollet M, Benzmüller C (2003) Automatic learning of proof methods in proof planning. Logic J IGPL 11(6):647–673 Jamnik M, Kerber M, Pollet M, Benzmüller C (2003) Automatic learning of proof methods in proof planning. Logic J IGPL 11(6):647–673
Zurück zum Zitat Kerber M, Pollet M (2006) A tough nut for mathematical knowledge management. In: Kohlhase M (ed) Mathematical knowledge management—4th international conference, MKM 2005. Springer, LNAI 3863. Bremen, Germany, pp 81–95 Kerber M, Pollet M (2006) A tough nut for mathematical knowledge management. In: Kohlhase M (ed) Mathematical knowledge management—4th international conference, MKM 2005. Springer, LNAI 3863. Bremen, Germany, pp 81–95
Zurück zum Zitat McCarthy J (1964) A tough nut for proof procedures. AI Project Memo 16. Stanford University, Stanford, California, USA McCarthy J (1964) A tough nut for proof procedures. AI Project Memo 16. Stanford University, Stanford, California, USA
Zurück zum Zitat Robinson JA (1965) A machine oriented logic based on the resolution principle. JACM 12:23–41CrossRefMATH Robinson JA (1965) A machine oriented logic based on the resolution principle. JACM 12:23–41CrossRefMATH
Zurück zum Zitat Sloman A (1996) What sort of architecture is required for a human-like agent? In: Rao RK (ed) Foundations of rational agency. Kluwer, The Netherlands Sloman A (1996) What sort of architecture is required for a human-like agent? In: Rao RK (ed) Foundations of rational agency. Kluwer, The Netherlands
Zurück zum Zitat Zinn C (2004) Understanding informal mathematical discourse. PhD thesis, Friedrich-Alexander Universität Erlangen-Nürnberg Zinn C (2004) Understanding informal mathematical discourse. PhD thesis, Friedrich-Alexander Universität Erlangen-Nürnberg
Metadaten
Titel
A Proof and Some Representations
verfasst von
Manfred Kerber
Copyright-Jahr
2014
DOI
https://doi.org/10.1007/978-3-319-06614-1_5

Premium Partner