Důkaz asistent - Proof assistant

Akademická konference viz Interactive Theorem Proving (konference).
Nesmí být zaměňována s Interaktivní kontrolní systém.
Interaktivní kontrolní relace v CoqIDE, zobrazující kontrolní skript vlevo a kontrolní stav vpravo.

v počítačová věda a matematická logika, a důkaz asistent nebo interaktivní věta prover je softwarový nástroj, který pomáhá s vývojem formální důkazy spoluprací člověk-stroj. To zahrnuje nějaký druh interaktivního editoru korektur nebo jiný rozhraní, s nimiž může člověk vést hledání důkazů, jejichž podrobnosti jsou uloženy v, a některé kroky poskytované, a počítač.

Porovnání systémů

Viz také: Závislý typ § Porovnání, a Automatizované dokazování věty § Porovnání
názevNejnovější verzeVývojářiJazyk implementaceFunkce
Logika vyššího řáduZávislé typyMalé jádroAutomatizace důkazůDůkaz odrazemGenerování kódu
ACL28.2Matt Kaufmann a J Strother MooreSpolečný LispNeBez typuNeAnoAno[1]Již spustitelný
Agda2.6.0.1Ulf Norell, Nils Anders Danielsson a Andreas Abel (Chalmers a Gothenburg )HaskellAnoAnoAnoNeČástečnýJiž spustitelný
Albatros0.4Helmut BrandlOCamlAnoNeAnoAnoNeznámýDosud není implementováno
Coq8.11.0INRIAOCamlAnoAnoAnoAnoAnoAno
F*úložištěMicrosoft Research a INRIAF*AnoAnoNeAnoAno[2]Ano
HOL LightúložištěJohn HarrisonOCamlAnoNeAnoAnoNeNe
HOL4Kananaskis-13 (nebo repo)Michael Norrish, Konrad Slind a dalšíStandardní MLAnoNeAnoAnoNeAno
Idrisi1.3.3Edwin BradyHaskellAnoAnoAnoNeznámýČástečnýJiž spustitelný
IsabelleIsabelle2020 (duben 2020)Larry Paulson (Cambridge ), Tobias Nipkow (Mnichov ) a Makarius WenzelStandardní ML, ScalaAnoNeAnoAnoAnoAno
Opírat sev3.4.2[3]Microsoft ResearchC ++AnoAnoAnoAnoAnoNeznámý
LEGO (není spojen se společností LEGO)1.3.1Randy Pollack (Edinburgh )Standardní MLAnoAnoAnoNeNeNe
Mizar8.1.05Białystok UniversityFree PascalČástečnýAnoNeNeNeNe
NuPRL5Cornell UniversitySpolečný LispAnoAnoAnoAnoNeznámýAno
PVS6.0SRI InternationalSpolečný LispAnoAnoNeAnoNeNeznámý
Twelf1.7.1Frank Pfenning a Carsten SchürmannStandardní MLAnoAnoNeznámýNeNeNeznámý
  • ACL2 - programovací jazyk, logická teorie prvního řádu a prověrka věty (s interaktivním i automatickým režimem) v tradici Boyer – Moore.
  • Coq - Který umožňuje vyjádření matematických tvrzení, mechanicky kontroluje důkazy těchto tvrzení, pomáhá najít formální důkazy a extrahuje certifikovaný program z konstruktivního důkazu jeho formální specifikace.
  • Prokazování teorémů HOL - Rodina nástrojů nakonec odvozených z LCF teorém prover. V těchto systémech je logickým jádrem knihovna jejich programovacího jazyka. Věty představují nové prvky jazyka a lze je zavést pouze prostřednictvím „strategií“, které zaručují logickou správnost. Složení strategie dává uživatelům možnost vytvářet významné důkazy s relativně malým počtem interakcí se systémem. Členové rodiny zahrnují:
  • IMPS, interaktivní matematický kontrolní systém[4]
  • Isabelle je interaktivní tester teorémů, nástupce HOL. Hlavní kódová základna je licencována BSD, ale distribuce Isabelle sdružuje mnoho doplňkových nástrojů s různými licencemi.
  • Žert - založené na Javě.
  • LEGO
  • Matita - Světelný systém založený na počtu indukčních konstrukcí.
  • MINLOG - Asistent kontroly založený na minimální logice prvního řádu.
  • Mizar - Asistent kontroly založený na logice prvního řádu, v a přirozený odpočet styl a Teorie množin Tarski – Grothendieck.
  • PhoX - Asistent kontroly založený na logice vyššího řádu, který je rozšiřitelný.
  • Systém ověřování prototypů (PVS) - jazyk důkazu a systém založený na logice vyššího řádu.
  • TPS a ETPS - Interaktivní testovací věty také založené na lambda kalkulu jednoduše zadaného typu, ale založené na nezávislém formulace logické teorie a nezávislé implementace.
  • Typelab
  • Řebříček

The Věta Prover Museum je iniciativa na zachování zdrojů systémů prokazování vět pro budoucí analýzu, protože se jedná o důležité kulturní / vědecké artefakty. Má zdroje mnoha výše zmíněných systémů.

Uživatelská rozhraní

Populární front-end pro kontrolní asistenty je Emacs generální důkaz, založený na University of Edinburgh.Coq zahrnuje CoqIDE, který je založen na OCaml /Gtk. Isabelle zahrnuje Isabelle / jEdit, která je založena na jEdit a Isabelle /Scala infrastruktura pro zpracování důkazů orientovaných na dokumenty. Více nedávno, a Kód sady Visual Studio rozšíření pro Isabelle také vyvinul Makarius Wenzel.[5]

Viz také

Poznámky

  1. ^ Hunt, Warren; Matt Kaufmann; Robert Bellarmine Krug; J Moore; Eric W. Smith (2005). „Meta uvažování v ACL2“ (PDF). Springerova přednáška v informatice. 3603: 163–178.
  2. ^ Hledat „proofs by reflect“: arXiv:1803.06547
  3. ^ „Stránka Zprávy poskytovatele štíhlé věty“. GitHub.
  4. ^ Farmer, William M .; Guttman, Joshua D .; Thayer, F. Javier (1993). „IMPS: Interaktivní matematický kontrolní systém“. Journal of Automated Reasoning. 11 (2): 213–248. doi:10.1007 / BF00881906. Citováno 22. ledna 2020.
  5. ^ Wenzel, Makarius. „Isabelle“. Citováno 2. listopadu 2019.

Reference

externí odkazy

Katalogy