Geri Dön

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

  1. Tez No: 255979
  2. Yazar: SITAR KORTİK
  3. Danışmanlar: YRD. DOÇ. DR. ULUÇ SARANLI
  4. Tez Türü: Yüksek Lisans
  5. Konular: Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrol, Computer Engineering and Computer Science and Control
  6. Anahtar Kelimeler: Belirtilmemiş.
  7. Yıl: 2010
  8. Dil: İngilizce
  9. Üniversite: İhsan Doğramacı Bilkent Üniversitesi
  10. Enstitü: Mühendislik ve Fen Bilimleri Enstitüsü
  11. Ana Bilim Dalı: Bilgisayar Mühendisliği Ana Bilim Dalı
  12. Bilim Dalı: Belirtilmemiş.
  13. 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

  1. Mechanical theorem proving in classical geometry

    Başlık çevirisi yok

    FERRUH DUYGULUER

  2. 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

    İngilizce

    2021

    MatematikKoç Üniversitesi

    Matematik Ana Bilim Dalı

    PROF. MİNE ÇAĞLAR

    PROF. ALİ SÜLEYMAN ÜSTÜNEL

  3. 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

    Türkçe

    2016

    Mühendislik BilimleriKocaeli Üniversitesi

    Elektronik-Bilgisayar Eğitimi Ana Bilim Dalı

    PROF. DR. NAMIK YENER

  4. 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

    Türkçe

    1993

    Elektrik ve Elektronik Mühendisliğiİstanbul Teknik Üniversitesi

    PROF.DR. BİNGÖL YAZGAN

  5. İ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

    Türkçe

    1994

    Elektrik ve Elektronik Mühendisliğiİstanbul Teknik Üniversitesi

    PROF.DR. AHMET HAMDİ KAYRAN