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

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.