A comparative study of theorem provers
Teorem ispatlama sistemlerinin karşılaştırılmasıyla ilgili bir çalışma
- Tez No: 374438
- Danışmanlar: Assist. Prof. Dr. AYTEKİN VARGÜN
- Tez Türü: Yüksek Lisans
- Konular: Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrol, Computer Engineering and Computer Science and Control
- Anahtar Kelimeler: Belirtilmemiş.
- Yıl: 2014
- Dil: İngilizce
- Üniversite: Melikşah Üniversitesi
- Enstitü: Fen Bilimleri Enstitüsü
- Ana Bilim Dalı: Elektrik ve Bilgisayar Mühendisliği Ana Bilim Dalı
- Bilim Dalı: Belirtilmemiş.
- Sayfa Sayısı: 92
Özet
Teorem ispatlayıcılar ve ispat yardımcıları genellikle matematiksel problemleri çözmek için ya da yazılım ve donanımların formal olarak doğrulanmasında kullanılır. Yazılımların bakım işleminin yüksek maliyetli olmasını engellemek için müşterilere doğru ve güvenli kod teslim etmek kritiktir. Bu aynı zamanda vazgeçilmezdir çünkü sağlık, havacılık ve nükleer reaktörler ve benzeri alanlarla ilişkili uygulamalarda yaşamı tehdit eden problemlere neden olabilir. Teorem ispatlayıcıların kullanılmasıyla yapılabilen formal doğrulama, yüksek doğruluk ve güvenirliliğin garanti edilmesini sağlar. Teorem ispatlama süreci güvenilirlik, doğrululuk, ve diğer matematiksel özelliklerin ifade edilmesini (yazılmasını) ve bunlarla ilgili ispatların yazılması işlemini gerektirir. Bazı teorem ispatlayıcılar tamamıyla otomatiktir ancak birçok durumda ispatlama işleminin tamamlanabilmesi için kullanıcının sistemi yönlendirmesi gerekir. Uygun teorem ispatlayıcının seçimi kolay bir işlem değildir. Halihazırda ispat yazmada yardım sağlayabilen pek çok teorem ispatlayıcı vardır. Bazı uygulamalar ispatların detaylı bir şekilde yazılmasına ihtiyaç duyarken diğer bir kısmı ise tam otomasyon gerektirir. Bu tezdeki çalışma, Athena, Coq, ve Isabelle isimli üç popüler teorem ispatlayıcıyı karşılaştırmayı amaçlamaktadır. Bunu yapabilmek için farklı alanları temsil eden örnek problemler seçtik ve bunlarla ilgili formal tanımlamalar ve ispatlar yazdık. Bu süreçte, ispatların otomatik olarak yazılabilmesi, okunabilirlik, hatalardan temizleme ve belgeleme gibi kriterleri kullanarak bu yazılımları karşılaştırdık.
Özet (Çeviri)
Theorem provers and proof assistants are mainly used for solving mathematical problems or in formal verification of software and hardware. It is critical to deliver correct and safe code to customers to prevent high cost of software maintenance. This is also indispensable and can cause life-threatening problems in applications that are related to health, aerospace, nuclear reactors, etc. Formal verification via theorem provers provides high assurance of correctness and safety. The theorem proving process requires writing specifications and proofs of properties that identify safety, correctness or other mathematical features. Some theorem provers are fully automatic but in many cases interaction with proof assistants is required to complete the proof process. The choice of suitable theorem prover is not an easy process. There are currently many theorem provers which can provide help in writing proofs. Some applications may require proofs to be written in detail while some requires complete automation. The work in this thesis attempts to compare three popular theorem provers which are Athena, Coq and Isabelle. We selected representative examples from different domains and used each theorem prover to write formal proofs. During these steps, we compared these tools based on some criteria which include proof automation, readability, debugging, and documentation.
Benzer Tezler
- Özne ontolojisi üzerine gramatolojik bir araştırma
A grammatological research on subject ontology
ANIL ÜNAL
Doktora
Türkçe
2020
FelsefeMimar Sinan Güzel Sanatlar ÜniversitesiFelsefe Ana Bilim Dalı
DOÇ. DR. ÖZGE EJDER JOHNSON
- Üçüncü mertebeden Rivlin-Ericksen akışkanının biri sabit diğeri hareketli olan kesişen iki düzlem arasındaki yavaş akımı
The Creeping flow of the third-order Rivlin-Ericksen fluid between intersecting planes, one of which is stationary and the other moving
SERDAR BARIŞ
- Bulanık mantık kontrolör ile klasık PID kontrolör algoritmalarının karşılaştırılması
Comparative study of PID controllers and fuzzy logic controllers
ÇİĞDEM ERGÜVEN
Yüksek Lisans
Türkçe
1999
Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrolİstanbul Teknik ÜniversitesiDOÇ.DR. İBRAHİM EKSİN
- Determination of parameter regions for diagonal dominance and stability of MIMO systems
MIMO sistemlerin köşegen baskınlığı ve kararlılığı için parametre bölgelerinin belirlenmesi
İLHAN MUTLU
Doktora
İngilizce
2017
Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrolİstanbul Teknik ÜniversitesiKontrol ve Otomasyon Mühendisliği Ana Bilim Dalı
PROF. DR. MEHMET TURAN SÖYLEMEZ
- A comparative assessment of seismic soil liquefaction triggering relationships
Sismik zemin sıvılaşması tetiklenme bağıntılarının kıyaslamalı değerlendirilmesi
MAKBULE ILGAÇ
Yüksek Lisans
İngilizce
2015
İnşaat MühendisliğiOrta Doğu Teknik Üniversitesiİnşaat Mühendisliği Ana Bilim Dalı
PROF. DR. KEMAL ÖNDER ÇETİN