Manifest QED - QED manifesto

The Manifest QED byl návrh počítačové databáze všech matematický znalosti, přísně formalizované a se všemi důkazy, které byly zkontrolováno automaticky. (Q.E.D. prostředek quod erat demonstrandum v latinský, což znamená „který měl být prokázán.“)

Přehled

Myšlenka projektu vznikla v roce 1993, hlavně na popud Robert Boyer. Cíle projektu, předběžně pojmenované QED projekt nebo projekt QED, byly popsány v manifestu QED, dokumentu, který byl poprvé publikován v roce 1994, se vstupy několika výzkumníků.[1] Záměrně se zabránilo výslovnému autorství. Byl vytvořen zvláštní seznam adresátů a konaly se dvě vědecké konference o QED, první v roce 1994 v Argonne National Laboratories a druhý v roce 1995 v Varšava pořádá Mizar skupina.[2]

Zdá se, že se projekt do roku 1996 rozpustil, aniž by přinesl více než diskuse a plány. V dokumentu z roku 2007 uvádí Freek Wiedijk dva důvody neúspěchu projektu.[3] V pořadí podle důležitosti:

  • Velmi málo lidí pracuje na formalizaci matematiky. Pro plně mechanizovanou matematiku neexistuje žádná přesvědčivá aplikace.
  • Formalizovaná matematika ještě nepodobá skutečné tradiční matematice. To je částečně způsobeno složitostí matematické notace a částečně omezeními existujících věty provers a důkazní asistenti; článek zjistí, že hlavní uchazeči, Mizar, HOL, a Coq, mají vážné nedostatky ve schopnostech vyjadřovat matematiku.

Pravidelně se však navrhují projekty ve stylu QED a Mizar knihovna úspěšně formalizovala velkou část vysokoškolské matematiky. Od roku 2007 je to největší taková knihovna.[4] Dalším takovým projektem je Metamath důkazní databáze.

V roce 2014 dvacet let manifestu QED[5] workshop byl organizován jako součást Vídeňské logické léto.

Viz také

Reference

  1. ^ Manifest QED v Automatizovaný odpočet - CADE 12Springer-Verlag, Lecture Notes in Artificial Intelligence, sv. 814, str. 238-251, 1994. HTML verze
  2. ^ Zpráva QED Workshop II
  3. ^ Freek Wiedijk, Manifest QED se vrátil, 2007
  4. ^ Fairouz Kamareddine, Manuel Maarek, Krzysztof Retel a J. B. Wells, Postupná automatizace / formalizace matematických textů do Mizaru
  5. ^ Dvacet let workshopu QED Manifesto

Další čtení

  • H. Barendregt & F. Wiedijk, Výzva počítačové matematiky, Transakce A Královské společnosti 363 č. 1835, 2351-2375, 2005
  • „Zvláštní vydání na formální důkaz“. Oznámení Americké matematické společnosti. Prosinec 2008. (problém s otevřeným přístupem)
  • Richard A. De Millo, Richard J. Lipton, Alan J. Perlis, Sociální procesy a důkazy vět a programů, Komunikace ACM, Svazek 22, číslo 5 (květen 1979), strany: 271 - 280
  • John Harrison, Formalizovaná matematika, Technická zpráva 36, Turku Center for Computer Science (TUCS)

externí odkazy