Hard decision and optimization problems are present in many applications of computational tools. Some challenging questions are: how do we schedule a professional sports league, whether a cryptographic protocol is safe, whether there is some input data that will cause a program to hang or produce
wrong output, which is the most convenient time slot for a video conference, how can a flexible admission control for safe overbooking be defined for cloud computing, or how a flexible text cataloging and information retrieval can be defined for the (semantic) web.
A declarative approach to solve such problems consists in modelling the problem in some logical framework and then applying powerful logic-based techniques to analyse and/or solve the resulting model. In this setting, problems can often be formulated using mathematical formulas or other logic based languages. Once the problem is expressed in the corresponding language we can use existing general techniques or develop novel ones to solve it. When this approach is applied to our specific problems, we might need to use some of their particularities in order to improve its performance. However, thanks to the initial abstraction from particular problems to general problems expressed in a given language, this "declarative approach" makes the development of tools to solve hard real problems significantly easier and faster. As logical frameworks we will mainly use (extensions of) propositional and first-order logic. In particular, we will consider: SAT (satisfaction of
propositional formulas), SAT modulo theories (SMT, where propositions are replaced by atoms in the given theory), Constraint Programming (CP, where clauses are replaced by predicates over a pre-defined language), Fuzzy Logic (FL, where clauses have some uncertainty), Rewrite Logic (RWL, with modelling and programming advanced capabilities), Logic Programming (LP), and Fuzzy Logic Programming (FLP). In this project we will focus on the combination and extension of these successful formal languages to get the necessary expressiveness for our practical applications. Guided by applications for scheduling and planning, for security, for agents, for machine learning, for concurrent and sequential program analysis, for bio-informatics or for XML manipulation, we will develop efficient algorithms and tools to solve problems described in the previous logical frameworks.
As precise applications we consider: (a) sports scheduling as done with Hypercube and KNVB, the Netherlands, (b) program analysis in collaboration with Microsoft Research at Cambridge, (c) evaluation of transcript sequences in collaboration with the Centre for Genomic Regulation (CRG) in Barcelona, (d) security in collaboration with the University of Illinois at Urbana-Champaign and the Naval Research Laboratory at Washington, (e) new features in the Maude language with the University of Illinois at Urbana-Champaign and SRI International in California, (f) knowledge discovering and flexible manipulation of data retrieved from the web in collaboration with the University of Almeria, and (g) fuzzy scheduling for resource usage within cloud data centers with the Umea University.
This is therefore a project that covers all the way in the development and application of computer technologies from the basic theory and techniques to industrial and social impact problems.