Using model generation theorem provers for the computation of answer sets
Yanıt kümelerinin hesaplanmasında model oluşturabilen teorem ispatlayıcılarının kullanılması
- Tez No: 255311
- Danışmanlar: DOÇ. DR. FERDA NUR ALPASLAN
- Tez Türü: Doktora
- Konular: Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrol, Computer Engineering and Computer Science and Control
- Anahtar Kelimeler: Bilgi gösterimi, Mantıksal programlama, Teorem ispatlayıcı, Information display, Logic programming, Theorem prover
- Yıl: 2009
- Dil: İngilizce
- Üniversite: Orta Doğu Teknik Üniversitesi
- Enstitü: Fen Bilimleri Enstitüsü
- Ana Bilim Dalı: Bilgisayar Mühendisliği Ana Bilim Dalı
- Bilim Dalı: Belirtilmemiş.
- Sayfa Sayısı: Belirtilmemiş.
Özet
Yanıt kümesi programlama, arama problemlerinin çözülmesinde kullanılan bildirimsel bir yaklaşımdır. Sonuçların yerine koyma yöntemiyle alındığı ispat tabanlı bir yaklaşım değildir. Problemi temsil eden mantık program öyle oluşturulur ki programın yanıt kümesi anlam bilimine göre bulunan modelleri, problemin çözümlerine karşılık gelir.Mantık programının yanıt kümeleri yanıt kümesi çözümleyicisi (Smodels, Cmodels, Clasp ve Dlv) tarafından bulunur. Kullanıcılar kullanım rahatlığı açısından değişkenlerin olduğu programlar yazsalar da, şimdiki yanıt kümesi çözümleyiciler değişkenlerin olmadığı yalın programlarla çalışmaktadır. Yanıt kümesi programlamanın indirgeme süreci, değişkenlerin olduğu bir programın sadece önermelerden oluşan halini oluşturur. İndirgeme süreci çok büyük bir program oluşturabilir. Bu da yanıt kümesi çözümleyicilerinin işini zorlaştırabilir.Model oluşturabilen teorem ispatlayıcılar (Paradox, Darwin ve FM-Darwin) niceleme mantığında verilen bir teori doğru olduğu zaman, teoriyi doğrulayan modeli oluşturabilme yeteneğine sahiptir. Bu çalışmada model oluşturabilen teorem ispatlayıcılarının yanıt kümesi programlamada hesaplayıcı sistem olarak kullanılması önerilmektedir. Ana motivasyon yanıt kümesi programlamada bulunan indirgeme sürecinin kaldırılmasını ya da model oluşturabilen sistemler tarafından daha verimli bir şekilde yapılmasını sağlamaktır. Ayrıca, indirgeme süreci dışında, model oluşturabilen teorem ispatlayıcılar şimdiki yanıt kümesi çözümleyicilerinden daha iyi performans gösterebilir. Önerilen yöntem yanıt kümelerini doğruluk çözümleyicilerini kullanarak bulmaya çalışan yöntemin niceleme mantığı seviyesine çıkarılması olarak görülebilir.Bu çalışmada bir mantık programını niceleme mantığı önermelerine çeviren tamamlamaişleminden yararlanılmıştır. Tamamlama dışında, model oluşturabilen teorem ispatlayıcılara uygun girdiyi oluşturmak için gerekli dönüşümler de incelenmiştir. Tüm bu dönüşümleri gerçekleştirebilen Completor adında bir sistem geliştirilmiştir. Deneysel sonuçlar Completor ve teorem ispatlayıcılarını birlikte kullanmanın yanıt kümelerininhesaplanmasında etkili bir yöntem olduğunu göstermiştir. Özellikle Paradox'un deneylerdeki zaman sonuçları Completor ve Paradox'u birlikte yanıt kümesi çözümleyiciler yerine kullanmanın daha avantajlı olacağını göstermiştir. Bu avantaj sadece önermelerden oluşan halinin çok büyük olduğu programlar için daha açık olarak gözlenmiştir; çünkü bu tür programlar için indirgeme süreci darboğaz teşkil etmektedir.
Özet (Çeviri)
Answer set programming (ASP) is a declarative approach to solving search problems. Logic programming constitutes the foundation of ASP. ASP is not a proof-theoretical approach where you get solutions by answer substitutions. Instead, the problem is represented by a logic program in such a way that models of the program according to the answer set semantics correspond to solutions of the problem.Answer set solvers (Smodels, Cmodels, Clasp, and Dlv) are used for finding answer sets of a given program. Although users can write programs with variables for convenience, current answer set solvers work on ground logic programs where there are no variables. The grounding step of ASP generates a propositional instance of a logic program with variables. It may generate a huge propositional instance and make the search process of answer set solvers more difficult.Model generation theorem provers (Paradox, Darwin, and FM-Darwin) have the capability of producing a model when the first-order input theory is satisfiable. This work proposes the use of model generation theorem provers as computational engines for ASP. The main motivation is to eliminate the grounding step of ASP completely or to perform it more intelligently using the model generation system. Additionally, regardless of grounding, model generation systems may display better performance than the current solvers. The proposed method can be seen as lifting SAT-based ASP, where SAT solvers are used to compute answer sets, to the first-order level for tight programs.A completion procedure which transforms a logic program to formulas of first-order logic is utilized. Besides completion, other transformations which are necessary for forming a firstorder theory suitable for model generation theorem provers are investigated. A system called Completor is implemented for handling all the necessary transformations. The empirical results demonstrate that the use of Completor and the theorem provers together can be an efective way of computing answer sets. Especially, the run time results of Paradox in the experiments has showed that using Completor and Paradox together is favorable compared to answer set solvers. This advantage has been more clearly observed for programs with large propositional instances, since grounding can be a bottleneck for such programs.
Benzer Tezler
- Buğdayda farklı melezleme teknikleri kullanarak tohum tutma oranının saptanılması
Başlık çevirisi yok
İSMAİL TÜZÜN
Yüksek Lisans
Türkçe
1986
ZiraatUludağ ÜniversitesiTarla Bitkileri Ana Bilim Dalı
PROF. DR. HALİS RUHİ EKİNGEN
- Antakya tarihi ticaret merkezi mekansal yapı değişim ve gelişim sürecinin kent ticaret merkezi planlamasına etkinliği
The Effectiveness of spatial structural chance and development period of the historical trade center of Antakya in the urban trade planning
NEVİN TURGUT
Yüksek Lisans
Türkçe
1986
Şehircilik ve Bölge PlanlamaGazi ÜniversitesiŞehir ve Bölge Planlama Ana Bilim Dalı
YRD. DOÇ. DR. NURCAN UYDAŞ
- Pik demiri ve karbon çeliğinin sulu çözeltiler içindeki korozyon hızının tayini
Determination of the rate of corrosion of the cast iran and carbon steel in the aqueous solutions
EMİNE NAZAN ÜNAL
Yüksek Lisans
Türkçe
1985
Kimya MühendisliğiGazi ÜniversitesiKimya Mühendisliği Ana Bilim Dalı
DOÇ. DR. HAYRİ YALÇIN
- Bazı esterlerin kinetik incelenmesi ve termodinamik parametrelerin belirlenmesi
Kinetic study and detesmination of thermodnamic parameters of some esters
İBRAHİM TAŞ
Yüksek Lisans
Türkçe
1986
Kimya MühendisliğiUludağ ÜniversitesiKimya Ana Bilim Dalı
PROF. DR. MUSTAFA CEBE
- Çoklu amaçların çözümlemesinde amaç programlaması ile genelleştirilmiş ters yaklaşımı ve yem sanayiinde bir uygulama
Goal programming and generalieed inverse approaches in the multi-objective analysis and application in feed industry
HASAN BAL