Automath
Automath was een formele taal die vanaf 1967 door Nicolaas Govert de Bruijn werd ontwikkeld, die bedoeld was wiskundige theorieën zodanig uit te drukken dat de bijbehorende automatische bewijschecker de juistheid ervan kon verifiëren. Het Automath-systeem bevatte vele nieuwe ideeën die later werden overgenomen of opnieuw werden uitgevonden in gebieden als de getypeerde lambda-calculus en de expliciete substitutie. Afhankelijke typen zijn daarvan een voorbeeld. Automath was het eerste praktische systeem dat gebruikmaakte van de Curry-Howard-correspondentie.
Proposities werden weergegeven als verzamelingen van hun bewijzen, in Automath "categorieën" genoemd. De vraag of een propositie bewijsbaarheid was, werd een kwestie van het niet-leegzijn van de verzameling; de Bruijn was niet op de hoogte van Howards werk en stelde deze correspondentie onafhankelijk van hem op.[1]
Aangezien Automath op dat moment nooit echt duidelijk in de publiciteit kwam, werd het niet breed toegepast; het bleek echter zeer invloedrijk in de latere ontwikkeling van logische raamwerken en bewijsassistenten.[2][3]
Externe links
- (en) The Automath Archive (mirror)
- (en) Automath door Freek Wiedijk
- ↑ (en) Morten Heine Sørensen, Paweł Urzyczyn, Lectures on the Curry-Howard isomorphism, Elsevier, 2006, ISBN 0444520775, blz. 98-99
- ↑ (en) R.P. Nederpelt, J.H. Geuvers, R.C. de Vrijer (1994) Selected Papers op Automath. deel. 133 van Studies Logic, Elsevier, Amsterdam. ISBN 0-444-89822-0.
- ↑ (en) F. Kamareddine (2003) Thirty-five years of automating mathematics. Werkshop, Dordrecht, Boston, gepubliceerd door Kluwer Academic Publishers, ISBN 1402016565.
Content Disclaimer
Informasi ini disarikan dari Wikipedia dan disajikan kembali untuk tujuan edukasi. Konten tersedia di bawah lisensi CC BY-SA 3.0. Kami tidak bertanggung jawab atas ketidakakuratan data yang bersumber dari kontribusi publik tersebut.
- The information displayed on this website is sourced in part or in whole from Wikipedia and has been adapted for the purpose of restating it. We strive to provide accurate and relevant information, however:
- There is no guarantee of absolute accuracy. Wikipedia is an open, collaborative project that can be edited by anyone, so information is subject to change.
- It is not intended to constitute professional advice. The content displayed is for informational and educational purposes only. For important decisions (e.g., medical, legal, or financial), please consult a professional.
- Content copyright. Wikipedia is licensed under the Creative Commons Attribution-ShareAlike License (CC BY-SA). This means that content may be reused with appropriate attribution and shared under a similar license.
- Responsible use. Any risk arising from the use of information from this website is entirely the responsibility of the user.