Direkt zum Inhalt | Direkt zur Navigation

Eingang zum Volltext

Lizenz

Bitte beziehen Sie sich beim Zitieren dieses Dokumentes immer auf folgende
URN: urn:nbn:de:bsz:25-opus-87144
URL: http://www.freidok.uni-freiburg.de/volltexte/8714/


Giritli, Mehmet

First-order and modal logics for spatial reasoning

Raum und Logik: Prädikaten- und modallogische Methoden für das räumliche Schließen

Dokument1.pdf (1.251 KB) (md5sum: 2adf6259864050fe8a4d718e1b51d451)

Kurzfassung in Englisch

Spatial representation and reasoning is mainly concerned with the reasoning about our surrounding physical space and has found many applications across various fields including geographical information systems (GIS), robotic navigation, high level vision, spatial propositional semantics of natural languages, engineering design, specifying visual language syntax and semantics, common-sense reasoning about physical systems and document-structure recognition.

There are already various elegant theories of the space developed within mathematics over the centuries, like (point-set) topology and Euclidean (or non-Euclidean) geometry, which can provide a sophisticated basis for the representation of the space. However, developing and investigating the properties of algorithms for reasoning with these theories has not been a topic of interest until the recent attention from certain fields in computer science, especially from the field of artificial intelligence. This thesis aims to contribute formalisms in the form of modal and first-order logics aiming possible applications in different areas of spatial reasoning.

In the first part of the thesis, we introduce logics of comparative distances. Many formalisms in the literature have been devoted to capture the common-sense relationships between objects by using topology. Although topology is a very attractive model for common-sense reasoning about the space due to its computational feasibility, there are many areas where a purely topological representation remains simply inadequate. For example, when two objects are apart from each other (or when they are disconnected' in the appropriate topological terminology), there is nothing more that can be said about their relationship to each other: They could be very close to each other or they could be miles apart from each other -- we can not tell the difference. Hence, there is a certain interest for formalisms that are more expressive than topology and yet somehow remain less expressive than a fully-metric representation.

Logics of comparative distances aim to improve on this, without introducing a fully-metric representation of the space. The novel side of the formalisms is that, instead of quantitatively measuring the distances between points in the space (from which the distance between objects can be obtained), it compares the distances between objects, e.g., if my arm can reach to my computer, but not to my desk lamp then the distance between me and the desk lamp is greater than the distance between me and my computer.' We employ modal and first-order logic formalisms to perform this kind of spatial reasoning and investigate their logical and computational properties. Our results show that, while the first-order comparative distance logic is finitely axiomatisable, the modal comparative distance logic is also finitely axiomatisable and moreover, it has the finite model property and it is decidable, with an NP-complete satisfiability problem.

In the second part of the thesis, we present a modal logic formalism which can talk about angles. Our underlying goal in constructing this logic is not only to obtain a formalism which can reason about mere angles, but to contribute the development of logical formalisms of trigonometry which will eventually deal with angles.

Unfortunately, the angular modal logic presented in this thesis deals only with the angle side of the problem. More precisely, our formalism is only able to reason about the angle information within triangles induced by every trio of points in the space and not the distance information between points. Although there is a discussion at the end of the Chapter on how angles and distances can be combined in a single formalism, this major but important task is a part of the future research agenda.

For the modal language, we use binary modal operators with the usual Kripkean semantics, e.g., $\varphi$ holds at somewhere and $\psi$ holds at somewhere else, with $a$ degrees of angle in between about here.' As we show in the thesis, using this paradigm it becomes a trivial task to express the useful qualitative notions of collinearity´ and betweenness´ as well. We establish that this formalism has the finite model property and it is decidable. The complexity of the satisfiability problem is known to be in NEXPTIME via the proof of the finite model property, but unfortunately a lower bound could not be determined.


Kurzfassung in Sonst.

Mekansal temsiliyet ve uslamlama temelde çevremizdeki fiziksel mekan hakkında akıl yürütmek ile ilgilidir ve coğrafi bilgi sistemleri (GIS), robotik navigasyon, yüksek seviye vizyon, doğal dillerin mekansal önermesel anlambilimi, mühendislik tasarımı, fiziksel sistemler hakkında sağduyusal uslamlama ve belge-yapısı tanınması gibi çeşitli alanlarda birçok uygulamaları olmuştur.

Mekansal temsiliyet için gelişmiş bir temel sağlayabilecek, topoloji ve geometri gibi, yüzyıllar boyunca matematik içerisinde geliştirilmiş muazzam teoriler halihazırda zaten mevcuttur. Ancak, bu teorilerle uslamlamak için algoritmalar geliştirmek ve bu algoritmaların özelliklerini incelemek, bilgisayar bilimi konusunda belirli alanlardan ve özellikle de yapay zeka alanından yakın zamanda gelen dikkate kadar ilgi çeken bir konu olmamıştır. Bu doktora tezi, mekansal uslamlamanın değişik alanlarında olası uygulamaları hedefleyen modal ve birinci-derece mantıklar şeklinde formal sistemlerle katkıda bulunmayı amaçlamaktadır.

Tezin ilk bölümünde, karşılaştırmalı mesafeler mantıklarını tanıtacağız. Literatürde neseler arasındaki sağduyusal bağıntıları topoloji ile yakalamaya çalışan pek çok formal sistem mevcuttur. Hernekadar topoloji, bilişimsel faydaları yüzünden sağduyusal mekansal uslamlama için çok çekici bir model olsa da, sadece topolojik bir temsiliyetin basitçe yetersiz kalacağı pek çok alan da mevcuttur. Örnek olarak, iki nesene birbirlerinden ayrık oldukları zaman (uygun topolojik terminolojiyle 'bağlantısız' oldukları zaman), birbirleriyle olan bağıntı hakkında daha fazla bir şey söylemek mümkün değildir: Birbirlerine çok yakın da olabilirler, çok uzak da --topoloji ile aradaki farkı temsil etmek mümkün değildir. İşte bu yüzden, ifade gücü topolojiden daha yüksek ama yine de tam-metrik bir temsiliyetten daha az bir ifade gücüne sahip formal sistemler için belli bir ilgi vardır.

İşte karşılaştırmalı mesafeler mantığı, uzayın tam-metrik bir temsiliyetine başvurmadan, bu durum üzerinde ilerlemeyi amaçlar. Bu formal sistemlerin en asil yanları ise, uzayın noktaları arasındaki mesafeleri nicel bir şekilde ölçmek yerine (ki buradan da nesneler arasındaki mesafe ölçümü yapılabilir), neseler arasındaki mesafeleri birbirleriyle karşılaştırır, ör., eğer kolum bilgisayarıma ulaşıyor ama masa lambama ulaşamıyorsa, o zaman benimle masa lambam arasındaki mesafe, benimle bilgisayarım arasındakinden daha büyüktür.´ Bu tarz bir mekansal uslamlamayı gerçekleştirebilmek için modal ve birinci-derece mantıkları kullanıp, bunların mantıksal ve bilişimsel özellikleri araştırıldı. Sonuçlarımız şunu gösteriyor ki, bir tarafta birinci-derece karşılaştırmalı mesafeler mantığı sonlu bir şekilde aksiyomlaştırılabilirken, modal karşılaştırmalı mesafeler mantığı da sonlu bir şekilde aksiyomlaştırılabilip, aynı zamanda kararverilebilir ve sonlu model özelliğine sahip olup, tatminedilebilirlik problemi NP-tam'dır.

Tezin ikinci bölümünde, açılar üzerinde kullanılabilecek bir modal mantık formalizasyonu sunacağız. Bu mantığı oluşturmamızdaki temel neden sadece açılar hakkında uslamlama yapabilen bir mantık sistemi elde etmek değil, ama trigonometrinin mantık formalizasyonlarının gelişmesine katkıda bulunmaktır ki, bu sistemlerle açılar hakkında uslamlama da doğal olarak yapılabilecektir.

Maalesef, bu tezin içerisinde sunulan açısal modal mantık bu ana problemin sadece açılarla olan kısmında kullanılabilmektedir. Detaylandırmak gerekirse, sunduğumuz formalizasyon uzaydaki her üç noktanın oluşturacağı bir uçgenin iç açılarıyla ilgili uslamlama yapabilmekte fakat bu noktalar arasındaki mesafelerli buna katamamaktadır. Hernekadar ilgili bölüm sonunda açılar ve mesafelerin nasıl birleştirileceği konusunda bir tartışma olsa da bu büyük fakat önemli görev, gelecek araştırma ajandamızın bir parçasıdır.

Modal dil için, ikili mdodal operatörleri alışılagelmiş Kripke-stili anlambilimi çerçevesinde kullandık, ör., şu anki yer çevresinde aralarında $a$ derece açıyla, bir yerde $\varphi$ ve başka bir yerde de $\psi$ geçerlidir.' Tezde gösterdiğimiz gibi, bu paradigmayı kullanarak doğrudaşlık ´ ve arasındalık´ gibi kullanışlı nitel kavramları ifade etmek de çok kolay bir işe dönüşür. Çalışmalarımız bu fromal sistemin sonlu model özelliğine ve ayrıca kararverilebilir bir tatminedilebilirlik problemine sahip olduğunu gösterdi. Tatminedilebilirlik probleminin karmaşıklığının NEXPTIME içerisinde olduğu, sonlu model özelliği ispatı vasıtasıyla bilinmesine rağmen alt sınırı henüz tespit edilememiştir.


SWD-Schlagwörter: Artificial Intelligence: AI , Prädikat <Logik> , Modallogik , Mathematische Logik , Räumliches Schließen
Freie Schlagwörter (englisch): Artificial Intelligence , Mathematical Logic , Modal Logic , Knowledge Representation and Reasoning , Spatial Reasoning
Institut: Institut für Informatik
Fakultät: Technische Fakultät (bisher: Fak. f. Angew. Wiss.)
DDC-Sachgruppe: Informatik
Dokumentart: Dissertation
Erstgutachter: Nebel, Bernhard (Prof. Dr.)
Sprache: Englisch
Tag der mündlichen Prüfung: 05.09.2011
Erstellungsjahr: 2012
Publikationsdatum: 04.10.2012
Indexliste