La recerca del nostre grup "Lògica i Programació" s'emmarca en el desenvolupament de tècniques i eines per a l'aplicació de la lògica a la resolució de sistemes de restriccions. Més concretament, les principals línies de la nostra investigació es basen per una banda en (a) l'estudi de mètodes de resolució de problemes mitjançant resolvedors de satisfactibilitat proposicional (SAT), de satisfactibilitat mòdul teories (SMT), de programació amb restriccions (CP), i d'extensions d'aquests a optimització (Max-SAT, Max-SMT); i (b) per una altra en l'aplicació d'aquests mètodes per atacar problemes complexos d'interès pràctic, com ara de planificació industrial o d'anàlisis de programes. Mentre que la recerca de tipus més teòric és presentada a les conferències i revistes internacionals de més prestigi de les respectives àrees, els resultats en la vessant més pràctica es materialitzen en transferència de tecnologia en empreses tant de dins com de fora de Catalunya.

http://futur.upc.edu/LOGPROG

The group carries out research in basic computer science. In particular, it has internationally-recognised expertise in the (closely related) fields of logic in computer science, computational complexity and constraint-solving problems, and in the use of advanced programming techniques (e.g. constraint programming, automated deduction, etc.) for the development of practical software tools.

In what follows, we give a brief overview of these research lines. Logic has been called "the calculus of computer science", because its role in computer science is similar to that of mathematics in the physical sciences (see, for example, www.cs.rice.edu/~vardi/logic).

Similarly to the way in which architects and engineers analyse their designs mathematically, computer scientists use logic to analyse systems¿ properties (e.g. correctness, safety and security), during all the phases of their life cycles (e.g. specification, development, verification and maintenance). Also, for systems whose efficiency is critical, logic-based analysis can be very helpful, and in all kinds of systems, logic-based techniques help to reduce costs (see, for example, the section on software productivity tools at research.microsoft.com). Hence, it is not surprising that there is an increasing tendency to use logic-based formalisms in all kinds of hardware and software systems and their components, such as databases or programming languages, among others.

Computational complexity involves the study of the resources required during computation to solve a given problem. The most common resources are time (number of computation steps) and space (amount of memory). Other resources can also be considered, such as randomness (how randomness can increase efficiency) and parallelism (how the use of parallel processors can help). Today, the connections between logic and complexity are well established. For example, the field of proof complexity involves the study of the mathematical relationships between complexity classes (i.e. classes of problems that are solvable using the same amount of resources) and the length of proofs in certain logical systems. This field arose as an approach to the well-known problem of whether the P class of problems equals the NP class or not (see the million-dollar prizes at www.claymath.org): if one could show that, for every propositional proof system, there is a class of tautologies with no short proofs, then the answer is negative. The study of the limitations of proof systems has also led to the discovery of important new algorithms.

Constraint programming is the study of computational systems based on constraints. It has recently emerged as an area of research that engages researchers from a variety of fields. The idea is to solve problems by stating constraints (i.e. conditions, properties) that must be satisfied by the solution. Constraint programming consists of the generation of requirements (constraints) and the solution of these requirements by specialised constraint solvers. It has been successfully applied in numerous domains, including computer graphics (to express geometric coherence), natural language processing (to construct efficient parsers), database systems (to ensure and/or restore the consistency of the data), operations research (optimisation problems), molecular biology (DNA sequencing), business applications (option trading), electrical engineering (to locate faults), circuit design (to compute layouts), etc. Most, if not all, of these practical problems fall into the complexity class of NP-complete problems, for which proof complexity results give insight into classes of deterministic algorithms.

The research group will continue to carry out research in logic-based methods in the areas of automated deduction, rewriting, constraint/logic programming, hardware and software verification, and symbolic computation. For constraint-satisfaction problems and algorithms for combinatorial optimisation problems, the group will also continue to work on aspects such as heuristics, symmetries, and valued constraints, and carry out research in the field of proof and circuit complexity and its close relationship with automated theorem-proving and the satisfiability problem.

Specific tools that are being developed and maintained include automated deduction systems for first-order logic, efficient decision procedures for decidable logics of interest, environments for automated termination proofs, and environments for program verification. Moreover, the research group will continue to apply such tools to circuit verification, industrial planning/scheduling, the Semantic Web, and education, and to pursue their free distribution throughout the Internet.

New research lines of particular interest include the forthcoming Semantic World Wide Web and its associated description logics for semantic search criteria, consistency/integrity restrictions, etc. Another example is the crucial need for logic-based techniques for the verification of cryptographic protocols, in applications such as secrecy, electronic signatures, and electronic money (since testing is useless against malicious attackers). From a more theoretical point of view, we intend to open new lines of research in quantum computing, cryptography, data compression, and applications of game theory to computer science.

All the members of the group have international experience, some as researchers, lecturers and guest lecturers at international institutions. This facilitates close relationships with prestigious institutions, such as the Institute for Advanced Study in Princeton (USA), the DIMACS Research Centre at Rutgers University (USA), the University of Toronto (Canada), the University of California at San Diego (USA), the Max-Planck-Institut for Computer Science (Germany), the École Normale Superieure (France), the École Polytechnique (France), etc.

http://futur.upc.edu/LOGPROG

The group carries out research in basic computer science. In particular, it has internationally-recognised expertise in the (closely related) fields of logic in computer science, computational complexity and constraint-solving problems, and in the use of advanced programming techniques (e.g. constraint programming, automated deduction, etc.) for the development of practical software tools.

In what follows, we give a brief overview of these research lines. Logic has been called "the calculus of computer science", because its role in computer science is similar to that of mathematics in the physical sciences (see, for example, www.cs.rice.edu/~vardi/logic).

Similarly to the way in which architects and engineers analyse their designs mathematically, computer scientists use logic to analyse systems¿ properties (e.g. correctness, safety and security), during all the phases of their life cycles (e.g. specification, development, verification and maintenance). Also, for systems whose efficiency is critical, logic-based analysis can be very helpful, and in all kinds of systems, logic-based techniques help to reduce costs (see, for example, the section on software productivity tools at research.microsoft.com). Hence, it is not surprising that there is an increasing tendency to use logic-based formalisms in all kinds of hardware and software systems and their components, such as databases or programming languages, among others.

Computational complexity involves the study of the resources required during computation to solve a given problem. The most common resources are time (number of computation steps) and space (amount of memory). Other resources can also be considered, such as randomness (how randomness can increase efficiency) and parallelism (how the use of parallel processors can help). Today, the connections between logic and complexity are well established. For example, the field of proof complexity involves the study of the mathematical relationships between complexity classes (i.e. classes of problems that are solvable using the same amount of resources) and the length of proofs in certain logical systems. This field arose as an approach to the well-known problem of whether the P class of problems equals the NP class or not (see the million-dollar prizes at www.claymath.org): if one could show that, for every propositional proof system, there is a class of tautologies with no short proofs, then the answer is negative. The study of the limitations of proof systems has also led to the discovery of important new algorithms.

Constraint programming is the study of computational systems based on constraints. It has recently emerged as an area of research that engages researchers from a variety of fields. The idea is to solve problems by stating constraints (i.e. conditions, properties) that must be satisfied by the solution. Constraint programming consists of the generation of requirements (constraints) and the solution of these requirements by specialised constraint solvers. It has been successfully applied in numerous domains, including computer graphics (to express geometric coherence), natural language processing (to construct efficient parsers), database systems (to ensure and/or restore the consistency of the data), operations research (optimisation problems), molecular biology (DNA sequencing), business applications (option trading), electrical engineering (to locate faults), circuit design (to compute layouts), etc. Most, if not all, of these practical problems fall into the complexity class of NP-complete problems, for which proof complexity results give insight into classes of deterministic algorithms.

The research group will continue to carry out research in logic-based methods in the areas of automated deduction, rewriting, constraint/logic programming, hardware and software verification, and symbolic computation. For constraint-satisfaction problems and algorithms for combinatorial optimisation problems, the group will also continue to work on aspects such as heuristics, symmetries, and valued constraints, and carry out research in the field of proof and circuit complexity and its close relationship with automated theorem-proving and the satisfiability problem.

Specific tools that are being developed and maintained include automated deduction systems for first-order logic, efficient decision procedures for decidable logics of interest, environments for automated termination proofs, and environments for program verification. Moreover, the research group will continue to apply such tools to circuit verification, industrial planning/scheduling, the Semantic Web, and education, and to pursue their free distribution throughout the Internet.

New research lines of particular interest include the forthcoming Semantic World Wide Web and its associated description logics for semantic search criteria, consistency/integrity restrictions, etc. Another example is the crucial need for logic-based techniques for the verification of cryptographic protocols, in applications such as secrecy, electronic signatures, and electronic money (since testing is useless against malicious attackers). From a more theoretical point of view, we intend to open new lines of research in quantum computing, cryptography, data compression, and applications of game theory to computer science.

All the members of the group have international experience, some as researchers, lecturers and guest lecturers at international institutions. This facilitates close relationships with prestigious institutions, such as the Institute for Advanced Study in Princeton (USA), the DIMACS Research Centre at Rutgers University (USA), the University of Toronto (Canada), the University of California at San Diego (USA), the Max-Planck-Institut for Computer Science (Germany), the École Normale Superieure (France), the École Polytechnique (France), etc.

http://futur.upc.edu/LOGPROG

Enviaments recents

  • Look-ahead with mini-bucket heuristics for MPE 

    Dechter, Rina; Kask, Kalev; Lam, William; Larrosa Bondia, Francisco Javier (AAAI Press (Association for the Advancement of Artificial Intelligence), 2016)
    Comunicació de congrés
    Accés obert
    The paper investigates the potential of look-ahead in the con-text of AND/OR search in graphical models using the Mini-Bucket heuristic for combinatorial optimization tasks (e.g., MAP/MPE or weighted CSPs). We present and ...
  • Limited discrepancy AND/OR search and its application to optimization tasks in graphical models 

    Larrosa Bondia, Francisco Javier; Rollón Rico, Emma; Dechter, Rina (AAAI Press (Association for the Advancement of Artificial Intelligence), 2016)
    Text en actes de congrés
    Accés obert
    Many combinatorial problems are solved with a Depth-First search (DFS) guided by a heuristic and it is well-known that this method is very fragile with respect to heuristic mistakes. One standard way to make DFS more robust ...
  • Classes of term rewrite systems with polynomial confluence problems 

    Godoy Balil, Guillem; Nieuwenhuis, Robert Lukas Mario (2002-06-06)
    Report de recerca
    Accés obert
    The confluence property of ground (i.e., variable-free) term rewrite systems (GTRS) is well-known to be decidable. This was proved independently in [DTHL87,DHLT90] and in [Oya87] using tree automata techniques and ground ...
  • The Width-size method for general resolution is optimal 

    Bonet Carbonell, M. Luisa; Galesi, Nicola (1999-02)
    Report de recerca
    Accés obert
    The Width-Size Method for resolution was recently introduced by Ben-Sasson and Wigderson (BSW): Short Proofs are Narrow - Resolution Made Simple STOC 99). They found a trade-off between two complexity measures for ...
  • Succinct circuit representations and leaf languages are basically the same concept 

    Borchert, Bernd; Lozano Bojados, Antoni (1996-01)
    Report de recerca
    Accés obert
    This paper connects two topics of Complexity Theory: The topic of succinct circuit representations initiated by Galperin and Wigderson, and the topic of leaf languages. A Boolean circuit c describes in a natural way the ...
  • On the complexity of moving vertices in a graph 

    Lozano Bojados, Antoni; Raghavan, Vijay (1998-01)
    Report de recerca
    Accés obert
    We consider the problem of deciding whether a given graph G has an automorphism which moves at least k vertices (where k is a function of |V(G)|), a question originally posed by Lubiw (1981). Here we show that this ...
  • Linear lower bounds and simulations in Frege systems with substitutions 

    Bonet Carbonell, M. Luisa; Galesi, Nicola (1996-10)
    Report de recerca
    Accés obert
    Our work concerns Frege systems, substitution Frege systems (sF), renaming Frege systems, top/bottom-Frege systems and extended Frege systems (eF). Urquhart shows that tautologies associated to a binary strings ...
  • CBR and MBR techniques: review for an application in the emergencies domain 

    Merida-Campos, Carlos; Rollón Rico, Emma (2003-06-01)
    Report de recerca
    Accés obert
    The purpose of this document is to provide an in-depth analysis of current reasoning engine practice and the integration strategies of Case Based Reasoning and Model Based Reasoning that will be used in the design and ...
  • Lambda extensions of rewrite orderings 

    Jouannaud, Jean Pierre; Rubio Gimeno, Alberto (1995-10)
    Report de recerca
    Accés obert
    In this work we provide a new proof of the result by Gallier and Tannen that the combination of an arbitrary terminating first-order rewrite system with the simply typed lambda calculus is strongly normalizing. This proof ...
  • Extension orderings 

    Rubio Gimeno, Alberto (1995-10)
    Report de recerca
    Accés obert
    In this paper we study how to extend a collection of term orderings on disjoint signatures to a single one, called an extension ordering, which preserves (part of) their properties. Apart of its own interest, e.g. in ...

Mostra'n més