Un instrument interactiv de demonstrare a teoremei

Un instrument interactiv de demonstrare a teoremei ( rezolvator interactiv de teoreme ) este un software care ajută cercetătorul să dezvolte dovezi formale . Dovezile sunt produse în procesul de interacțiune om-mașină. De obicei, un astfel de software include o formă de editor interactiv de dovezi sau altă interfață prin care o persoană poate căuta dovezi stocate pe computer, precum și proceduri automate de verificare a dovezilor efectuate de computer.

Comparația sistemelor

• HOL theorem prover  este o familie de produse software care, în cele din urmă, sunt derivate din instrumentul de demonstrare a teoremei LCF . În toate aceste sisteme, nucleul logic este biblioteca limbajului de programare încorporat în ele. Teoremele sunt elemente noi ale limbajului și sunt introduse folosind „strategii” care garantează corectitudinea logică. Strategie oferă utilizatorilor capacitatea de a crea dovezi importante cu relativ puține interacțiuni cu sistemul. Acest grup de sisteme include:
  • HOL4
  • Lumină HOL
  • Puterea Dovada
• IMPS [4]

Interfață cu utilizatorul

O interfață populară pentru instrumentele interactive de demonstrare a teoremelor este Proof General bazată pe Emacs, dezvoltată la Universitatea din Edinburgh . Coq include CoqIDE care este scris în OCaml/ Gtk . Isabelle include Isabelle/jEdit, care se bazează pe jEdit și cadrul Isabelle/ Scala pentru procesarea dovezilor centrate pe documente. Pentru Visual Studio Code , există și o extensie concepută pentru a funcționa cu Isabelle. A fost dezvoltat de Makarius Wenzel [5] .

Vezi și

• Dovada automata
• Calcul de probă
• Manifest QED
• Verificarea formală
• Problema satisfacabilității formulelor în teorii
• Metamath  este un limbaj conceput pentru dezvoltarea enunțurilor matematice formale, al cărui ecosistem include un instrument interactiv de demonstrare a teoremelor și mai multe baze de date cu mii de teoreme înregistrate și dovedite.

Note

1. ↑ Hunt, Warren; Matt Kaufman; Robert Bellarmine Krug; J Moore; Eric W. Smith. Meta raționament în ACL2  // Note de curs  Springer în informatică : jurnal. - 2005. - Vol. 3603 . - P. 163-178 .
2. ↑ Căutare „dovezi prin reflecție”: arXiv : 1803.06547
3. ↑ Pagina de versiuni Lean Theorem Prover . GitHub . Arhivat din original pe 5 septembrie 2020. (nedefinit)
4. ↑ Farmer, William M.; Guttman, Joshua D.; Thayer, F. Javier. IMPS: Un sistem interactiv de demonstrare matematică  //  Journal of Automated Reasoning. - 1993. - Vol. 11 , nr. 2 . - P. 213-248 . - doi : 10.1007/BF00881906 .
5. ↑ Wenzel, Makarius Isabelle . Preluat la 31 mai 2020. Arhivat din original la 4 iunie 2020. (nedefinit)

Literatură

• Henk Barendregt și Herman Geuvers (2001). „Asistenți de dovezi care utilizează sisteme de tip dependent” . În Manualul de raționament automat .
• Frank Pfenning (2001). „Cadre logice” . În Manualul de raționament automat .
• Frank Pfenning (1996). „Practica cadrelor logice”.
• Robert L. Constable (1998). „Tipuri în informatică, filozofie și logică”. În Manualul de teorie a dovezilor .
• H. Geuvers. Asistenți de dovezi: Istorie , idei și viitor .
• Freek Wiedijk. „ Cei șaptesprezece doveditori ai lumii ”

Link -uri

• „Introducere” d Programare certificată cu tipuri dependente .
• Introducere în Coq Proof Assistant (cu o introducere generală în demonstrarea interactivă a teoremei)
• Demonstrarea interactivă a teoremei pentru utilizatorii Agda
• O listă de instrumente de demonstrare a teoremelor

• Matematică digitală după categorie: doveditori de tactică
• Sisteme și grupuri automate de deducere
• Demonstrarea teoremei și sistemele de raționament automat
• Baza de date a sistemelor de raționament mecanizat existente
• NuPRL: Alte sisteme
• Cadre logice specifice și implementări
• DMOZ : Știință: Matematică: Logica și fundamente: Logica computațională: Cadre logice