Automath

Automath (pour « automating mathematics ») était un langage formel, développé par Nicolaas Govert de Bruijn à partir de 1967, dont le but était d'exprimer des théories mathématiques complètes de manière à inclure un assistant de preuve qui pouvait en vérifier la correction.

Le système Automath apportait de nombreuses notions novatrices qui ont été adoptées ou réinventées ultérieurement, comme la substitution explicite ou la notion de type dépendant dont Automath est un exemple paradigmatique. Automath était aussi le premier système pratique qui exploitait la correspondance de Curry-Howard. Les propositions étaient représentées comme les ensembles (appelées « catégories ») de leurs preuves, et le problème de l'existence de preuve se ramenait à tester la vacuité d'un ensemble ; de Bruijn ne connaissait pas les travaux de Howard, et a énoncé la correspondance indépendamment[1]. Automath n'a pas été largement publié à l'époque, et n'a pas été utilisé à grande échelle ; mais c'est un système précurseur des assistants de preuve actuels[2],[3].

Références

  1. ↑ (en) Morten Heine Sørensen et Paweł Urzyczyn, Lectures on the Curry-Howard Isomorphism, North-Holland Publishing Co., coll. « Studies in Logic and the Foundations of Mathematics » (no 149), , 442 p. (ISBN 978-0-444-52077-7), p. 98-99.
  2. ↑ (en) Rob P. Nederpelt, J. H. Geuvers et Roel C. de Vrijer (éditeurs), Selected papers on Automath, Amsterdam/Lausanne/New York etc., North-Holland Publishing Co., coll. « Studies in Logic and the Foundations of Mathematics » (no 133), , xx+1024 (ISBN 978-0-444-89822-7).
  3. ↑ (en) Fairouz D. Kamareddine (éditeur), Thirty-five years of automating mathematics : Dedicated to 35 years of de Bruijn's Automath, Dordrecht, Kluwer Academic Publishers, coll. « Applied Logic Series » (no 28), , x+318 (ISBN 978-1-4020-1656-1, présentation en ligne).
(en) Cet article est partiellement ou en totalité issu de l’article de Wikipédia en anglais intitulé « Automath » (voir la liste des auteurs).

Liens internes

Liens externes

Read other articles:

Daftar lukisan Vincent van Gogh

Vincent van Gogh adalah pelukis pasca-impresionis Belanda yang merupakan salah satu pelukis terbesar dalam sejarah seni Eropa. Berikut lukisan-lukisan yang dibuat oleh Vincent van Gogh dengan judul dalam bahasa Indonesia. Lukisan Jalan setapak di taman Di ambang kekekalan Augustine Roulin dengan bayinya Petani dengan pekerjaannya Gubuk petani di Auvers Batang pohon Pemandangan desa pada waktu subuh Pemandangan Arles Pemandangan Arles dengan bunga lili Pemandangan Montmartre Pohon yang berbung...

 

 

Ermesinda

Ermesinda dari Asturias, oleh Francisco Joaquín Gutiérrez de la Vega. 1854. (Museo del Prado, Madrid). Ermesinda (skt. 720 atau skt. 730 — ?) atau Ormisenda, Ermisenda, Ermesinde, Ermessenda) adalah permaisuri Kerajaan Asturias, sebagai istri Raja Alfonsu I dari Asturias (Alfonsu yang Katolik). Dia adalah putri Raja Pelayo dari Asturias dan ratunya, Gaudiosa. Chronicon Albeldense berbahasa Latin menyatakan bahwa Ermesinda adalah putri Pelagius, raja pertama Asturias, dan ratunya, Gau...

 

 

Прощание славянки

У этого термина существуют и другие значения, см. Прощание славянки (значения). Прощание славянки Песня Дата выпуска 1912 Жанр марш Язык русский Композитор Василий Агапкин  Медиафайлы на Викискладе Марш в исполнении Оркестра береговой охраны США, 2006 год «Проща́ние сл�...

Египтопитек

† Египтопитек Реконструкция внешнего вида египтопитека Научная классификация Домен:ЭукариотыЦарство:ЖивотныеПодцарство:ЭуметазоиБез ранга:Двусторонне-симметричныеБез ранга:ВторичноротыеТип:ХордовыеПодтип:ПозвоночныеИнфратип:ЧелюстноротыеНадкласс:Четвероно...

 

 

Halte Transjakarta Karet Kuningan

615 Karet Kuningan Halte TransjakartaHalte Karet Kuningan, 2023LetakKotaJakarta SelatanDesa/kelurahanKaret Kuningan, SetiabudiKodepos12940AlamatJalan HR Rasuna SaidKoordinat6°13′02″S 106°49′51″E / 6.21729°S 106.8309°E / -6.21729; 106.8309Koordinat: 6°13′02″S 106°49′51″E / 6.21729°S 106.8309°E / -6.21729; 106.8309Desain HalteStruktur BRT, median jalan bebas 1 tengah Pintu masukJembatan penyeberangan di sudut Jalan HR...

 

 

Storia dello zoo

Storia dello zooOpera teatrale AutoreEdward Albee Titolo originaleThe Zoo Story Lingua originaleInglese Composto nel1958 Prima assoluta28 settembre 1959Schiller Theater (Berlino Ovest) PremiObie Award alla migliore opera teatrale   Manuale Storia dello zoo è un'opera teatrale del drammaturgo statunitense Edward Albee, debuttata a Berlino Ovest nel 1959. Indice 1 Trama 2 Produzioni 3 Note 4 Altri progetti 5 Collegamenti esterni Trama Peter e Jerry si incontrano su una panchina a Central ...

دوشان أوهرين

دوشان أوهرين (بالتشيكية: Dušan Uhrin)‏  معلومات شخصية الميلاد 5 فبراير 1943 (العمر 81 سنة) الطول 1.83 م (6 قدم 0 بوصة) مركز اللعب وسط الجنسية تشيكوسلوفاكيا  أبناء دوشان أوهرين جونيور  المسيرة الاحترافية1 سنوات فريق م. (هـ.) 1959–1964 FK Admira Prague [الإنجليزية]‏ 1964–1965 سلافيا �...

 

 

Gerald Wilson

American trumpetist For other people named Gerald Wilson, see Gerald Wilson (disambiguation). Gerald WilsonWilson in 2005Background informationBirth nameGerald Stanley WilsonBorn(1918-09-04)September 4, 1918Shelby, Mississippi, U.S.DiedSeptember 8, 2014(2014-09-08) (aged 96)[1]Los Angeles, California, U.S.GenresJazz, popOccupation(s)Musician, composer, bandleaderInstrument(s)TrumpetYears active1938–2012LabelsCapitol, Pacific Jazz, Discovery, Mack AvenueMusical artist Gerald Sta...

 

 

ماريا تيودورا أدوراثيون روانو

ماريا تيودورا أدوراثيون روانو (بالإسبانية: María Teodora Adoración Ruano Sanchón)‏    معلومات شخصية الميلاد 11 يناير 1969 (العمر 55 سنة) الجنسية إسبانيا  المدرسة الأم الجامعة البابوية في شلمنقة  الحياة العملية المهنة دراجة،  ومدير رياضي،  وسياسية  نوع السباق سباق الدراجات ع�...

Classe bilingue franco-bretonne

Si ce bandeau n'est plus pertinent, retirez-le. Cliquez ici pour en savoir plus. Cet article ne cite aucune source et peut contenir des informations erronées (signalé en septembre 2021). Si vous disposez d'ouvrages ou d'articles de référence ou si vous connaissez des sites web de qualité traitant du thème abordé ici, merci de compléter l'article en donnant les références utiles à sa vérifiabilité et en les liant à la section « Notes et références ». Trouver des sou...

 

 

Barbel (perhiasan)

Barbel dengan ulir sekrup di permukaan/luar batang (kiri) dan ulir sekrup di dalam batang (kanan). Barbel melengkung (curved barbell) yang dipakai pada tindik pusar. Barbel ladam (circular barbell atau horshoe barbell) yang dipasang pada tindik hidung. Barbel adalah jenis anting atau perhiasan tindik yang terdiri dari suatu batang logam (atau bahan lainnya), dan sepasang bola atau pengganjal pada kedua ujungnya. Anting ini disebut barbel karena bentuk awalnya yang lurus membuatnya tampak sepe...

 

 

Chicane

Contoh chicane dalam sirkuit olahraga otomotif. Chicane adalah kurva serpentin di jalan, ditambah dengan desain dari didikte oleh geografi. Chicane menambahkan putaran ekstra dan digunakan baik di olahraga otomotif seperti balap mobil / motor maupun di jalan raya konvensional untuk memperlambat lalu lintas demi keamanan. Misalnya, salah satu bentuk chicane adalah belokan pendek berbentuk dangkal yang mengharuskan pengemudi berbelok sedikit ke kiri dan sedikit demi sedikit melanjutkan perjalan...

Family Portrait (Voyager)

1990 Solar System image by Voyager 1 The Family Portrait of the Solar System taken by Voyager 1 The Family Portrait, or sometimes Portrait of the Planets, is an image of the Solar System acquired by Voyager 1 on February 14, 1990, from a distance of approximately 6 billion km (40 AU; 3.7 billion mi) from Earth. It features individual frames of six planets and a partial background indicating their relative positions. The picture is a mosaic of 60 frames.[1] The...

 

 

埼玉労働局

埼玉労働局 Saitama Labour Bureau 埼玉労働局及びさいたま労働基準監督署が入る明治安田生命さいたま新都心ビル 種別 都道府県労働局 管轄区域 埼玉県 所在地 〒330-6016埼玉県さいたま市中央区新都心11-2明治安田生命さいたま新都心ビル14・15・16階 リンク 公式サイト 埼玉労働局（さいたまろうどうきょく）は、厚生労働省の地方支分部局である都道府県労働局の一つで、�...

 

 

Aachen

City in North Rhine-Westphalia, Germany For other uses, see Aachen (disambiguation). City in North Rhine-Westphalia, GermanyAachen Oche (Aachen dialect)CityView over Aachen with the town hall and the cathedralAachen Cathedral and St. Foillan's ChurchChoir and apse with Shrine of MaryOctagon of the Palatine ChapelShrine of CharlemagneBust of CharlemagneElise's FountainSt. John's Church FlagCoat of armsLocation of Aachen within Städteregion Aachen Aachen Show map of GermanyAachen Show map of N...

Sauvegarde (informatique)

« Sauvegarde » redirige ici. Pour les autres significations, voir Sauvegarde (homonymie). Pour les articles homonymes, voir Backup. Si ce bandeau n'est plus pertinent, retirez-le. Cliquez ici pour en savoir plus. Cet article ne cite pas suffisamment ses sources (avril 2014). Si vous disposez d'ouvrages ou d'articles de référence ou si vous connaissez des sites web de qualité traitant du thème abordé ici, merci de compléter l'article en donnant les références utiles à sa ...

 

 

Henry F. Dimock

American lawyer Henry Farnam DimockBorn(1842-03-28)March 28, 1842South Coventry, ConnecticutDiedApril 10, 1911(1911-04-10) (aged 69)New York CityAlma materYale UniversityHarvard Law SchoolBoard member ofBoston & Maine Railroad, Knickerbocker Trust Company, Metropolitan Steamship Company, Dominion Iron and Steel Company, Yale CorporationSpouseSusan Collins WhitneyChildrenSusan M. DimockParent(s)Timothy DimockLaura F. Booth Henry Farnam Dimock (March 28, 1842 – April 10, 19...

 

 

André Brink

André Philippus Brink André Philippus Brink (Vrede, 29 maggio 1935 – Città del Capo, 6 febbraio 2015) è stato uno scrittore sudafricano autore sia in lingua inglese sia in lingua afrikaans e professore universitario a Città del Capo, città dove risiedeva. È noto soprattutto per l'intensa attività letteraria negli anni sessanta, che l'ha portato a essere assieme al più noto scrittore e pittore Breyten Breytenbach, la figura chiave del movimento Sestigers, del quale facevano parte au...

Air Rhodesia Flight 827

1979 aircraft incident in Zimbabwe Air Rhodesia Flight 827A similar Air Rhodesia aircraftAirliner shootdownDate12 February 1979SummaryShot down with a Strela 2 missile by ZIPRA guerrillasSiteVuti African Purchase Area 16°25′S 29°26′E / 16.417°S 29.433°E / -16.417; 29.433AircraftAircraft typeVickers ViscountOperatorAir RhodesiaRegistrationVP-YNDFlight originSalisbury International Airport, RhodesiaLast stopoverKariba, RhodesiaDestinationSalisbury Internatio...

 

 

1996 Republican Party presidential primaries

1996 Republican Party presidential primaries ← 1992 January 29 to June 4, 1996 2000 →   Candidate Bob Dole Pat Buchanan Steve Forbes Home state Kansas Virginia New Jersey Delegate count 1,437 101 51 Contests won 46 4 2 Popular vote 9,024,742 3,184,943 1,751,187 Percentage 58.8% 20.8% 11.4% Gold denotes a state won by Pat Buchanan. Green denotes a state won by Steve Forbes. Purple denotes a state won by Bob Dole. Gray denotes a territory that did...