Logic and Programming
research group at
Main research line:
Methods and foundations of logicbased tools for dealing with hard
computational problems
Logic
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,
2007)
The
group has done research in automated theorem proving in firstorder logic with equality (paramodulation) and in higherorder logic (higherorder
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.
Members:


Jordi Coll, PhD Student

Joan Espasa, PhD Student

Marc Garcia

Dr. Josep Suy

Past members:
Software:

WSimply: a system for solving constraint satisfaction problems using SMT.

fzn2smt: a compiler from the FlatZinc language to the standard SMTLIB language.

rcpsp2smt: a system for solving the ResourceConstrained Project Scheduling Problem using SMT.

mrcpsp2smt: a system for solving the Multimode ResourceConstrained Project Scheduling Problem using SMT.

mrcpspmax2smt: a system for solving the Multimode ResourceConstrained Project Scheduling Problem with Minimum and Maximum Time Lags using SMT.

rcpspt2smt: a system for solving the RCPSP with TimeDependent Capacities and Requests using SMT.

viewproject: a system for editing ResourceConstrained Projects

TILC: the interactive lambdacalculus tracer.

RanTanPlan: A Planner based in the planning as satisfiability approach, that relies on a SMT solver.
Publications: please check personal pages
Last update: May 26, 2015