Interaktivní nástroj pro dokazování teorémů

Interaktivní nástroj pro dokazování teorémů ( interaktivní řešič teorémů ) je software , který pomáhá výzkumníkovi při vývoji formálních důkazů . Důkazy vznikají v procesu interakce člověk-stroj. Takový software obvykle obsahuje nějakou formu interaktivního editoru důkazů nebo jiného rozhraní, jehož prostřednictvím může osoba vyhledávat důkazy uložené v počítači, stejně jako automatizované postupy ověřování důkazů prováděné počítačem.

Porovnání systémů

• HOL theorem prover  je rodina softwarových produktů, které jsou nakonec odvozeny od nástroje LCF theorem prover . Ve všech těchto systémech je logickým jádrem knihovna programovacího jazyka v nich zabudovaná. Věty jsou nové prvky jazyka a jsou zaváděny pomocí „strategií“, které zaručují logickou správnost. Strategizace dává uživatelům možnost vytvářet důležité důkazy s relativně malým počtem interakcí se systémem. Tato skupina systémů zahrnuje:
  • HOL4
  • HOL Světlo
  • Důkazní síla
• IMPS [4]

Uživatelské rozhraní

Populárním rozhraním pro interaktivní nástroje pro ověřování teorémů je Proof General založený na Emacs vyvinutý na University of Edinburgh . Coq obsahuje CoqIDE, které je napsáno v OCaml/ Gtk . Isabelle zahrnuje Isabelle/jEdit, který je založen na jEdit a rámci Isabelle/ Scala pro zpracování důkazů zaměřených na dokumenty. Pro Visual Studio Code existuje také rozšíření navržené pro práci s Isabelle. Vyvinul jej Makarius Wenzel [5] .

Viz také

• Automatický důkaz
• Důkazové výpočty
• manifest QED
• Formální ověření
• Problém splnitelnosti formulí v teoriích
• Metamath  je jazyk určený pro vývoj formálních matematických výroků, jehož ekosystém zahrnuje interaktivní nástroj pro ověřování teorémů a několik databází s tisíci zaznamenaných a ověřených teorémů.

Poznámky

1. ↑ Hunt, Warren; Matt Kaufman; Robert Bellarmine Krug; J Moore; Eric W. Smith. Meta Reasoning v ACL2  //  Springer Lecture Notes in Computer Science : deník. - 2005. - Sv. 3603 . - S. 163-178 .
2. ↑ Hledejte „důkazy odrazem“: arXiv : 1803.06547
3. ↑ Stránka Vydání Lean Theorem Prover . GitHub . Archivováno z originálu 5. září 2020. (neurčitý)
4. ↑ Farmář, William M.; Guttman, Joshua D.; Thayer, F. Javier. IMPS: Interaktivní matematický důkazní systém  //  Journal of Automated Reasoning. - 1993. - Sv. 11 , č. 2 . - str. 213-248 . - doi : 10.1007/BF00881906 .
5. ↑ Wenzel, Makarius Isabelle . Staženo 31. května 2020. Archivováno z originálu dne 4. června 2020. (neurčitý)

Literatura

• Henk Barendregt a Herman Geuvers (2001). "Asistenti důkazu používající systémy závislého typu" . In Handbook of Automated Reasoning .
• Frank Pfenning (2001). "Logické rámce" . In Handbook of Automated Reasoning .
• Frank Pfenning (1996). „Praxe logických rámců“.
• Robert L. Constable (1998). „Typy v informatice, filozofii a logice“ . In Příručka teorie důkazů .
• H. Geuvers. Důkazní asistenti: Historie , nápady a budoucnost .
• Freek Wiedijk. " Sedmnáct Provers of the World "

Odkazy

• "Úvod" d Certifikované programování se závislými typy .
• Úvod do Coq Proof Assistant (s obecným úvodem do interaktivního dokazování teorémů)
• Interaktivní dokazování teorémů pro uživatele Agda
• Seznam nástrojů pro dokazování teorémů

• Digitální matematika podle kategorie: Taktické důkazy
• Automatizované odpočtové systémy a skupiny
• Dokazování teorémů a automatizované systémy uvažování
• Databáze existujících mechanizovaných uvažovacích systémů
• NuPRL: Jiné systémy
• Specifické logické rámce a implementace
• DMOZ : Věda: Matematika: Logika a základy: Výpočetní logika: Logické rámce