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

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.