Kanıt yardımcısı - Proof assistant

Akademik konferans için, bkz. Etkileşimli Teorem Kanıtlama (konferans) .
İle karıştırılmamalıdır Etkileşimli kanıt sistemi .
CoqIDE'de, prova komut dosyasını solda ve prova durumunu sağda gösteren etkileşimli bir prova oturumu.

Gelen bilgisayar bilimleri ve matematik mantık , bir prova asistanı veya interaktif teoremi prover gelişimine yardımcı olacak bir yazılım aracıdır resmi provaları insan-makine işbirliği ile. Bu, bir insanın, ayrıntılarının bir bilgisayarda saklandığı ve bazı adımların bir bilgisayar tarafından sağlanan kanıtların aranmasına rehberlik edebileceği bir tür etkileşimli kanıt düzenleyicisini veya başka bir arabirimi içerir .

Sistem karşılaştırması

Ayrıca bakınız: Bağımlı tip § Karşılaştırma ve Otomatik teorem ispatlama § Karşılaştırma
İsim En son sürüm Geliştirici(ler) uygulama dili Özellikleri
Üst düzey mantık Bağımlı türler Küçük çekirdek Kanıt otomasyonu Yansıma yoluyla kanıt Kod oluşturma
ACL2 8.3 Matt Kaufmann ve J Strother Moore Ortak Lisp Numara yazılmamış Numara Evet Evet Zaten yürütülebilir
Ağda 2.6.2 Ulf Norell, Nils Anders Danielsson ve Andreas Abel ( Chalmers ve Göteborg ) Haskell Evet Evet Evet Numara Kısmi Zaten yürütülebilir
Albatros 0,4 Helmut Brandl OCaml Evet Numara Evet Evet Bilinmeyen Henüz uygulanmadı
Coq 8.13.2 INRIA OCaml Evet Evet Evet Evet Evet Evet
F* depo Microsoft Araştırma ve INRIA F* Evet Evet Numara Evet Evet Evet
HOL Işık depo John Harrison OCaml Evet Numara Evet Evet Numara Numara
HOL4 Kananaskis-13 (veya repo) Michael Norrish, Konrad Slind ve diğerleri standart makine öğrenimi Evet Numara Evet Evet Numara Evet
İdris 2 0.4.0. Edwin Brady İdris Evet Evet Evet Bilinmeyen Kısmi Evet
Isabelle Isabelle 2021 (Şubat 2021) Larry Paulson ( Cambridge ), Tobias Nipkow ( München ) ve Makarius Wenzel Standart ML , Scala Evet Numara Evet Evet Evet Evet
Eğilmek v3.4.2 Microsoft Araştırması C++ Evet Evet Evet Evet Evet Bilinmeyen
LEGO ( Lego'ya bağlı değil ) 1.3.1 Randy Pollack ( Edinburgh ) standart makine öğrenimi Evet Evet Evet Numara Numara Numara
Mizar 8.1.05 Białystok Üniversitesi Ücretsiz Pascal Kısmi Evet Numara Numara Numara Numara
NuPRL 5 Cornell Üniversitesi Ortak Lisp Evet Evet Evet Evet Bilinmeyen Evet
PVS 6.0 SRI Uluslararası Ortak Lisp Evet Evet Numara Evet Numara Bilinmeyen
on iki 1.7.1 Frank Pfenning ve Carsten Schürmann standart makine öğrenimi Evet Evet Bilinmeyen Numara Numara Bilinmeyen
  • ACL2  – Boyer-Moore geleneğinde bir programlama dili, birinci dereceden bir mantıksal teori ve bir teorem ispatlayıcı (hem etkileşimli hem de otomatik modlarla).
  • Coq  – Matematiksel iddiaların ifadesine izin veren, bu iddiaların kanıtlarını mekanik olarak kontrol eden, biçimsel kanıtların bulunmasına yardımcı olan ve biçimsel özelliklerinin yapıcı kanıtından onaylı bir program çıkaran.
  • HOL teoremi ispatlayıcıları  – Sonuçta LCF teoremi ispatlayıcısından türetilen bir araç ailesi . Bu sistemlerde mantıksal çekirdek, programlama dillerinin bir kütüphanesidir. Teoremler, dilin yeni unsurlarını temsil eder ve yalnızca mantıksal doğruluğu garanti eden "stratejiler" yoluyla tanıtılabilir. Strateji kompozisyonu, kullanıcılara sistemle nispeten az etkileşimle önemli kanıtlar üretme yeteneği verir. Ailenin üyeleri şunları içerir:
  • IMPS, Etkileşimli Matematiksel Kanıt Sistemi
  • Isabelle , HOL'nin halefi olan etkileşimli bir teorem ispatlayıcısıdır. Ana kod tabanı BSD lisanslıdır, ancak Isabelle dağıtımı birçok eklenti aracını farklı lisanslarla bir araya getirir.
  • Jape  – Java tabanlı.
  • Eğilmek
  • LEGO
  • Matita  – Endüktif Yapıların Hesabına dayalı bir ışık sistemi.
  • MINLOG  – Birinci dereceden minimum mantığa dayalı bir ispat asistanı.
  • Mizar  – Doğal bir kesinti tarzında birinci dereceden mantığa ve Tarski-Grothendieck küme teorisine dayanan bir ispat yardımcısı .
  • PhoX  – Genişletilebilir olan yüksek dereceli mantığa dayalı bir prova yardımcısı.
  • Prototip Doğrulama Sistemi (PVS) – daha yüksek mertebeden mantığa dayalı bir ispat dili ve sistemi.
  • TPS ve ETPS  – Etkileşimli teorem kanıtlayıcılar ayrıca basit bir şekilde yazılan lambda hesabını temel alır, ancak mantıksal teorinin bağımsız bir formülasyonuna ve bağımsız uygulamaya dayanır .
  • Typelab
  • Civanperçemi

Teorem Prover Müzesi onlar önemli kültürel bilimsel / eserler olduğundan, gelecek analizi için teoremi prover sistemlerinin kaynaklarını korumak için bir girişimdir. Yukarıda bahsedilen sistemlerin birçoğunun kaynaklarına sahiptir.

Kullanıcı arayüzleri

Prova asistanları için popüler bir ön uç , Edinburgh Üniversitesi'nde geliştirilen Emacs tabanlı Proof General'dir . Coq OCaml / dayanmaktadır CoqIDE içerir Gtk . Isabelle, jEdit'e dayanan Isabelle/ jEdit'i ve belge odaklı kanıt işleme için Isabelle/ Scala altyapısını içerir. Daha yakın zamanlarda, Isabelle için bir Visual Studio Code uzantısı da Makarius Wenzel tarafından geliştirilmiştir.

Ayrıca bakınız

Notlar

Referanslar

Dış bağlantılar

Kataloglar