A comparative study of theorem provers

Abstract

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.

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.