Research Projects in Knowledge Representation and Reasoning
Declarative programming tools developed in knowledge representation and reasoning are successfully used in numerous knowledge-intense scientific and industrial applications. Nevertheless, computational knowledge representation is far from realizing its full potential. Even experts in declarative programming expend substantial effort fine-tuning encodings and reasoning tools before acceptable performance is obtained for the domain of interest. Principled performance evaluation and code optimization have been proven essential to imperative programming and software engineering. We are interested in exploring the means for automated optimizations in the realm of computational knowledge representation. One obstacle that we face is that there is no clear basis to explain the relationship between a declarative specification of a problem, its specific instance, and the efficiency of available reasoning tools. Nevertheless, the advances in portfolio solving as well as automatic configuration fields suggest directions for overcoming this obstacle. Applying automatic configuration tools in refining methodology of code optimization in declarative programming is our first step towards an ultimate goal of defining principal methods for automated optimization in declarative constraint programming.
Declarative programming serves as the computational paradigm in qualitative knowledge representation. However, while modularity has long been recognized as one of the key techniques in software development, the research on modular declarative programming formalisms is at an early stage. We are interested in advancing understanding of fundamental issues of declarative programming for modeling and reasoning with multi-logics, formalisms for modular and multi-context knowledge representation, and integrating diverse languages and reasoning tools tailored for problems in large-scale applications in modular knowledge representation settings are the overarching objectives of our project.
Answer Set Programming is a novel declarative constraint programming paradigm inspired by ideas from knowledge representation, logic programming, and non-monotonic reasoning. It found its applications in many computationally intensive tasks including scheduling, planning, difficult search problems in bioinformatics and software verification that require elaboration tolerant solutions. Answer set solving technology extends computational methods of propositional satisfiability in the following way. As a declarative programming paradigm, it provides a rich, simple modeling language that, among other features, incorporates recursive definitions. Answer set programming languages use variables; software tools called grounders are used as front ends of answer set solvers to eliminate variables, whereas SAT-like procedures form their back-ends. Exploiting SAT-based techniques in creating novel solving procedures for answer set programming as well as understanding the landscape of modern answer set solving methods is one of the research questions that we address. Answer set solvers Cmodels(DIFF), Cmodels and Sup are the in-house software systems.
Constraint Answer Set Programming is a novel, promising direction of research whose roots go back to propositional satisfiability. Satisfiability solvers are efficient tools for solving boolean constraint satisfaction problems that arise in different areas of computer science, including software and hardware verification. Some constraints are more naturally expressed by non-boolean constructs. Satisfiability modulo theories extends boolean satisfiability by the integration of non-boolean symbols defined by a background theory in another formalism, such as a constraint processing language. Answer set programming extends computational methods of satisfiability in yet another way. Constraint Answer Set Programming draws on both of these extensions of SAT technology: it integrates Answer Set Programming with constraint processing. We are interested in establishing new computational methods, modeling language dialects for Constraint Answer Set Programming, and studying and comparing existing approaches.
Research Projects in Natural Language Understanding
With the availability of open online ontologies (such as VerbNet and WordNet) describing the use, meaning and functions of words, an opportunity exists to enhance parser technology. We look to bring automated reasoning built on semantic understanding to the processing of language.
In the problem of recognizing textual entailment, the goal is to decide, given a text and a hypothesis expressed in a natural language, whether a human reasoner would call the hypothesis a consequence of the text. One approach to this problem is to use a first-order reasoning tool to check whether the hypothesis can be derived from the text conjoined with relevant background knowledge, after expressing all of them by first-order formulas. Another possibility is to express the hypothesis, the text, and the background knowledge in a logic programming language, and use a logic programming system. We explore the relation of these methods to each other as well as new possibilities for applying symbolic based methods for the task of textual inference.
Choice of Plausible Alternatives (COPA) is a commonsense causal reasoning challenge proposed in 2011. Given an utterance (a) The shirt shrunk. Decide whether an utterance I poured bleach on it or I put in the dryer. is the cause for (a). This challenge targets two areas of research in Artificial Intelligence: natural language processing and knowledge representation and reasoning. We are interested in exploiting knowledge representation and reasoning techniques in identifying solution to this challenge.
Combinatory categorical grammar is one of the grammar formalisms used for natural language parsing. This grammar assigns structured lexical categories to words and uses combinatory rules to combine these categories to parse a sentence. We explore a new approach to parsing that relies on a prominent knowledge representation formalism, answer set programming -- a declarative programming paradigm. Compared to other approaches, there is no need to implement a specific parsing algorithm using such a declarative method. Rather, a programmer encodes the specifications about the combinators of the grammar. This approach is implemented in a parsing tool kit called AspCcgTk that is a wide-coverage natural language parser.
The Winograd Schema Challenge is composed of instances of coreference resolution problems that prove to be difficult for modern natural language processing methods. Ability to perform commonsense inference seems to be the key in tackling this challenge. An approach that takes commonsense reasoning into account is the focus of this project.