A backwards theorem prover with focusing, resource management and constraints for robotic planning within intuitionistic linear logic

Abstract

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.

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.