Last update: May 21, 2019
Logic and Programming
research group at
Main research line:
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, verification…
In fact, logic has been called "the calculus of computer science", as
it plays a similar role in computer science to that of calculus in the
physical sciences and traditional engineering disciplines (M. Vardi,
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 propositional satisfiability
(SAT) and SAT modulo theories (SMT) and their applications to solve combinatorial
problems in areas such as planning and scheduling: timetabling, task sequencing in industrial processes, etc.
Joan Espasa, PhD 2018, later at Launchmetrics
Miquel Palahí, PhD 2015, later at Unipart Group
WSimply: a system for solving constraint satisfaction problems using SMT.
fzn2smt: a compiler from the FlatZinc language to the standard SMT-LIB language.
rcpsp2smt: a system for solving the Resource-Constrained Project Scheduling Problem using SMT.
mrcpsp2smt: a system for solving the Multi-mode Resource-Constrained Project Scheduling Problem using SMT.
rcpspt2smt: a system for solving the RCPSP with Time-Dependent Capacities and Requests using SMT.
viewproject: a system for editing Resource-Constrained Projects
TILC: the interactive lambda-calculus tracer.
RanTanPlan: A Planner based in the planning as satisfiability approach, that relies on a SMT solver.
Publications: please check personal pages