Mechanical theorem proving in classical geometry

Abstract

ÖZET DÜZLEM GEOMETRİ KURAMLARININ BİLGİSAYARLA KANITLANMASI DUYGULUER, Fer ruh Yüksek Lisans Tezi, Bilgisayar Mühendisliği Bölümü Tez Yöneticisi : Doç. Dr. Müren Gökeri Orta Doğu Teknik Üniversitesi Aralık 1987, 160 sayfa Bu tez düzlem geometrinin bir alt kümesinde çalışan bir yazılımı anlatmaktadır. Yazılımda tümevarım ve tümdengelim yöntemleri kullanılmakta ve tümdengelim yönteminden daha etkin olarak yararlanılmaktadır. Bu yöntem, kuramı daha basit parçalara ayırarak çözüme gitme temeline dayanmaktadır. Bu parçalar aksiyomlar yada daha önce kanıtlanmış kuramlardır. Tümevarım yöntemi ise, varsayımlardan yola çıkarak yeni iddialar üretmekte kullanılmaktadır. Bunların yanısıra, tezde bilgisayarla kuramların kanıtlanmasına ilişkin kavramlar ve tarihsel gelişmeler de sunulmaktadır. Yazılım 1MB PC üzerinde Prolog dili kullanılarak geliştirilmiştir. Anahtar Kelimeler: Kuram kanıtlama, bilgisayarla kuramların kanıtlanması.tümevarım, tümdengelim, Prolog. iv

ABSTRACT MECHANICAL THEOREM PROVING IN CLASSICAL GEOMETRY DUYGULUER, Ferruh M.S. in Computer Engineering Middle East Technical University Supervisor: Assoc. Prof. Dr. Muren Gokeri December 1987, 160 Pages This thesis describes a software which operates on a subset of plane geometry. The program employs a combination of forward and backward inference mechanisms with backward component playing a more important role. The backward mechanism splits a theorem into more easily proved parts. These are axioms or previously proved theorems. Forward mechanism is used to generate new assertions from hypotheses, in order to reduce the search time of backward component. In addition to these, the thesis covers the theory and the historical background of the mechanical theorem proving. The software was developed on an IBM PC. Key words : Theorem proving, mechanical theorem proving, forward and backward inference, Prolog. iii