Miquel Bofill Arasa
ASSOCIATE PROFESSOR
depT. informàtica, matemàtica aplicada I ESTADÍSTICA
C/ universitat de girona, 6
17003 girona - catalunya (SPAIN)
office p4 228
tel. (+34) 618 260 252
fax (+34) 972 418 792
FINGERPRINT: 7D1A 93C4 54C7 E6FC A450 F193 5842 AE36 8240 C149
Research areas of interest
My research interest is related to Logic in Computer Science:
Check the LAI research group web page for additional information (SOFTWARE, Etc.)
Journal Articles
Miquel Bofill, Jordi Coll, Jesús Giráldez-Cru, Josep Suy, Mateu Villaret
The Impact of Implied Constraints on MaxSAT B2B Instances
International Journal of Computational Intelligence Systems, Vol. 15, Article number: 63, August 2022. © Springer Nature
doi:10.1007/s44196-022-00121-5
Miquel Bofill, Jordi Coll, Gerard Martín, Josep Suy, Mateu Villaret
The Sample Analysis Machine Scheduling Problem: Definition and comparison of exact solving approaches
Computers & Operations Research, Vol. 142, June 2022, 105730. © Elsevier Ltd.
Miquel Bofill, Jordi Coll, Marc Garcia, Jesús Giráldez-Cru, Gilles Pesant, Josep Suy, Mateu Villaret
Constraint Solving Approaches to the Business-to-Business Meeting Scheduling Problem
Journal of Artificial Intelligence Research, Vol. 74, pages 263–301, May 2022. © AI Access Foundation, Inc.
Miquel Bofill, Jordi Coll, Peter Nightingale, Josep Suy, Felix Ulrich-Oltean, Mateu Villaret
SAT encodings for Pseudo-Boolean constraints together with at-most-one constraints
Artificial Intelligence, Vol. 302, January 2022, 103604. © Elsevier Ltd.
Author’s version: [Paper]
The final publication is available online at doi: 10.1016/j.artint.2021.103604
Miquel Bofill, Joan Espasa, Mateu Villaret
Relaxing non-interference requirements in parallel plans
Logic Journal of the IGPL, Vol. 29(1), pages 45–71, February 2021. © Oxford University Press
Special issue on Logics and Artificial Intelligence, Published: 01 August 2019
Miquel Bofill, Jordi Coll, Josep Suy, Mateu Villaret
SMT encodings for Resource-Constrained Project Scheduling Problems
Computers & Industrial Engineering 149: 106777, November 2020. © Elsevier Ltd.
doi: 10.1016/j.cie.2020.106777
Miquel Bofill, Jordi Coll, Josep Suy, Mateu Villaret
An MDD-based SAT encoding for pseudo-Boolean constraints with at-most-one relations
Artificial Intelligence Review, Vol. 53(7), pages 5157–5188, October 2020. © Springer Nature
Author’s version: [Paper]
The final publication is available online at doi: 10.1007/s10462-020-09817-6
Elvira Albert, Miquel Bofill, Cristina Borralleras, Enrique Martin-Martin, Albert Rubio
Resource Analysis driven by (Conditional) Termination Proofs
Theory and Practice of Logic Programming, Vol. 19(5-6), pages 722–739, September 2019. © Cambridge University Press
doi: 10.1017/S1471068419000152
Miquel Bofill, Felip Manyà, Amanda Vidal, Mateu Villaret
New complexity results for Łukasiewicz logic
Soft Computing, Vol. 23(7), pages 2187–2197, April 2019. © Springer Berlin Heidelberg
doi: 10.1007/s00500-018-3365-9
Miquel Bofill, Joan Espasa, Mateu Villaret
The RANTANPLAN planner: system description
The Knowledge Engineering Review, Vol. 31(5), pages 452–464, November 2016. © Cambridge University Press
Author’s version: [Paper] [BibTeX]
End-users may view and download the material for private research and study only.
The final publication is available online at doi: 10.1017/S0269888916000229
Carlos Ansótegui, Miquel Bofill, Felip Manyà, Mateu Villaret
Automated theorem provers for multiple-valued logics with satisfiability modulo theory solvers
Fuzzy Sets and Systems, Vol. 292, pages 32–48, June 2016. © Elsevier B.V.
doi: 10.1016/j.fss.2015.04.011
Marta Verdaguer, Josep Suy, Mateu Villaret, Narcís Clara, Miquel Bofill, Manel Poch
An exact approach for the prioritization process of industrial influents in wastewater systems
Clean Technologies and Environmental Policy, Volume 18, Issue 1, pages 339–346, January 2016. © Springer
First published online: June 18, 2015
doi: 10.1007/s10098-015-0992-z
Carlos Ansótegui, Miquel Bofill, Felip Manyà, Mateu Villaret
SAT and SMT Technology for Many-Valued Logics
Multiple-Valued Logic and Soft Computing, Vol. 24(1-4), pages 151–172, 2015. © Old City Publishing
Author’s version: [Paper] [BibTeX]
The final publication is available online at [URL]
Miquel Bofill, Ginés Moreno, Carlos Vázquez, Mateu Villaret
Automatic Proving of Fuzzy Formulae with Fuzzy Logic Programming and SMT
Electronic Communications of the EASST, Vol. 64: Programming and Computer Languages 2013, 1–19, 2014.
Miquel Bofill, Dídac Busquets, Víctor Muñoz, Mateu Villaret
Reformulation based MaxSAT robustness
Constraints, Vol. 18(2), pages 202–235, April 2013. © Springer
First published online: November 14, 2012
Author’s version: [Paper] [BibTeX]
The final publication is available online at doi: 10.1007/s10601-012-9130-2
Carlos Ansótegui, Miquel Bofill, Miquel Palahí, Josep Suy, Mateu Villaret
Solving weighted CSPs with meta-constraints by reformulation into satisfiability modulo theories
Constraints, Vol. 18(2), pages 236–268, April 2013. © Springer
First published online: November 13, 2012
Author’s version: [Paper] [BibTeX]
The final publication is available online at doi: 10.1007/s10601-012-9131-1
Miquel Bofill, Cristina Borralleras, Enric Rodríguez-Carbonell, Albert Rubio
The recursive path and polynomial ordering for first-order and higher-order terms
Journal of Logic and Computation, Vol. 23(1), pages 263–305, February 2013.
First published online: June 22, 2012
Author’s version: [Paper] [BibTeX]
The final publication is available online at doi: 10.1093/logcom/exs027
Miquel Bofill, Albert Rubio
Paramodulation with Non-Monotonic Orderings and Simplification
Journal of Automated Reasoning, Vol. 50:1, pages 51–98, January 2013. © Springer
First published online: December 15, 2011
Author’s version: [Paper] [BibTeX]
The final publication is available online at doi: 10.1007/s10817-011-9244-z
Miquel Bofill, Miquel Palahí, Josep Suy, Mateu Villaret
Solving constraint satisfaction problems with SAT modulo theories
Constraints, Vol. 17(3), pages 273–303, July 2012. © Springer
Author’s version: [Paper] [BibTeX]
The final publication is available online at doi: 10.1007/s10601-012-9123-1
Miquel Bofill, Albert Rubio
Paramodulation with Well-founded Orderings
Journal of Logic and Computation, Vol. 19(2), pages 263–302, April 2009.
First published online: November 21, 2008
Author’s version: [Paper] [BibTeX]
The final publication is available online at doi: 10.1093/logcom/exn073
Miquel Bofill, Guillem Godoy, Robert Nieuwenhuis, Albert Rubio
Paramodulation and Knuth-Bendix Completion with Nontotal and Nonmonotonic Orderings
Journal of Automated Reasoning, Vol. 30:1, pages 99–120, January 2003. © Kluwer
Author’s version: [Paper] [BibTeX]
The final publication is available online at doi: 10.1023/A:1022515030222
Conference and Workshop Papers
Miquel Bofill, Josu Oca
Towards Compact and Efficient SMT Formulations for AI Planning
In Actas de las XXIV Jornadas de Programación y Lenguajes (PROLE 2025). Sistedes (2025).
Córdoba, Spain, September 2025.
Miquel Bofill, Jordi Coll, Marc Garcia, Jesús Giráldez-Cru, Gilles Pesant, Josep Suy, Mateu Villaret
Constraint Solving Approaches to the Business-to-Business Meeting Scheduling Problem (Extended Abstract)
In Procs. 32nd International Joint Conference on Artificial Intelligence (IJCAI 2023)
pages 6851-6852, Macao, SAR, China, August 2023. ijcai.org
[Paper]
Miquel Bofill, Jordi Coll, Peter Nightingale, Jesús Giráldez-Cru, Josep Suy, Felix Ulrich-Oltean, Mateu Villaret
SAT Encodings for Pseudo-Boolean Constraints Together With At-Most-One Constraints (Extended Abstract)
In Procs. 32nd International Joint Conference on Artificial Intelligence (IJCAI 2023)
pages 6853-6857, Macao, SAR, China, August 2023. ijcai.org
[Paper]
Miquel Bofill, Cristina Borralleras, Joan Espasa, Mateu Villaret
On Grid Graph Reachability and Puzzle Games
In 22nd Workshop on Constraint Modelling and Reformulation (ModRef 2023)
Co-located with the 29th International Conference on Principles and Practice of Constraint Programming (CP 2023)
Toronto, Canada, August 2023.
[Paper]
Miquel Bofill, Cristina Borralleras, Joan Espasa, Gerard Martin, Gustavo Patow, Mateu Villaret
A Good Snowman is Hard to Plan
In 2023 Workshop on Knowledge Engineering for Planning and Scheduling (KEPS 2023)
Co-located with the 33rd International Conference on Automated Planning and Scheduling (ICAPS 2023)
Prague, Czech Republic, July 2023.
[Paper]
Miquel Bofill, Jesús Giráldez-Cru, Josep Suy, Mateu Villaret
A Study on Implied Constraints in a MaxSAT Approach to B2B Problems
In Procs. 22nd International Conference of the Catalan Association for Artificial Intelligence (CCIA 2019)
Artificial Intelligence Research and Development
Frontiers in Artificial Intelligence and Applications, Vol. 319, pages 183–192. © IOS Press
Author’s version: [Paper] [BibTeX]
The final publication is available at IOS Press through https://dx.doi.org/10.3233/FAIA190123
Carlos Ansótegui, Miquel Bofill, Jordi Coll, Nguyen Dang, Juan Luis Esteban, Ian Miguel, Peter Nightingale, András Z. Salamon, Josep Suy, Mateu Villaret
Automatic Detection of At-Most-One and Exactly-One Relations for Improved SAT Encodings of Pseudo-Boolean Constraints
In Procs. 25th International Conference on Principles and Practice of Constraint Programming (CP 2019)
LNCS 11802, pages 20–36, Stamford, CT, USA, September 30 – October 4, 2019. © Springer-Verlag
Author’s version: [Paper] [BibTeX]
The final authenticated publication is available at doi: 10.1007/978-3-030-30048-7_2
Miquel Bofill, Jordi Coll, Josep Suy, Mateu Villaret
SAT Encodings of Pseudo-Boolean Constraints with At-Most-One Relations
In Procs. 16th International Conference on Integration of Constraint Programming, Artificial Intelligence and Operations Research (CPAIOR 2019)
LNCS 11494, pages 112–128, Thessaloniki, Greece, June 2019. © Springer
Author’s version: [Paper] [BibTeX]
The final authenticated publication is available online at doi: 10.1007/978-3-030-19212-9_8
Miquel Bofill, Joan Espasa, Mateu Villaret
Relaxed Exists-Step Plans in Planning as SMT
In Procs. 26th International Joint Conference on Artificial Intelligence (IJCAI 2017)
pages 563–570, Melbourne, Australia, August 2017. ijcai.org
[Paper]
Miquel Bofill, Jordi Coll, Josep Suy, Mateu Villaret
Compact MDDs for Pseudo-Boolean Constraints with At-Most-One Relations in Resource-Constrained Scheduling Problems
In Procs. 26th International Joint Conference on Artificial Intelligence (IJCAI 2017)
pages 555–562, Melbourne, Australia, August 2017. ijcai.org
[Paper]
Miquel Bofill, Jordi Coll, Josep Suy, Mateu Villaret
An Efficient SMT Approach to Solve MRCPSP/max Instances with Tight Constraints on Resources
In Procs. 23rd International Conference on Principles and Practice of Constraint Programming (CP 2017)
LNCS 10416, pages 71–79, Melbourne, VIC, Australia, August 28 – September 1, 2017. © Springer-Verlag
Author’s version: [Paper] [BibTeX]
The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-319-66158-2_5
Miquel Bofill, Marcos Calderón, Francesc Castro, Esteve Del Acebo, Pablo Delgado, Marc Garcia, Marta García, Marc Roig, María O. Valentín, Mateu Villaret
The Spanish Kidney Exchange Model: Study of Computation-Based Alternatives to the Current Procedure
In Procs. 16th Conference on Artificial Intelligence in Medicine (AIME 2017)
LNCS 10259, pages 272–277, Vienna, Austria, June 2017. © Springer
Author’s version: [Paper] [BibTeX]
The final publication is available at doi: 10.1007/978-3-319-59758-4
Miquel Bofill, Jordi Coll, Josep Suy, Mateu Villaret
Solving the Multi-Mode Resource-Constrained Project Scheduling Problem with SMT
In Procs. 28th IEEE International Conference on Tools with Artificial Intelligence (ICTAI 2016)
pages 239–246, San José, CA, USA, November 2016.
© IEEE, 2016. doi: 10.1109/ICTAI.2016.0045
Miquel Bofill, Marc Garcia, Jesús Giráldez-Cru, Mateu Villaret
A Study on Implied Constraints in a MaxSAT Approach to B2B Problems
Workshop on Pragmatics of SAT (POS 2016)
Co-located with the 19th International Conference on Theory and Applications of Satisfiability Testing (SAT 2016)
Bordeaux, France, July 2016.
Miquel Bofill, Joan Espasa, Mateu Villaret
A Semantic Notion of Interference for Planning Modulo Theories
In Procs. 26th International Conference on Automated Planning and Scheduling (ICAPS 2016)
pages 56–64, London, UK, June 2016. © AAAI
Miquel Bofill, Felip Manyà, Amanda Vidal, Mateu Villaret
The Complexity of 3-Valued Łukasiewicz Rules
In Procs. 12th International Conference on Modeling Decisions for Artificial Intelligence (MDAI 2015)
LNCS 9321, pages 221–229, Skövde, Sweden, September 2015. © Springer
Author’s version: [Paper] [BibTeX]
The final publication is available at doi: 10.1007/978-3-319-23240-9_18
Jesús Manuel Almendros-Jiménez, Miquel Bofill, Alejandro Luna Tedesqui, Ginés Moreno, Carlos Vázquez, Mateu Villaret
Fuzzy XPath for the Automatic Search of Fuzzy Formulae Models
In Procs. 9th International Conference on Scalable Uncertainty Management (SUM 2015)
LNCS 9310, pages 385–398, Québec City, QC, Canada, September 2015. © Springer
Author’s version: [Paper] [BibTeX]
The final publication is available at doi: 10.1007/978-3-319-23540-0_26
Miquel Bofill, Felip Manyà, Amanda Vidal, Mateu Villaret
Finding Hard Instances of Satisfiability in Łukasiewicz Logics
In Procs. 45th IEEE International Symposium on Multiple-Valued Logic (ISMVL 2015)
pages 30-35, Waterloo, Ontario, Canada, May 2015.
© IEEE, 2015. doi: 10.1109/ISMVL.2015.10
Miquel Bofill, Marc Garcia, Josep Suy, Mateu Villaret
MaxSAT-Based Scheduling of B2B Meetings
In Procs. 12th International Conference on Integration of AI and OR Techniques in Constraint Programming (CPAIOR 2015)
LNCS 9075, pages 65–73, Barcelona, Spain, May 2015. © Springer
Author’s version: [Paper] [BibTeX]
The final publication is available at doi: 10.1007/978-3-319-18008-3_5
Miquel Bofill, Joan Espasa, Mateu Villaret
The RANTANPLAN planner: System description
In Workshop on Constraint Satisfaction Techniques for Planning and Scheduling Problems (COPLAS 2015)
Co-located with the 25th International Conference on Automated Planning and Scheduling (ICAPS 2015)
Jerusalem, Israel, June 2015.
[Paper]
Miquel Bofill, Jordi Coll, Josep Suy, Mateu Villaret
A System for Generation and Visualization of Resource-Constrained Projects
In Procs. 17th International Conference of the Catalan Association for Artificial Intelligence (CCIA 2014)
Artificial Intelligence Research and Development - Recent Advances and Applications
Frontiers in Artificial Intelligence and Applications, Vol. 269, pages 237–246. © IOS Press
Author’s version: [Paper] [BibTeX]
The final publication is available at doi: 10.3233/978-1-61499-452-7-237
Miquel Bofill, Miquel Palahí, Josep Suy, Mateu Villaret
Solving Intensional Weighted CSPs by Incremental Optimization with BDDs
In Procs. 20th International Conference on Principles and Practice of Constraint Programming (CP 2014)
LNCS 8656, pages 207–223, Lyon, France, September 2014. © Springer-Verlag
Author’s version: [Paper] [BibTeX]
The final publication is available at doi: 10.1007/978-3-319-10428-7_17
Miquel Bofill, Joan Espasa, Marc Garcia, Miquel Palahí, Josep Suy, Mateu Villaret
Scheduling B2B Meetings
In Procs. 20th International Conference on Principles and Practice of Constraint Programming (CP 2014)
LNCS 8656, pages 781–796, Lyon, France, September 2014. © Springer-Verlag
Author’s version: [Paper] [BibTeX]
The final publication is available at doi: 10.1007/978-3-319-10428-7_56
Miquel Bofill, Dídac Busquets, Mateu Villaret
Reformulation Based MaxSAT Robustness - (Extended Abstract)
In Procs. 20th International Conference on Principles and Practice of Constraint Programming (CP 2014)
LNCS 8656, pages 908–912, Lyon, France, September 2014. © Springer-Verlag
Author’s version: [Paper] [BibTeX]
The final publication is available at doi: 10.1007/978-3-319-10428-7_65
Miquel Bofill, Joan Espasa, Mateu Villaret
Efficient SMT Encodings for the Petrobras Domain
In Procs. 13th International Workshop on Constraint Modelling and Reformulation (ModRef 2014)
Co-located with the 20th International Conference on Principles and Practice of Constraint Programming (CP 2014)
pages 68–84, Lyon, France, September 2014.
Miquel Bofill, Miquel Palahí, Josep Suy, Mateu Villaret
Boosting Weighted CSP Resolution with Shared BDDs
In Procs. 12th International Workshop on Constraint Modelling and Reformulation (ModRef 2013)
Co-located with the 19th International Conference on Principles and Practice of Constraint Programming (CP 2013)
pages 57–73, Uppsala, Sweden, September 2013.
Miquel Bofill, Ginés Moreno, Carlos Vázquez, Mateu Villaret
Automatic Proving of Fuzzy Formulae with Fuzzy Logic Programming and SMT
In Procs. XIII Spanish Conference on Programming and Computer Languages (PROLE 2013)
pages 151–165, Madrid, Spain, September 2013.
Miquel Bofill, Joan Espasa, Miquel Palahí, Mateu Villaret
An extension to Simply for solving Weighted Constraint Satisfaction Problems with Pseudo-Boolean Constraints
In Procs. XII Spanish Conference on Programming and Computer Languages (PROLE 2012)
pages 141–155, Almería, Spain, September 2012.
Carlos Ansótegui, Miquel Bofill, Felip Manyà, Mateu Villaret
Building Automated Theorem Provers for Infinitely-Valued Logics with Satisfiability Modulo Theory Solvers
In Procs. 42nd IEEE International Symposium on Multiple-Valued Logic (ISMVL 2012)
pages 25–30, Victoria, BC, Canada, May 2012.
© IEEE, 2012. doi: 10.1109/ISMVL.2012.63
Miquel Bofill, Cristina Borralleras, Enric Rodríguez-Carbonell, Albert Rubio
The recursive path and polynomial ordering
In Procs. 12th International Workshop on Termination (WST 2012)
pages 29–33, Obergurgl, Austria, February 2012.
Carlos Ansótegui, Miquel Bofill, Miquel Palahí, Josep Suy, Mateu Villaret
A Proposal for Solving Weighted CSPs with SMT
In Procs. 10th International Workshop on Constraint Modelling and Reformulation (ModRef 2011)
Co-located with the 17th International Conference on Principles and Practice of Constraint Programming (CP 2011)
pages 5–19, Perugia, Italy, September 2011.
Carlos Ansótegui, Miquel Bofill, Miquel Palahí, Josep Suy, Mateu Villaret
W-MiniZinc: A Proposal for Modeling Weighted CSPs with MiniZinc
In Procs. 1st International Workshop on MiniZinc (MZN 2011)
Co-located with the 17th International Conference on Principles and Practice of Constraint Programming (CP 2011)
Perugia, Italy, September 2011.
Carlos Ansótegui, Miquel Bofill, Miquel Palahí, Josep Suy, Mateu Villaret
Satisfiability Modulo Theories: an Efficient Approach for the Resource-Constrained Project Scheduling Problem
In Procs. 9th Symposium on Abstraction, Reformulation and Approximation (SARA 2011)
pages 2–9, Cardona, Spain, July 2011.
Carlos Ansótegui, Miquel Bofill, Felip Manyà, Mateu Villaret
Extending Multiple-Valued Clausal Forms with Linear Integer Arithmetic
In Procs. 41st IEEE International Symposium on Multiple-Valued Logic (ISMVL 2011)
pages 230–235, Tuusula, Finland, May 2011.
© IEEE, 2011. doi: 10.1109/ISMVL.2011.53
Miquel Bofill, Dídac Busquets, Mateu Villaret
A Declarative Approach to Robust Weighted Max-SAT
In Procs. 12th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP 2010)
pages 67–76, Hagenberg, Austria, July 2010.
© ACM, 2010. This is the author’s version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in the Proceedings of the 12th international ACM SIGPLAN symposium on Principles and practice of declarative programming (PPDP 2010), Hagenberg, Austria, 26-28 July 2010.
Miquel Bofill, Josep Suy, Mateu Villaret
A System for Solving Constraint Satisfaction Problems with SMT
In Procs. 13th International Conference on Theory and Applications of Satisfiability Testing (SAT 2010)
LNCS 6175, pages 300–305, Edinburgh, UK, July 2010. © Springer-Verlag
doi: 10.1007/978-3-642-14186-7_25
Miquel Bofill, Dídac Busquets, Mateu Villaret
Auction Robustness through Satisfiability Modulo Theories
Proceedings of the Second Workshop on Agreement Technologies (WAT 2009)
Volume 635 of CEUR Workshop Proceedings, pages 33-44
Sevilla, Spain, November 2009
Miquel Bofill, Miquel Palahí, Josep Suy, Mateu Villaret
SIMPLY: a Compiler from a CSP Modeling Language to the SMT-LIB Format
In Procs. 8th International Workshop on Constraint Modelling and Reformulation (ModRef 2009)
Co-located with the 15th International Conference on Principles and Practice of Constraint Programming (CP 2009)
pages 30–44, Lisbon, Portugal, September 2009.
[Paper] [Paper (long version)] [BibTeX]
Miquel Bofill, Miquel Palahí, Mateu Villaret
A System for CSP Solving through Satisfiability Modulo Theories
In Procs. IX Jornadas sobre Programación y Lenguajes (PROLE 2009)
pages 303–312, Donostia, Spain, September 2009.
Miquel Bofill, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio
A Write-Based Solver for SAT Modulo the Theory of Arrays
In Procs. 8th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2008)
pages 1–8, Portland, USA, November 2008.
© IEEE, 2008. This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. In most cases, these works may not be reposted without the explicit permission of the copyright holder.
doi: 10.1109/FMCAD.2008.ECP.18
Miquel Bofill, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio
The Barcelogic SMT Solver
In Procs. 20th International Conference on Computer Aided Verification (CAV 2008)
LNCS 5123, pages 294–298, Princeton, USA, July 2008. © Springer-Verlag
doi: 10.1007/978-3-540-70545-1_27
Miquel Bofill, Albert Rubio
Redundancy Notions for Paramodulation with Non-Monotonic Orderings
In Procs. 2nd International Joint Conference on Automated Reasoning (IJCAR 2004)
LNAI 3097, pages 107–121, Cork, Ireland, July 2004. © Springer-Verlag
doi: 10.1007/978-3-540-25984-8_6
[Paper] [Paper (long version)] [BibTeX]
Miquel Bofill, Albert Rubio
Well-foundedness is Sufficient for Completeness of Ordered Paramodulation
In Procs. 18th International Conference on Automated Deduction (CADE 2002)
LNAI 2392, pages 456–470, Copenhagen, Denmark, July 2002. © Springer-Verlag
[Paper] [Paper (long version)] [BibTeX]
Miquel Bofill, Guillem Godoy
On the Completeness of Arbitrary Selection Strategies for Paramodulation
In Procs. 28th International Colloquium on Automata, Languages and Programming (ICALP 2001)
LNCS 2076, pages 951–962, Crete, Greece, July 2001. © Springer-Verlag
[Paper] [Paper (long version)] [BibTeX]
Miquel Bofill, Guillem Godoy, Robert Nieuwenhuis, Albert Rubio
Modular Redundancy for Theorem Proving
In Procs. 3rd International Workshop on Frontiers of Combining Systems (FroCoS 2000)
LNAI 1794, pages 186–199, Nancy, France, April 2000. © Springer-Verlag
Miquel Bofill, Guillem Godoy, Robert Nieuwenhuis, Albert Rubio
Paramodulation with Non-Monotonic Orderings
In Procs. 14th Annual IEEE Symposium on Logic in Computer Science (LICS 1999)
pages 225–234, Trento, Italy, July 1999. © IEEE Comp. Sc. Press
PhD thesis
Equational Reasoning with Non-Monotonic Orderings
Technical University of Catalonia, July 2004.
Supervisor: Albert Rubio
[Thesis]
ADVISEES
Joan Espasa, PhD (grad. 2018, co-advised, later at University of St Andrews)
Miquel Palahí, PhD (grad. 2015, co-advised, later at Unipart Group)
Josep Suy, PhD (grad. 2012, co-advised)
