Tez No	İndirme	Tez Künye	Durumu
476643		Linear planning logic and linear logic graph planner: Domain independent task planners based on linear logic / Doğrusal planlama mantığı ve doğrusal mantık grafik planlayıcı: Doğrusal mantık tabanlı alan bağımsız görev planlayıcılar Yazar:SITAR KORTİK Danışman: PROF. DR. VAROL AKMAN Yer Bilgisi: İhsan Doğramacı Bilkent Üniversitesi / Mühendislik ve Fen Bilimleri Enstitüsü / Bilgisayar Mühendisliği Ana Bilim Dalı / Bilgisayar Mühendisliği Bilim Dalı Konu:Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrol = Computer Engineering and Computer Science and Control Dizin:	Onaylandı Doktora İngilizce 2017 170 s.
Doğrusal mantık, tek kullanımlık varsayımları kullanmaya zorlayan tekdüze ol- mayan bir mantık olduğu için, dinamik durumlu alanları etkili olarak göstermeye olanak sağlıyor. İçinde, bir robotun durumunda fiziksel ve bilgisel bileşenlerin bir- likte tekdüze olmayan özellikler sergilendiği robotik görev planlaması, bu tür alan- lar için önemli bir örnektir. STRIPS planlama problemleri için, doğrusal mantıkta ispatları otomatik ortaya çıkaracak iki adet yeni ve etkili teorem ispatlayıcı or- taya koyuyoruz. Ortaya koyduğumuz ilk planlayıcı olan Doğrusal Planlama Mantığı, Prolog ve Lolli gibi programlama dillerinde sıkça kullanılan geriye zincir- leme prensibiyle çalışmaktadır ve atomik olmayan sonuçları da ele alacak şekilde genişletilmiştir. Bu yeni planlayıcının deneysel bir uygulaması olan RHex robotu için görsel yönlendirmeyle otomatik gezinme, robotik görev planlayıcı kapsamında gösterilmiştir. Ortaya koyduğumuz ikinci planlayıcı olan Doğrusal Mantık Grafik Planlayıcısı, doğrusal mantık için grafik tabanlı teorem ispaylayıcı olarak formüle edilmis, rastgele olmayan ve eş zamanlı alanlar icin otomatik bir planlayıcıdır. Bu yeni grafik tabanlı teori ispatlayıcı, çoklu sayıdaki özdeş nesnelerin olduğu zamanlarda (sürü icindeki robotlar, büyük fabrikadaki parçalar), özellikler plan- lama problemleriyle alakası olmayan ispat permütasyonlarını azaltarak planlama performansını arttırıyor. İkinci planlayıcının, eş zamanlı üretim alanında eylem planlaması icin uygulamasını örnek üzerinde gösteriyoruz ve literatürde farklı problem tiplerinde ve alanlarında performanslarıyla bilinen, dört farklı otomatik planlayıcı olan BlackBox, Symba-2, Metis ve Temporal Fast Downward (TFD) ile karsılaştırmasını sağlıyoruz. Yeni planlayıcımızın herhangi bir buluşsala bağlı olmamasına rağmen, diğer sistemleri çoklu özdeş nesnelerin varlığında eş zamanlı alanlarda yendiğini gösteriyoruz. Simetri azaltma ve sayısal akışkanlar ile ilgili mevcut metodlar kullanılsa bile, yukarıdaki kazanımlar sürüyor ve yeni plan- layıcımız binlerce nesneli problemleri çözebiliyor. Bu çıkarımlara ek olarak, bu yeni planlayıcı ile plan oluşturmanın, çoklu küme yeniden yazım sistemlerine eşit olduğunu gösteriyoruz.
Linear Logic is a non-monotonic logic, with semantics that enforce single-use assumptions thereby allowing native and efficient encoding of domains with dy- namic state. Robotic task planning is an important example for such domains, wherein both physical and informational components of a robot's state exhibit non-monotonic properties. We introduce two novel and efficient theorem provers for automated construction of proofs for an exponential multiplicative fragment of linear logic to encode deterministic STRIPS planning problems in general. The first planner we introduce is Linear Planning Logic (LPL), which is based on the backchaining principle commonly used for constructing logic programming languages such as Prolog and Lolli, with a novel extension for LPL to handle program formulae with non-atomic conclusions. We demonstrate an experimen- tal application of LPL in the context of a robotic task planner, implementing visually guided autonomous navigation for the RHex hexapod robot. The sec- ond planner we introduce is the Linear Logic Graph Planner (LinGraph), an automated planner for deterministic, concurrent domains, formulated as a graph- based theorem prover for a propositional fragment of intuitionistic linear logic. The new graph-based theorem prover we introduce in this context substantially improves planning performance by reducing proof permutations that are irrele- vant to planning problems particularly in the presence of large numbers of objects and agents with identical properties (e.g. robots within a swarm, or parts in a large factory). We illustrate LinGraph's application for planning the actions of robots within a concurrent manufacturing domain and provide comparisons with four existing automated planners, BlackBox, Symba-2, Metis and the Tempo- ral Fast Downward (TFD), covering a wide range of state-of-the-art automated planning techniques and implementations that are well-known in the literature for their performance on various of problem types and domains. We show that even though LinGraph does not rely on any heuristics, it still outperforms these sys- tems for concurrent domains with large numbers of identical objects and agents, finding feasible plans that they cannot identify. These gains persist even when existing methods on symmetry reduction and numerical fluents are used, with LinGraph capable of handling problems with thousands of objects. Following these results, we also formally show that plan construction with LinGraph is equivalent to multiset rewriting systems, establishing a formal relation between LinGraph and intuitionistic linear logic.