Bilkent University
Department of Computer Engineering
S E M I N A R
Constructing Robotic Plans in a Heuristic-Based Theorem Prover
Sitar Kortik
Ph.D. Student
Computer Engineering Department
Bilkent UniversityWe know that intuitionistic linear logic is a good tool for encoding planning problems.
In my M.S. thesis, intuitionistic linear logic is used for this reason. The main scope of the M.S. thesis is implementing a backwards theorem prover with resource management and constraints within the intuitionistic linear logic for robotic planning problems. We gained valuable experiences in backwards theorem provers and proof search in linear logic during the M.S. study. However, we also encounter some efficiency issues in the introduced theorem prover. In the PhD study, we want to carry these experiences forward for robotic planning and also want to mitigate the efficiency issues in theorem provers. Recently, we progressed on a fragment of intuitionistic linear logic which we call Linear Planning Logic (LPL). This new language is an extension of linear hereditary Harrop formulas (LHHF), with the addition of negative occurrences of simultaneous conjunction and multiplicative unit. In LPL, we construct proof terms for proofs.
Here, constructed proofs are annotated proof terms which are created in the theorem prover. In the scope of PhD thesis, we execute the constructed proofs by the theorem prover for the robotic planning problems such as manipulation planning, product assembly line compilation and mobile robot planning. From the nature of proof search in theorem provers, there are some efficiency issues. For improving the efficiency of the proof search, we can introduce a heuristic-based theorem prover. Another efficiency issue that we want to handle is loop detection and loop preventing in the proof search.
DATE: 08 October, 2012, Monday @ 15:40
PLACE: EA409