Last update: February 26, 2020
Logic and Programming
Methods and foundations of logic-based
tools for dealing with hard
plays a fundamental role in many computer science areas:
databases, programming languages, software engineering,
In fact, logic has been called "the calculus of computer
it plays a similar role in computer science to that of
calculus in the
physical sciences and traditional engineering disciplines (M.
group has done research in automated theorem proving in
first-order logic with equality (paramodulation)
and in higher-order logic (higher-order
unification). Nowadays the group is interested in
(SAT) and SAT modulo theories (SMT) and their applications to
problems in areas such as planning and scheduling:
timetabling, task sequencing in industrial processes, etc.
a system for solving constraint satisfaction problems
a compiler from the FlatZinc language to the standard
a system for solving the Resource-Constrained Project
Scheduling Problem using SMT.
a system for solving the Multi-mode Resource-Constrained
Project Scheduling Problem using SMT.
a system for solving the RCPSP with Time-Dependent
Capacities and Requests using SMT.
a system for editing Resource-Constrained Projects
the interactive lambda-calculus tracer.
A Planner based in the planning as satisfiability
approach, that relies on a SMT solver.
Publications: please check