Research Projects Topics
Tools and Methodologies for Verifying Answer Set Programs
This project encompasses a number of research ventures falling under the umbrella topic of formal verification of answer set programs. These can be roughly divided into three interrelated categories. The first is the task of developing semantics for advanced ASP language constructs (aggregates and conditional literals) that do not refer to grounding. This allows ASP practitioners to reason formally about the correctness of their programs without reference to a particular input. The second category seeks to enhance modularity in Answer Set programs. From a formal verification perspective, it is desirable to reason about program components in isolation. This allows proofs of correctness for sub-programs to be recycled, and simplifies the task of verifying extended programs. Finally, the ability to automatically verify programs will make widespread adoption of formal methods for ASP development much more palatable.
Automated Optimization of Programs and Processing Tools in Answer Set Programming
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.
Modularity For Modeling And Solving In Declarative 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 And Solving
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.
Cmodels(DIFF) | Cmodels | Sup
Constraint Answer Set Programming
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.
What Lexical Wide Coverage Resources Can Do For Parsing and Information Extraction
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.