Otomatik teorem ispatı - Automated theorem proving

Otomatik teorem ispatı ( ATP veya otomatik kesinti olarak da bilinir ), bilgisayar programları tarafından matematiksel teoremlerin ispatlanmasıyla ilgilenen otomatik muhakeme ve matematiksel mantığın bir alt alanıdır . Matematiksel kanıt üzerinden otomatik akıl yürütme , bilgisayar biliminin gelişimi için büyük bir itici güçtü .

mantıksal temeller

Biçimselleştirilmiş mantığın kökleri Aristoteles'e kadar uzanırken , 19. yüzyılın sonu ve 20. yüzyılın başlarında modern mantığın ve biçimselleştirilmiş matematiğin gelişimi görüldü. Frege 'nin Begriffsschrift (1879) tam hem tanıtıldı önermeler taşı ve ne esasen modern yüklem mantığı . Onun Aritmetik Temelleri 1884 yayınlanan, (bir kısmı) genel mantıkta matematik olarak ifade edilmiştir. Bu yaklaşım, Russell ve Whitehead tarafından , ilk kez 1910–1913'te yayınlanan ve 1927'de gözden geçirilmiş ikinci baskıyla, etkili Principia Mathematica'da devam ettirildi. Russell ve Whitehead , prensipte, formel mantığın aksiyomlarını ve çıkarım kurallarını kullanarak tüm matematiksel doğruları elde edebileceklerini düşündüler. süreci otomasyona açmak. 1920'de Thoralf Skolem , Leopold Löwenheim'ın önceki bir sonucunu basitleştirdi , bu da Löwenheim-Skolem teoremine ve 1930'da bir Herbrand evreni kavramına ve birinci dereceden formüllerin (ve dolayısıyla) tatmin edilemezliğine (dolayısıyla) izin veren bir Herbrand yorumuna yol açtı. geçerliliği bir teoreminin) (potansiyel olarak sonsuz sayıda) önerme satisfiability sorunlarına azaltılmalıdır.

1929'da Mojżesz Presburger , toplama ve eşitlikle doğal sayılar teorisinin (şimdi onun onuruna Presburger aritmetiği olarak adlandırılır ) karar verilebilir olduğunu gösterdi ve dilde verilen bir cümlenin doğru mu yanlış mı olduğunu belirleyebilecek bir algoritma verdi. Bununla birlikte, bu olumlu sonuçtan kısa bir süre sonra Kurt Gödel , Yeterince güçlü herhangi bir aksiyomatik sistemde, sistemde kanıtlanamayan doğru ifadeler olduğunu göstererek , Principia Mathematica ve İlgili Sistemlerin Biçimsel Olarak Karar Verilemez Önermeleri Üzerine (1931) yayınlamıştır . Bu konu 1930'larda Alonzo Church ve Alan Turing tarafından daha da geliştirildi , bir yandan iki bağımsız ama eşdeğer hesaplanabilirlik tanımı yapan ve diğer yandan kararsız sorular için somut örnekler veren Alan Turing .

İlk uygulamalar

İkinci Dünya Savaşı'ndan kısa bir süre sonra , ilk genel amaçlı bilgisayarlar kullanıma sunuldu. 1954'te Martin Davis , Princeton, New Jersey'deki İleri Araştırma Enstitüsü'nde bir JOHNNIAC vakum tüplü bilgisayar için Presburger'in algoritmasını programladı . Davis'e göre, "En büyük zaferi, iki çift sayının toplamının çift olduğunu kanıtlamasıydı". Daha iddialı oldu Mantık Teorisi Makinesi 1956 yılında, bir kesinti sistemi önermeler mantığı arasında Principia Mathematica tarafından geliştirilen, Allen Newell , Herbert A. Simon ve JC Shaw . Ayrıca bir JOHNNIAC üzerinde çalışan Mantık Teorisi Makinesi, küçük bir dizi önermesel aksiyomdan ve üç tümdengelim kuralından ispatlar oluşturdu : modus ponens , (önermesel) değişken ikamesi ve formüllerin tanımlarına göre değiştirilmesi. Sistem buluşsal rehberlik kullandı ve Principia'nın ilk 52 teoreminin 38'ini kanıtlamayı başardı .

Mantık Teorisi Makinesi'nin "sezgisel" yaklaşımı, insan matematikçileri taklit etmeye çalıştı ve prensipte bile her geçerli teorem için bir kanıtın bulunabileceğini garanti edemedi. Buna karşılık, diğer, daha sistematik algoritmalar, en azından teorik olarak, birinci dereceden mantık için eksiksizlik sağladı. İlk yaklaşımlar, değişkenleri Herbrand evreninden terimlerle somutlaştırarak birinci dereceden bir formülü ardışık olarak daha büyük önerme formülleri kümelerine dönüştürmek için Herbrand ve Skolem'in sonuçlarına dayanıyordu . Önerme formülleri daha sonra bir dizi yöntem kullanılarak tatmin edilemezlik açısından kontrol edilebilir. Gilmore'un programı , bir formülün tatmin edilebilirliğinin açık olduğu bir biçim olan, ayrık normal biçime dönüştürmeyi kullandı .

Sorunun karar verilebilirliği

Altta yatan mantığa bağlı olarak, bir formülün geçerliliğine karar verme sorunu önemsizden imkansıza kadar değişir. Önerme mantığının sık görülen durumu için , sorun karar verilebilir ancak ortak NP-tamamlandı ve bu nedenle genel kanıt görevleri için yalnızca üstel zamanlı algoritmaların var olduğuna inanılıyor. Bir İçin birinci dereceden yüklem hesabı , Gödel'in tamlık teoremi devletler teoremleri (kanıtlanabilir ifadeleri) tam mantıksal geçerli olduğunu iyi biçimli formülleri böylece geçerli formüller tanımlayarak, bir ardışık enumerable : sınırsız kaynaklar göz önüne alındığında, herhangi bir geçerli formül sonunda kanıtlanabilir. Ancak, geçersiz formüller (olanlar değil , belirli bir teori gerektirdiği), her zaman kabul edilemez.

Yukarıdakiler, Peano aritmetiği gibi birinci dereceden teoriler için geçerlidir . Bununla birlikte, birinci dereceden bir teori tarafından tanımlanabilecek belirli bir model için, modeli tanımlamak için kullanılan teoride bazı ifadeler doğru olabilir ancak karar verilemez. Örneğin, Gödel'in eksiklik teoremi ile , uygun aksiyomlar listesinin sonsuz sayılabilir olmasına izin verilse bile, uygun aksiyomları doğal sayılar için doğru olan herhangi bir teorinin, doğal sayılar için tüm birinci dereceden ifadelerin doğruluğunu kanıtlayamayacağını biliyoruz. Otomatik bir teorem ispatlayıcısı, tam olarak araştırılan ifade, kullanılan teoride karar verilemez olduğunda, ilgilenilen modelde doğru olsa bile, bir ispat ararken sona ermede başarısız olacaktır. Bu teorik sınıra rağmen, pratikte teorem ispatlayıcıları, herhangi bir birinci mertebeden teori (tamsayılar gibi) tarafından tam olarak tanımlanmayan modellerde bile birçok zor problemi çözebilir.

İlgili sorunlar

Daha basit, ancak ilgili bir sorun, bir teorem için mevcut bir kanıtın geçerli olarak onaylandığı ispat doğrulamasıdır . Bunun için genellikle her bir ispat adımının ilkel bir özyinelemeli fonksiyon veya program tarafından doğrulanabilmesi gerekir ve bu nedenle problem her zaman karar verilebilir.

Otomatik teorem ispatlayıcılar tarafından üretilen ispatlar tipik olarak çok büyük olduğu için ispat sıkıştırma problemi çok önemlidir ve ispatın çıktısını küçültmeyi ve dolayısıyla daha kolay anlaşılır ve kontrol edilebilir hale getirmeyi amaçlayan çeşitli teknikler geliştirilmiştir.

Kanıt asistanları , bir insan kullanıcının sisteme ipuçları vermesini gerektirir. Otomasyon derecesine bağlı olarak, kanıtlayıcı esasen, kullanıcının kanıtı resmi bir şekilde sağladığı bir kanıt denetleyicisine indirgenebilir veya önemli kanıtlama görevleri otomatik olarak gerçekleştirilebilir. Etkileşimli ispatlayıcılar çeşitli görevler için kullanılır, ancak tam otomatik sistemler bile bir dizi ilginç ve zor teoremi kanıtlamıştır, bunlardan en az biri uzun süredir matematikçilerin gözünden kaçmış olan Robbins varsayımıdır . Bununla birlikte, bu başarılar düzensizdir ve zor problemler üzerinde çalışmak genellikle yetkin bir kullanıcı gerektirir.

Bir sürecin aksiyomlarla başlayıp çıkarım kurallarını kullanarak yeni çıkarım adımları üreten geleneksel bir kanıttan oluşuyorsa teorem kanıtlaması olarak kabul edildiği teorem kanıtlama ve diğer teknikler arasında bazen başka bir ayrım yapılır. Diğer teknikler , en basit durumda birçok olası durumun kaba kuvvetle numaralandırılmasını içeren model kontrolünü içerir (her ne kadar model denetleyicilerinin fiili uygulaması çok fazla zeka gerektirir ve basitçe kaba kuvvete indirgenmez).

Model kontrolünü bir çıkarım kuralı olarak kullanan hibrit teorem kanıtlama sistemleri vardır. Belirli bir teoremi kanıtlamak için yazılmış programlar da vardır, (genellikle gayri resmi) bir kanıtla birlikte, program belirli bir sonuçla biterse, teoremin doğrudur. Buna iyi bir örnek , programın hesaplamasının muazzam boyutu nedeniyle insanlar tarafından doğrulanması esasen imkansız olan ilk iddia edilen matematiksel kanıt olarak çok tartışmalı olan dört renk teoreminin makine destekli kanıtıydı (bu tür kanıtlara non- insan olarak adlandırılır). -anketlenebilir kanıtlar ). Program destekli ispatın bir başka örneği, Connect Four oyununun her zaman ilk oyuncu tarafından kazanılabileceğini gösteren kanıttır .

Endüstriyel kullanımlar

Otomatik teorem ispatının ticari kullanımı, çoğunlukla entegre devre tasarımı ve doğrulamasında yoğunlaşmıştır . Pentium FDIV hatasından bu yana, modern mikroişlemcilerin karmaşık kayan nokta birimleri , ekstra inceleme ile tasarlanmıştır. AMD , Intel ve diğerleri, bölme ve diğer işlemlerin işlemcilerinde doğru bir şekilde uygulandığını doğrulamak için otomatik teoremi kanıtlamayı kullanır.

Birinci dereceden teoremi kanıtlama

1960'ların sonlarında, otomatik kesinti araştırmalarını finanse eden ajanslar, pratik uygulamalara olan ihtiyacı vurgulamaya başladı. İlk verimli alanlardan biri o idi programı doğrulama birinci dereceden teoremi ispatlayıcılar böyle erken bir program doğrulama sistemleri arasında Önemli vb Pascal, Ada gibi dillerde bilgisayar programlarının doğruluğunu doğrulaması sorununu uygulandı sayede Stanford Pascal Doğrulayıcı oldu tarafından geliştirilen David Luckham de Stanford Üniversitesi . Bu aynı zamanda kullanarak Stanford'da geliştirilen Stanford Çözünürlük Prover dayanıyordu John Alan Robinson 'ın çözünürlük prensibini. Bu, çözümler resmi olarak yayınlanmadan önce Amerikan Matematik Derneği Bildirimlerinde ilan edilen matematiksel problemleri çözme yeteneğini gösteren ilk otomatik kesinti sistemiydi.

Birinci dereceden teorem ispatı, otomatik teorem ispatının en olgun alt alanlarından biridir. Mantık, genellikle makul ölçüde doğal ve sezgisel bir şekilde, keyfi sorunların belirlenmesine izin verecek kadar anlamlıdır. Öte yandan, hala yarı karar verilebilir ve tam otomatik sistemler sağlayan bir dizi sağlam ve eksiksiz hesap geliştirilmiştir . Yüksek mertebeden mantıklar gibi daha açıklayıcı mantıklar, birinci mertebeden mantıktan daha geniş bir problem yelpazesinin uygun ifadesine izin verir, ancak bu mantıklar için ispat teoremleri daha az gelişmiştir.

Karşılaştırmalar, yarışmalar ve kaynaklar

Uygulanan sistemlerin kalitesi, standart kıyaslama örneklerinden oluşan geniş bir kütüphanenin – Teorem Kanıtlayıcıları için Binlerce Problem (TPTP) Problem Kitaplığı – varlığından ve ayrıca her yıl ilk kez düzenlenen CADE ATP Sistem Yarışması'ndan (CASC) yararlanmıştır. -birinci dereceden problemlerin birçok önemli sınıfı için -dereceden sistemler.

Bazı önemli sistemler (hepsi en az bir CASC yarışma bölümü kazanmıştır) aşağıda listelenmiştir.

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.

Popüler teknikler

Yazılım sistemleri

Ayrıca bakınız: İspat yardımcısı § Karşılaştırma ve Kategori:Teorem ispatlayan yazılım sistemleri
Karşılaştırmak
İsim Lisans türü internet servisi Kütüphane bağımsız Son güncelleme ( YYYY-aa-gg biçimi )
ACL2 3 tümceli BSD Numara Numara Evet Mayıs 2019
Prover9/Su samuru Kamu malı Via TPTP Sistem Evet Numara 2009
japon GPLv2 Evet Evet Numara 15 Mayıs 2015
PVS GPLv2 Numara Evet Numara 14 Ocak 2013
Aslan II BSD Lisansı Via TPTP Sistem Evet Evet 2013
EQP ? Numara Evet Numara Mayıs 2009
ÜZGÜN GPLv3 Evet Evet Numara 27 Ağustos 2008
PhoX ? Numara Evet Numara 28 Eylül 2017
Keymaera GPL Via Java Webstart Evet Evet 11 Mart 2015
Gandalf ? Numara Evet Numara 2009
E GPL Via TPTP Sistem Numara Evet 4 Temmuz 2017
SNARK Mozilla Kamu Lisansı 1.1 Numara Evet Numara 2012
Vampir Vampir Lisansı Via TPTP Sistem Evet Evet 14 Aralık 2017
Teorem Kanıtlama Sistemi (TPS) TPS Dağıtım Sözleşmesi Numara Evet Numara 4 Şubat 2012
SPAS FreeBSD lisansı Evet Evet Evet Kasım 2005
IsaPlanlayıcısı GPL Numara Evet Evet 2007
Anahtar GPL Evet Evet Evet 11 Ekim 2017
Prenses lgpl v2.1 Via Java Webstart ve TPTP Sistem Evet Evet 27 Ocak 2018
iProver GPL Via TPTP Sistem Numara Evet 2018
Meta Teoremi ücretsiz Numara Numara Evet Nisan 2020
Z3 Teoremi Kanıtlayıcısı MIT Lisansı Evet Evet Evet 19 Kasım 2019

Ücretsiz yazılım

Tescilli yazılım

Ayrıca bakınız

Notlar

Referanslar

  • Çene-Liang Chang; Richard Char-Tung Lee (1973). Sembolik Mantık ve Mekanik Teorem Kanıtlaması . Akademik Basın .
  • Loveland, Donald W. (1978). Otomatik Teorem Kanıtı: Mantıksal Bir Temel. Bilgisayar Bilimlerinde Temel Çalışmalar Cilt 6 . Kuzey Hollanda Yayıncılık .
  • Luckham, David (1990). Spesifikasyonlarla Programlama: Anna'ya Giriş, Ada Programlarını Belirtmek İçin Bir Dil . Springer-Verlag Metinleri ve Bilgisayar Bilimlerinde Monograflar, 421 pp. ISBN 978-461396871.

Dış bağlantılar