A backwards theorem prover with focusing, resource management and constraints for robotic planning within intuitionistic linear logic
Robotik planlama için odaklanma, kaynak yönetimi ve kısıtlamaların katılarak hedefe yönelik teorem ispatlamanın sezgisel doğrusal mantıkta gerçekleştirimi
- Tez No: 255979
- Danışmanlar: YRD. DOÇ. DR. ULUÇ SARANLI
- 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: 2010
- Dil: İngilizce
- Üniversite: İhsan Doğramacı Bilkent Üniversitesi
- Enstitü: Mühendislik ve Fen Bilimleri Enstitüsü
- Ana Bilim Dalı: Bilgisayar Mühendisliği Ana Bilim Dalı
- Bilim Dalı: Belirtilmemiş.
- Sayfa Sayısı: 107
Özet
Bu tezin ana kapsamı, robotik planlama problemleri için, odaklanma, kaynak yöönetimi ve kısıtlamaların da dahil edilerek, sezgisel doğrusal mantıkta, hedefe yönelik bir teorem ispatlama çatısı oluşturmak. Bu amaçla, hedefe yöönelik formöulasyon şekli, uygulama ve test aşamasında daha anlaşılır bir içerik sunmaktadır. Bununla beraber, mevcut hedefe yöonelik teorem ispatlayıcılar, ispat aramada ya etkili bir yööntem sunamamaktadırlar ya da kullandıkları dili Doğgrusal Hereditary Harrop Formöülleri gibi daha köücük parçalara kısıtlayarak etkili bir yööntem sağlayabilmektedirler. Bahsedilen yaklaşımlardan ilki, sonuç sisteminin öölçeklenebilirliğine öönemli derecede zarar verdiği için uygun değildir. İkinci bahsedilen teorem ispatlama yaklaşımlarında ise öölçeklenebilirlik konusu çözüulebilir fakat ifade edebileceği dili kısıtlar ve belirli olmayan planlama elemanlarını ele alamayabilir. Bu tezde tanımladığımız ispatlama teorisi, robotik planlama problemlerindeki dinamik durum elemanlarının ifade edilmesinde, doğrusallığın ve söürekli kısıtlamaların etkili bir biçimde kullanılmasını sağlıyor. Bu amaçla, tanımladığımız sistemin SWI-Prolog dilinde bir uygulamasını gerçekleştirdik. Bu uygulamaya kısıtlamaları da dahil ederek sistemi genişlettik. Sistemimizin ifade gücünü ve verimliliğini, bazı robot planlama öörnekleri vererek destekledik.
Özet (Çeviri)
The main scope of this thesis is implementing a backwards theorem prover with focusing, resource management and constraints within the intuitionistic rst-order linear logic for robotic planning problems. To this end, backwards formulations provide a simpler context for experimentation. However, existing backward theorem provers are either implemented without regard to the eficiency of the proofsearch,or when they do, restrict the language to smaller fragments such as Linear Hereditary Harrop Formulas (LHHF). The former approach is unsuitable since it signicantly impairs the scalability of the resulting system. The latter family of theorem provers address the scalability issue but impact the expressivity of the resulting language and may not be able to deal with certain non-deterministic planning elements. The proof theory we describe in this thesis enables us to efectively experiment with the use of linearity and continuous constraints to encode dynamic state elements characteristic of robotic planning problems. Tothis end, we describe a prototype implementation of our system in SWI-Prolog, and also incorporate continuous constraints into the prototype implementation of the system. We support the expressivity and eficiency of our system with some examples.
Benzer Tezler
- Mechanical theorem proving in classical geometry
Başlık çevirisi yok
FERRUH DUYGULUER
Yüksek Lisans
İngilizce
1987
Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve KontrolOrta Doğu Teknik ÜniversitesiDOÇ. DR. MÜREN GÖKERİ
- Regularity of monge potentials and hedging in a degenerate market
Monge potensiyellerinin düzenliliği and yoz pazarda riskten korunma
İHSAN DEMİREL
Doktora
İngilizce
2021
MatematikKoç ÜniversitesiMatematik Ana Bilim Dalı
PROF. MİNE ÇAĞLAR
PROF. ALİ SÜLEYMAN ÜSTÜNEL
- Kayıpsız optik dalga kılavuzlarında iletilen modların ve metamateryal yüklü kapalı kılavuzlarda geriye doğru dalgaların transmisyon hattı eşdeğerlikleri yöntemi ile incelenmesi
Investigation of transmitted modes of lossless optical waveguides and backward waves of metamaterial loaded closed waveguides with transmission line equivalent method
PELİN KELEBEKLER
Doktora
Türkçe
2016
Mühendislik BilimleriKocaeli ÜniversitesiElektronik-Bilgisayar Eğitimi Ana Bilim Dalı
PROF. DR. NAMIK YENER
- Mikrodalga difraksiyon tomografisi için yeni bir paralel işleme algoritması
A New parallel processing algorithm for microwave diffraction tomography
MESUT KARTAL
Yüksek Lisans
Türkçe
1993
Elektrik ve Elektronik Mühendisliğiİstanbul Teknik ÜniversitesiPROF.DR. BİNGÖL YAZGAN
- İki boyutlu kafes parametrelerinin sınırlı veri alanlarından hesaplanması
The Calculation of the 2-D lattice parameters from short data records
NURŞEN YILDIZ
Yüksek Lisans
Türkçe
1994
Elektrik ve Elektronik Mühendisliğiİstanbul Teknik ÜniversitesiPROF.DR. AHMET HAMDİ KAYRAN