Abstract:

In this project we propose to study two important aspects of knowledge: learning and communication. Our approach is computational. Thus on the one hand our theories of learning and communication are formulated mathematically and as computational processes, and on the other hand, as a consequence of being computational these theories lend themselves to fairly direct computer implementation, both for experimentation and for development of applications. Learning and communication are interelated; for example learning a language involves trial communication, and participation in communication typically leads to learning. Here we structure our investigation of these mixed fields in three broad categories: Learning, Learning/Communication, and Communication, each subdivided into theory and applications, with theory generally providing the necessary foundations for applications. The learning theory part studies entailment bases for query learning and machine learning and mining in data streams; learning applications are public health, finance and social networks. The learning/communication theoretical part covers learning probabilistic finitestate machines as models for formal languages; the learning/communication applications are animal communication, child language evolution and acquisition of semantics. The communication theoretical part includes model theory and proof theory of categorial logic; the communication applications are parsing/theorem-proving and computational grammars of English, Catalan and Spanish.]]>

Abstract:

This project pivots around the satisfiability and constraint optimization problems for logical languages including propositional logic (SAT) and more general expressive constraint satisfaction problems (CSP). Our purpose is to conduct frontier research in this area exploiting the expertise of the four groups that participate in the project. TASSAT 2 is the continuation of the project that gives birth to it, TASSAT, that already proved its potential and viability. For this reason, the main objectives of this project are partly follow-ups on those of the previous project and partly new, with the following concrete goals in particular: In SAT we want to continue studying the structure of instances arising in industry, and apply this knowledge to develop more efficient solvers, both for SAT and for MAXSAT. In CSP we want to continue contributing to the problem of classification of tractable constraint languages. We will also study algorithms for geometric instances of MAXCSP and combinatorial problems of interest in computational complexity theory. An important novelty of the present proposal is its stronger emphasis in the implementation of practical solvers, including new branch-and-bound algorithms for MAXSAT, soft learning for MAXSAT, better variable selection techniques, portfolios, etc. We want to expand our presence in international solver competitions and participate in the solution of industrial problems. Another significant novelty in the goals is that we plan to expand the range of applications of the geometric methods to include graph isomorphism problems and other structures of interest in combinatorics and other areas of science. This new goal derives from some of the results obtained in the previous project that already had a notable international impact. Efficiency appears as one of the keywords in the ICT-related activities of the European H2020 (see SC4 and SC5 in "Societal challenges"). This may refer to efficiency in energy distribution, logistics applications, etc. SAT and MAXSAT solvers are a relatively new technology for optimization that can be applied in some of these areas. One of our goals in this project is to consolidate a consortium of research groups in the area, to compete in the application of European research projects.]]>

Abstract:

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 Almería, and (g) fuzzy scheduling for resource usage within cloud data centers with the Umeå 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.]]>