Mixture of experts learning in automated theorem proving


Tezin Türü: Yüksek Lisans

Tezin Yürütüldüğü Kurum: Boğaziçi Üniversitesi, FEN BİLİMLERİ ENSTİTÜSÜ, FEN BİLİMLERİ ENSTİTÜSÜ, Türkiye

Tezin Onay Tarihi: 2010

Tezin Dili: İngilizce

Öğrenci: CEMAL ACAR ERKEK

Danışman: TUNGA GÜNGÖR

Açık Arşiv Koleksiyonu: AVESİS Açık Erişim Koleksiyonu

Özet:

Otomatik Teorem İspatlama sistemlerinde başlıca zorluk, arama süreçlerini kısaltacak bir yöntem bulmaktır. Arama süreçlerini kısaltmak için, buluşsal yöntemleri kullanmak önemli bir rol oynar. Bu konuda yapılan çalışmaların sonucunda, çesitli buluşsal yöntemlerle başarılı sonuçlar alınmışsa da, tek bir buluşsal yöntemin tüm problem tiplerinin üstesinden gelemediği gösterilmiştir. Her problem tipinin değişik yaklaşım gerektirmesi, evrensel olarak en iyi buluşsal yöntemin bulunmasını imkansızlaştırır. Bir problem için doğru buluşsal yöntemin belirlenmesi, insan uzmanlar için bile çok zordur. Yeni bir buluşsal yöntem geliştirmek için makina öğrenmesi yöntemlerini kullanabiliriz. Bu tezde önerdiğimiz yaklaşım, sıfırdan yeni bir buluşsal yöntem geliştirmek yerine, uzmanların karışımı yöntemini kullanarak, var olan buluşsal yöntemlerin birleşiminden yeni bir buluşsal yöntem geliştirmektir. Her problem yeni bir yaklaşım gerektirdiği için, önerdiğimiz metot benzer problemlerin çözümlerini öğrenme verisi olarak kullanmaktadır. Çalışmamızın sonuçları, birleşik buluşsal yöntemin, karışımda kullanılan tekil buluşsal yöntemlerin her birinden daha iyi olduğunu göstermiştir.