Logic and Artificial Intelligence

research group at

Department of Computer Science, Applied Mathematics and Statistics, UdG

Main research line:

Methods and foundations of logic-based tools for dealing with hard computational problems

---

Logic plays a fundamental role in many Computer Science areas: programming languages, databases, software engineering, software and hardware verification, etc. The use of mathematical logic as a formalism for Artificial Intelligence was recognized by John McCarthy as early as in 1959, and since then it has played an important role in some central areas of AI research. Logic has also 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's research is related with automated reasoning (automated theorem proving in first-order logic with equality, higher-order unification, and multiple-valued logics) as well as to propositional satisfiability (SAT) and satisfiability modulo theories (SMT) and their applications to solve combinatorial problems in AI areas such as planning and scheduling.

Faculty

• Miquel Bofill

• Francesc Castro

• Josep Suy

• Mateu Villaret

PhD Students

• Jordi Coll, PhD (grad. 2019)

• Joan Espasa, PhD (grad. 2018, later at Launchmetrics)
  

• Miquel Palahí, PhD (grad. 2015, later at Unipart Group)

Graduate Students

• Marc Garcia

• Gerard Martín

Software

• 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.

• mrcpspmax2smt: a system for solving the Multi-mode Resource-Constrained Project Scheduling Problem 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.

• B2B benchmarks: dzn files used in the experiments of the paper "Constraint Solving Approaches to the Business-to-Business Meeting Scheduling Problem" (to appear)

Publications: see personal pages

 

---