Reseach



EVENTS


UNIF'15 - (Co-chair)
CPAIOR'15 - (Local Organizer)
CCIA'15 - (PC member)
CAEPIA'15 - (PC member)
PROLE'15 - (PC member)
RTA/TLCA'14 - (PC member)
UNIF'14 - (PC member)
CCIA'14 - (PC member)
SARA'13 - (PC member)
CCIA'13 - (PC member)
TPF'13 - Quinto taller de programación funcional (PC member)
MDAI'12 - (General co-chair)
CCIA'12 - (PC member)
TPF'12 - Cuarto taller de programación funcional (PC chair)
TPF'11 - Tercer taller de programación funcional (PC member)
TPF'10 - Segundo taller de programación funcional (PC member)
TPF'09 - Primer taller de programación funcional (PCmember)
UNIF'06 - (PC member)
UNIF'03 - (PC member)



Ph.D. Students


Joan Espasa (ongoing)
Miquel Palahí (ongoing)
Josep Suy (defended 2012)


Journals


Authors: Ansótegui C.; Bofill M.; Manyà F.; Villaret, M.Title: SAT and SMT Technology for Many-Valued Logics Journal: Journal Of Multiple-Valued Logic And Soft Computing (to appear)Volume: --- Number: --- Pages, Initial: --- final: --- Year: ---

Authors: Kutsia T.; Levy J.; Villaret M.Title: Anti-unification for Unranked Terms and Hedges Journal: Journal of Automated Reasoning Volume: 52    Number: 2    Pages, Initial: 155 final: 190 Year: 2014

Authors: Bofill, M.; Busquets, D.; Muñoz, V.; Villaret, M.Title: Reformulation based MaxSAT robustness Journal: Constraints Volume: 18 Number: 2 Pages, Initial: 202 final: 235 Year: 2013

Authors: Ansótegui, C.; Bofill, M.; Palahí, M., Suy, J.; Villaret, M.Title: Solving weighted CSPs with meta-constraints by reformulation into satisfiability modulo theories Journal: Constraints Volume: 18 Number: 2 Pages, Initial: 236 final: 268 Year: 2013

Authors : Bofill, M.; Palahí, M., Suy, J.; Villaret, M.Title: Solving Constraint Satisfaction Problems with SAT Modulo Theories Journal: Constraints Volume: 17 Number: 3 Pages, Initial: 273 final: 303 Year: 2012

Authors: Levy J.; Villaret M.Title: Nominal Unification from a Higher-Order Perspective Journal: Acm Transactions On Computational Logic Volume: 13 Number: 2 Pages, Initial: 1 final: 31 Year: 2012

Authors : Levy J.; Schmidt-Schauss M.; Villaret M.Title: On the Complexity of Bounded and Stratified Second-order Unification Journal: Logic Journal Of The Igpl Volume: 19 Number: 6 Pages, Initial: 763 final: 789 Year: 2011

Authors: Kutsia T.; Levy J.; Villaret M.Title: On the relation between Context and Sequence Unification Journal: Journal of Symbolic Computation Volume: 45    Number: 1    Pages, Initial: 74 final: 95 Year: 2010

Authors: Lopez, B. ; Muñoz, V.; Murillo, J.; Barber, F.; Salido, M.A.; Abril, M.; Cervantes, M.; Caro, L.F.; Villaret, M.Title: Experimental analysis of optimization techniques on the road passenger transportation problem Journal: Engineering Applications of Artificial Intelligence Volume: 22 Number: 3 Pages, Initial: 374 final: 388 Year: 2009

Authors: Levy J.; Villaret M.Title: Simplifying the signature in second-order unification Journal: Applicable Algebra in Engineering Communication and Computing Volume: 20    Number: 5-6 Pages, Initial: 427 final: 445 Year: 2009

Authors: Levy, J.; Schmidt-Schauss, M.; Villaret, M. Title: The complexity of monadic second-order unification Journal: Siam Journal on Computing Volume: 38 Number: 3 Pages, Initial: 1113 final: 1140 Year: 2008


Conferences and Workshops


Alex Baumgartner, Temur Kutsia, Jordi Levy and Mateu Villaret (2013). A Variant of Higher-Order Anti-Unification. Leibniz International Proceedings in Informatics of the  24th International Conference on Rewriting Techniques and Applications (RTA). LIPICS 21, pages 113--127.

Miquel Bofill, Miquel Palahí, Josep Suy, and Mateu Villaret (2013).
Boosting Weighted CSP Resolution with Shared BDDs.In Proceedings of the 12th International Workshop on Constraint Modelling and Reformulation (ModRef 2013), pages 57–73.

Miquel Bofill, Ginés Moreno, Carlos Vázquez, and Mateu Villaret  (2013). Automatic Proving of Fuzzy Formulae with Fuzzy Logic Programming and SMT.
In Proceedings of the XIII Spanish Conference on Programming and Computer Languages (PROLE 2013), pages 151–165.

Carlos Ansótegui, Miquel Bofill, Felip Manyà and Mateu Villaret (2012). Building Automated Theorem Provers for Infinitely-Valued Logics with Satisfiability Modulo Theory Solvers. In Proceedings of the 42nd IEEE International Symposium on Multi-Valued Logic (ISMVL'12), pages 25--30.

Miquel Bofill, Joan Espasa, Miquel Palahí and Mateu Villaret (2012). An Extension to Simply for Solving Weighted Constraint Satisfaction Problems with Pseudo-Boolean Constraints. In Proceedings of XII Jornadas sobre Programación y Lenguajes (Prole'12).


Temur Kutsia, Jordi Levy and Mateu Villaret (2011). Anti-Unification for Unranked Terms and Hedges. In Leibniz International Proceedings in Informatics of the 22nd International Conference on Rewriting Techniques and Applications (RTA11). LIPICS 10, pages 219--234.

Carlos Ansótegui, Miquel Bofill, Miquel Palahí, Josep Suy and Mateu Villaret (2011). Satisfiability Modulo Theories: an Efficient Approach for the Resource-Constrained Project Scheduling Problem. In Proceedings of the9th Symposium on Abstraction, Reformulation and Aproximation (SARA'11), pages 2--9.

Carlos Ansótegui, Miquel Bofill, Felip Manyà and Mateu Villaret (2011). Extending Multi-Valued Clausal Forms with Linear Integer Arithmetic. In Proceedings of the 41st IEEE International Symposium on Multi-Valued Logic (ISMVL'11). Pages 230--235.

Carlos Ansótegui, Miquel Bofill, Miquel Palahí, Josep Suy and Mateu Villaret (2011). A Proposal for Solving Weighted CSPs with SMT. In Proceedings of the 10th International Workshop on Constraint Modelling and Reformulation (ModRef 2011), pages 5--19.

Carlos Ansótegui, Miquel Bofill, Miquel Palahí, Josep Suy and Mateu Villaret (2011). W-MiniZinc: A Proposal for Modeling Weighted CSPs with MiniZinc. In Proceedings of the 1st International Workshop on MiniZinc (MZN 2011).


Miquel Bofill, Josep Suy and Mateu Villaret (2010). A system for solving constraint satisfaction problems with SMT. In Proceedings of the 13th International Conference of Theory and Applications of Satisfiability Testing (SAT 2010), Lecture Notes in Computer Science, 6175 pages 300--305.

Miquel Bofill, Dídac Busquets and Mateu Villaret (2010). A declarative approach to robust weighted max-SAT. In Proceedings of the 12th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP'10), pages 67--76.

Jordi Levy and Mateu Villaret (2010). An Efficient Nominal Unification Algorithm. In Leibniz International Proceedings in Informatics of the 21st International Conference on Rewriting Techniques and Applications (RTA'10). LIPICS 6, pages 209--226.


Miquel Bofill, Miquel Palahí, Josep Suy and Mateu Villaret (2009). Simply: a Compiler from a CSP Modeling Language to the SMT-LIB. In Proceedings of the 8th International Workshop on Constraint Modelling and Reformulation (ModRef'09), pages 30--44.

Miquel Bofill, Miquel Palahí and Mateu Villaret (2009). A System for CSP solving through Satisfiability Modulo Theories. In Proceedings of the  IX Jornadas de Programación y Lenguajes (PROLE'09), pages 303--312.

David Ruíz and Mateu Villaret (2009). TILC: The Interactive Lambda-Calculus Tracer. Electronic Notes in Theoretical Computer Science, vol. 248, pages 173--183. (Extended version of PROLE'08)

Miquel Bofill, Dídac Busquets and Mateu Villaret (2009). Auction robustness through satisfiability modulo theories. In Workshop on Agreement Technologies (WAT 2009).


Jordi Levy and Mateu Villaret (2008). Nominal Unification from a Higher-order Perspective.In Proceedings of the 19th Int.Conf. on Rewriting Techniques and Applications, RTA'08. Hagenberg, Austria, July 15-17, 2008. Volume 5117 of Lecture Notes in Computer Science, pages 246-260, Springer-Verlag. (Slides).

David Ruíz and Mateu Villaret (2008). TILC: The Interactive Lambda-Calculus Tracer. In Proceedings of the  VIII Jornadas de Programación y Lenguajes (PROLE'08).
 

Temur Kutsia, Jordi Levy and Mateu Villaret (2007). Sequence Unification Through Currying.
In Proceedings of the 18th Int.Conf. on Rewriting Techniques and Applications, RTA'07. Paris, France, June 26-28, 2007.
Volume 4533 of Lecture Notes in Computer Science, pages 288-302, Springer-Verlag. (Slides).
 

Jordi Levy, Manfred Schmidt-Schauss and Mateu Villaret (2006). Bounded Second-Order Unification Is NP-Complete.
In Proceedings of the 17th Int.Conf. on Rewriting Techniques and Applications, RTA'06. Seattle, WA, USA, August 12-14, 2006.
Volume 4098 of Lecture Notes in Computer Science, pages 400-414, Springer-Verlag.
 
Jordi Levy, Manfred Schmidt-Schauss and Mateu Villaret (2006). Stratified Context Unification is NP-complete.
In Proceedings of the 3rd International Joint Conference on Automated Reasoning, IJCAR'06. Seattle, WA, USA, August 17 - 20, 2006. Volume 4130 of Lecture Notes in Artificial Intelligence, pages 82-96, Springer-Verlag.
 

Jordi Levy, Joachim Niehren and Mateu Villaret (2005). Well-Nested Context Unification.
In Proceedings of the 20th Int. Conference on Automated Deduction, CADE-20. Tallinn, Estonia, July 22-27, 2005.
Volume 3632 of Lecture Notes in Artificial Intelligence, pages 149-163, Springer-Verlag.
 
Joachim Niehren and Mateu Villaret (2005). Describing Lambda-Terms in Context Unification.
In Proceedings of the 5th. Int Conf. on Logical Aspects of Computational Linguistics, LACL’05. Bordeaux, France, April 2005.
Volume 3492 of Lecture Notes in Artificial Intelligence, pages 221-237, Springer-Verlag.
 

Jordi Levy, Manfred Schmidt-Schauss and Mateu Villaret (2004). Monadic Second-Order Unification is NP-Complete.
In Proceedings of the 15th Int. Conf. on Rewriting Techniques and Applications, RTA'04. Aachen, Germany, June 3-5, 2004.
Volume 3091 of Lecture Notes in Computer Science, pages 55-69, Springer-Verlag. (Best Paper Award).
 

Joachim Niehren and Mateu Villaret (2003). Describing Lambda-Terms in Context Unification.
In 4th Workshop on Inference in Computational Semantics ICOS-4. Nancy, France, September 2003.
 

Joachim Niehren and Mateu Villaret (2002). Parallelism and Tree Regular Constraints.
In Proceedings of the 9th Int.l Conf. on Logic for Programming Artificial Intelligence and Reasoning, LPAR'02. Tiblissi, Georgia, October 2002.
Volume 2514 of Lecture Notes in Artficial Intelligence, pages 311-326, Springer-Verlag
 
Mateu Villaret (2002). Processing Tree Regular Constraints in Context Unification.
In Proceedings of the 7th Student Session of the European Summer School in Logic, Language, and Information, ESSLLI'02. Trento, Italy, August 2002.
Pages 271-283.
 
Jordi Levy and Mateu Villaret (2002). Currying Second-Order Unification Problems.
In Proceedings of the 13th Int. Conf. on Rewriting Techniques and Applications, RTA'02. Copenhagen, Denmark, July 22-24, 2002.
Volume 2378 of Lecture Notes in Computer Science, pages 326-339, Springer-Verlag.
 
Joachim Niehren and Mateu Villaret (2002). Parallelism and Tree Regular Constraints. In Proceedings of the 16th International Workshop on Unification (UNIF'02).


Jordi Levy and Mateu Villaret (2001). Context Unification and Traversal Equations.
In Proceedings of the 12th Int. Conf. on Rewriting Techniques and Applications, RTA'01. Utrecht, The Netherlands, May 22-24, 2001.
Volume 2051 of Lecture Notes in Computer Science, pages 169-184, Springer-Verlag.
 

Jordi Levy and Mateu Villaret (2000). Linear Second-Order Unification and Context Unification with Tree-Regular Constraints.
In Proceedings of the 11th Int. Conf. on Rewriting Techniques and Applications, RTA'00. Norwich, UK, July 10-12, 2000.
Volume 1833 of Lecture Notes in Computer Science, pages 156-171, Springer-Verlag.
 

Jordi Levy and Mateu Villaret (1998). Complexity Study of Some Classes of Context and Second-order Unification Problems.
In Proceedings of the 12th International Workshop on Unification (UNIF'98).


BOOKS


Editors: Vicenç Torra, Yasuo Narukawa, Beatriz López and Mateu Villaret. Proceedings of the 9th International Conference on Modeling Decisions for Artificial Intelligence (MDAI'12). Lecture Notes in Computer Science 7647, (2012). ISBN 978-3-642-34619-4.


Mateu Villaret (2004). On Some Variants of Second-Order Unification.
Ph. D. Thesis.
June 2004, Supervised by Jordi Levy
Publication: Monografies de l'IIIA, vol. 22, (2005). ISBN-84-00-08319-9.
Thesis Comitee: Albert Rubio, Guillem Godoy, Philippe de Groote, Joachim Niehren and Manfred Schmidt-Schauss.


Editors: Jordi Levy, Michael Kohlhase, Joachim Niehren and Mateu Villaret. Proceedings of the 17th International Workshop on Unification (UNIF'03), 2003. ISBN: 84-96221-00-8.




Top
 
Girona, 12/05/2014