Topics we are concerned with
The Winograd Schema Challenge (WSC) has been proposed as an alternative to the Turing Test for measuring a machine’s intelligence by letting it solve pronoun resolution problems that cannot be tackled by statistical analysis alone, but require commonsense, everyday background knowledge and some form of deeper "understanding" of the question. WSCs are thus hard to solve for machines, but easy for humans.
Many solutions so far are based on machine learning and natural language processing, and achieve results that are hardly better than guessing. Moreover, most knowledge-based approaches to the WSC have been purely theoretical. The goal of this thesis was to develop and implement a knowledge-based WSC solver. In particular, a logic of conditional beliefs called BO is employed that is capable of dealing with incomplete or even inconsistent information (which commonsense knowledge often is). It does so by formalising the observation that humans often reason by picturing different contingencies of what the world could be like, and then choose to believe what is thought to be most plausible. Relevant commonsense background information furthermore is obtained from the ConceptNet semantic network and translated into BO, and processed by the Limbo reasoner.
The goal of this thesis was to integrate Answer Set Programming (ASP) into a Golog system in order to obtain an agent framework that is capable of efficient non-monotonic reasoning with introspection.
The action language GOLOG has been used, among other things, for the specification of the behaviour of mobile robots. Since the task of such autonomous systems is typically open-ended, their GOLOG programs are usually non-terminating. To ensure that the program will let the robot exhibit the intended behaviour, it is often desirable to be able to formally specify and then verify the desired properties, which are often of a temporal nature. This task has been studied within our preliminary work from two perspectives: On the one hand, the problem was tackled for very expressive specification and action program formalisms, but without the goal of achieving decidability, i.e. the developed verification methods were not guaranteed to terminate. On the other hand, the verification problem was studied for action formalisms based on decidable description logics and very limited means of specifying admissible sequences of actions, which allowed us to show decidability and complexity results for the verification problem. The purpose of this project is to combine the advantages of both approaches by, on one hand, developing verification methods for GOLOG programs that are effective and practically feasible and, on the other hand, going beyond the formalisms with very limited expressiveness to enhance their usefulness. Among other things, both qualitative and quantitative temporal program properties will be addressed.