Robert Nieuwenhuis       

Catedrático de Universidad
Departamento de Lenguajes y Sistemas Informáticos (LSI)
Universidad Politécnica de Cataluña (UPC) in Barcelona, Spain.

(Full Professor, Software Department, Technical University of Catalonia)

Quick links:

Main publications
Research events I'm involved in
The Programming Group
Slides of a talk (2002) on our work on Logic in Computer Science
Research Interests
Teaching Activities
Other research information
Contact Information
My kids (Oct. 2004)
News:
Check CADE-20 (2005), the 20th International Conference on Automated Deduction, which I'm PC Chair of.
The competion schedule we made for the new 2004-2005 Spanish Professional Basketball League (ACB) (like we did for last year's one, ACB 2003-2004) is now official.

Research Interests

• Automated Deduction   (see also Automated Theorem Proving )
  
  • Completeness results for inference systems
    
  • Inductive proofs; proofs in particular (classes of) models
    
  • Heuristics for automated theorem proving
    
• Rewriting
  
  • Decision and complexity results
    
  • Applications
    
  • Termination
    
• The implementation of logics
  
  • Data structures and algorithms for term representation
    
  • Data structures and algorithms for term indexing
    
  • Construction of theorem proving systems: heuristics, re-usability, ...
    
• Symbolic Constraint Solving
  
  • Ordering constraints
    
  • Equality constraints, E-unification
    
• Logic-based complexity and decidability analysis
  
• Constraint and/or logic programming
  • In particular, (since 1992) round-robin sport tournaments scheduling.
    

Other research information

Main publications

Research events I'm involved in

Access to the COMPIT website , our methodology for COMParing Indexing Techniques for automated deduction.

The Saturate system is an experimental theorem proving environment for first-order logic, primarily based on saturation, which, together with Harald Ganzinger and Pilar Nivela, we developed at the Max-Planck-Institut for Computer Science. Saturate uses techniques of ordered chaining for arbitrary transitive relations, including orderings, equivalence relations and congruences, and integrates CNF transformation lazily into saturation.

Construction of Computational Logics II (CCL-II) is a EU Esprit Working Group of which I am the UPC scientific coordinator.

(Former) PhD. Students:

• Albert Rubio (defended 1994)
• Jose Miguel Rivero (defended 2000)
• Guillem Godoy (defended 2001)
• Miguel Angel Vallejo (ongoing)
• Albert Oliveras (ongoing)
• Enric Rodriguez (ongoing)

Computer science bibliography databases:
DBLP Computer Science Bibliography Trier
Citeseer ResearchIndex.
Computer Science Bibliographies Karlsruhe.

Click here to see a beautiful 10-store "human tower" (in Catalan: "castell"; one of the many interesting aspects of Catalan culture)