|
|
|
|
[1]
|
Miquel Bofill, Cristina Borralleras, Enric Rodríguez-Carbonell, and Albert
Rubio.
The recursive path and polynomial ordering for first-order and
higher-order terms.
J. Log. Comput., 23(1):263-305, 2013.
[ bib ]
|
|
[2]
|
Miquel Bofill and Albert Rubio.
Paramodulation with non-monotonic orderings and simplification.
J. Autom. Reasoning, 50(1):51-98, 2013.
[ bib ]
|
|
[3]
|
Clark Barrett, Morgan Deters, Leonardo Mendonça de Moura, Albert Oliveras,
and Aaron Stump.
6 years of smt-comp.
J. Autom. Reasoning, 50(3):243-277, 2013.
[ bib ]
|
|
[4]
|
Carlos Ansótegui, Maria Luisa Bonet, Jordi Levy, and Felip Manyà.
Resolution procedures for multiple-valued optimization.
Inf. Sci., 227:43-59, 2013.
[ bib ]
|
|
[5]
|
Carlos Ansótegui, Maria Luisa Bonet, and Jordi Levy.
Sat-based maxsat algorithms.
Artif. Intell., 196:77-105, 2013.
[ bib ]
|
|
[6]
|
Daniel Larraz, Enric Rodríguez-Carbonell, and Albert Rubio.
Smt-based array invariant generation.
In Giacobazzi et al. [7], pages 169-188.
[ bib ]
|
|
[7]
|
Roberto Giacobazzi, Josh Berdine, and Isabella Mastroeni, editors.
Verification, Model Checking, and Abstract Interpretation, 14th
International Conference, VMCAI 2013, Rome, Italy, January 20-22, 2013.
Proceedings, volume 7737 of Lecture Notes in Computer Science.
Springer, 2013.
[ bib ]
|
|
[8]
|
Javier Larrosa and Emma Rollon.
Risk-neutral bounded max-sum for distributed constraint optimization.
In Shin and Maldonado [9], pages 92-97.
[ bib ]
|
|
[9]
|
Sung Y. Shin and José Carlos Maldonado, editors.
Proceedings of the 28th Annual ACM Symposium on Applied
Computing, SAC '13, Coimbra, Portugal, March 18-22, 2013. ACM, 2013.
[ bib ]
|
|
[10]
|
Emma Rollon, Javier Larrosa, and Rina Dechter.
Semiring-based mini-bucket partitioning schemes.
In Rossi [12].
[ bib ]
|
|
[11]
|
Maria Luisa Bonet and Sam Buss.
An improved separation of regular resolution from pool resolution and
clause learning (extended abstract).
In Rossi [12].
[ bib ]
|
|
[12]
|
Francesca Rossi, editor.
IJCAI 2013, Proceedings of the 23rd International Joint
Conference on Artificial Intelligence, Beijing, China, August 3-9, 2013.
IJCAI/AAAI, 2013.
[ bib ]
|
|
[13]
|
Carlos Ansótegui, Maria Luisa Bonet, Joel Gabàs, and Jordi Levy.
Improving wpm2 for (weighted) partial maxsat.
In Schulte [15], pages 117-132.
[ bib ]
|
|
[14]
|
Ignasi Abío, Robert Nieuwenhuis, Albert Oliveras, Enric
Rodríguez-Carbonell, and Peter J. Stuckey.
To encode or to propagate? the best choice for each constraint in
sat.
In Schulte [15], pages 97-106.
[ bib ]
|
|
[15]
|
Christian Schulte, editor.
Principles and Practice of Constraint Programming - 19th
International Conference, CP 2013, Uppsala, Sweden, September 16-20, 2013.
Proceedings, volume 8124 of Lecture Notes in Computer Science.
Springer, 2013.
[ bib ]
|
|
[16]
|
Ignasi Abío, Robert Nieuwenhuis, Albert Oliveras, and Enric
Rodríguez-Carbonell.
A parametric approach for smaller and better encodings of cardinality
constraints.
In Schulte [15], pages 80-96.
[ bib ]
|
|
[17]
|
Deepak Kapur, Robert Nieuwenhuis, Andrei Voronkov, Christoph Weidenbach, and
Reinhard Wilhelm.
Harald ganzinger's legacy: Contributions to logics and programming.
In Voronkov and Weidenbach [18],
pages 1-18.
[ bib ]
|
|
[18]
|
Andrei Voronkov and Christoph Weidenbach, editors.
Programming Logics - Essays in Memory of Harald Ganzinger,
volume 7797 of Lecture Notes in Computer Science. Springer, 2013.
[ bib ]
|
|
[19]
|
Maria Luisa Bonet, Simone Linz, and Katherine St. John.
The complexity of finding multiple solutions to betweenness and
quartet compatibility.
IEEE/ACM Trans. Comput. Biology Bioinform., 9(1):273-285,
2012.
[ bib ]
|
|
[20]
|
Cristina Borralleras, Salvador Lucas, Albert Oliveras, Enric
Rodríguez-Carbonell, and Albert Rubio.
Sat modulo linear arithmetic for solving polynomial constraints.
J. Autom. Reasoning, 48(1):107-131, 2012.
[ bib ]
|
|
[21]
|
Ignasi Abío, Robert Nieuwenhuis, Albert Oliveras, Enric
Rodríguez-Carbonell, and Valentin Mayer-Eichberger.
A new look at bdds for pseudo-boolean constraints.
J. Artif. Intell. Res. (JAIR), 45:443-480, 2012.
[ bib ]
|
|
[22]
|
Stefano Bistarelli, Fabio Gadducci, Javier Larrosa, Emma Rollon, and Francesco
Santini.
Local arc consistency for non-invertible semirings, with an
application to multi-objective optimization.
Expert Syst. Appl., 39(2):1708-1717, 2012.
[ bib ]
|
|
[23]
|
Maria Luisa Bonet and Samuel R. Buss.
An improved separation of regular resolution from pool resolution and
clause learning.
In Cimatti and Sebastiani [24], pages 44-57.
[ bib ]
|
|
[24]
|
Alessandro Cimatti and Roberto Sebastiani, editors.
Theory and Applications of Satisfiability Testing - SAT 2012 -
15th International Conference, Trento, Italy, June 17-20, 2012. Proceedings,
volume 7317 of Lecture Notes in Computer Science. Springer, 2012.
[ bib ]
|
|
[25]
|
Maribel Fernández and Albert Rubio.
Nominal completion for rewrite systems with binders.
In Czumaj et al. [26], pages 201-213.
[ bib ]
|
|
[26]
|
Artur Czumaj, Kurt Mehlhorn, Andrew M. Pitts, and Roger Wattenhofer, editors.
Automata, Languages, and Programming - 39th International
Colloquium, ICALP 2012, Warwick, UK, July 9-13, 2012, Proceedings, Part II,
volume 7392 of Lecture Notes in Computer Science. Springer, 2012.
[ bib ]
|
|
[27]
|
Emma Rollon and Javier Larrosa.
Improved bounded max-sum for distributed constraint optimization.
In Milano [29], pages 624-632.
[ bib ]
|
|
[28]
|
Carlos Ansótegui, Maria Luisa Bonet, Joel Gabàs, and Jordi Levy.
Improving sat-based weighted maxsat solvers.
In Milano [29], pages 86-101.
[ bib ]
|
|
[29]
|
Michela Milano, editor.
Principles and Practice of Constraint Programming - 18th
International Conference, CP 2012, Québec City, QC, Canada, October 8-12,
2012. Proceedings, volume 7514 of Lecture Notes in Computer Science.
Springer, 2012.
[ bib ]
|
|
[30]
|
Carlos Ansótegui, Maria Luisa Bonet, Jordi Levy, and Chu Min Li.
Analysis and generation of pseudo-industrial maxsat instances.
In Riaño et al. [31], pages 173-184.
[ bib ]
|
|
[31]
|
David Riaño, Eva Onaindia, and Miguel Cazorla, editors.
Artificial Intelligence Research and Development - Proceedings
of the 15th International Conference of the Catalan Association for
Artificial Intelligence, University of Alacant, Spain, October 24-26, 2012,
volume 248 of Frontiers in Artificial Intelligence and Applications.
IOS Press, 2012.
[ bib ]
|
|
[32]
|
Robert Nieuwenhuis.
Sat and smt are still resolution: Questions and challenges.
In Gramlich et al. [33], pages 10-13.
[ bib ]
|
|
[33]
|
Bernhard Gramlich, Dale Miller, and Uli Sattler, editors.
Automated Reasoning - 6th International Joint Conference, IJCAR
2012, Manchester, UK, June 26-29, 2012. Proceedings, volume 7364 of
Lecture Notes in Computer Science. Springer, 2012.
[ bib ]
|
|
[34]
|
Javier Larrosa, Robert Nieuwenhuis, Albert Oliveras, and Enric
Rodríguez-Carbonell.
A framework for certified boolean branch-and-bound optimization.
J. Autom. Reasoning, 46(1):81-102, 2011.
[ bib ]
|
|
[35]
|
Nikolaj Bjørner, Robert Nieuwenhuis, Helmut Veith, and Andrei Voronkov.
Decision procedures in soft, hard and bio-ware - follow up (dagstuhl
seminar 11272).
Dagstuhl Reports, 1(7):23-35, 2011.
[ bib ]
|
|
[36]
|
Roberto Asín, Robert Nieuwenhuis, Albert Oliveras, and Enric
Rodríguez-Carbonell.
Cardinality networks: a theoretical and empirical study.
Constraints, 16(2):195-221, 2011.
[ bib ]
|
|
[37]
|
Ignasi Abío, Robert Nieuwenhuis, Albert Oliveras, and Enric
Rodríguez-Carbonell.
Bdds for pseudo-boolean constraints - revisited.
In Sakallah and Simon [39], pages 61-75.
[ bib ]
|
|
[38]
|
Ignasi Abío, Morgan Deters, Robert Nieuwenhuis, and Peter J. Stuckey.
Reducing chaos in sat-like search: Finding solutions close to a given
one.
In Sakallah and Simon [39], pages 273-286.
[ bib ]
|
|
[39]
|
Karem A. Sakallah and Laurent Simon, editors.
Theory and Applications of Satisfiability Testing - SAT 2011 -
14th International Conference, SAT 2011, Ann Arbor, MI, USA, June 19-22,
2011. Proceedings, volume 6695 of Lecture Notes in Computer Science.
Springer, 2011.
[ bib ]
|
|
[40]
|
Natalia Flerova, Emma Rollon, and Rina Dechter.
Bucket and mini-bucket schemes for m best solutions over graphical
models.
In Croitoru et al. [41], pages 91-118.
[ bib ]
|
|
[41]
|
Madalina Croitoru, Sebastian Rudolph, Nic Wilson, John Howse, and Olivier
Corby, editors.
Graph Structures for Knowledge Representation and Reasoning -
Second International Workshop, GKR 2011, Barcelona, Spain, July 16, 2011.
Revised Selected Papers, volume 7205 of Lecture Notes in Computer
Science. Springer, 2012.
[ bib ]
|
|
[42]
|
Emma Rollon and Javier Larrosa.
On mini-buckets and the min-fill elimination ordering.
In Lee [43], pages 759-773.
[ bib ]
|
|
[43]
|
Jimmy Ho-Man Lee, editor.
Principles and Practice of Constraint Programming - CP 2011 -
17th International Conference, CP 2011, Perugia, Italy, September 12-16,
2011. Proceedings, volume 6876 of Lecture Notes in Computer Science.
Springer, 2011.
[ bib ]
|
|
[44]
|
Maria Luisa Bonet and Katherine St. John.
On the complexity of uspr distance.
IEEE/ACM Trans. Comput. Biology Bioinform., 7(3):572-576,
2010.
[ bib ]
|
|
[45]
|
Bozhena Bidyuk, Rina Dechter, and Emma Rollon.
Active tuples-based scheme for bounding posterior beliefs.
J. Artif. Intell. Res. (JAIR), 39:335-371, 2010.
[ bib ]
|
|
[46]
|
Marc Bezem, Robert Nieuwenhuis, and Enric Rodríguez-Carbonell.
Hard problems in max-algebra, control theory, hypergraphs and other
areas.
Inf. Process. Lett., 110(4):133-138, 2010.
[ bib ]
|
|
[47]
|
Antoine Miné and Enric Rodríguez-Carbonell.
Preface.
Electr. Notes Theor. Comput. Sci., 267(1):1-2, 2010.
[ bib ]
|
|
[48]
|
Albert Atserias and Maria Luisa Bonet.
On the automatizability of resolution and related propositional proof
systems.
Electronic Colloquium on Computational Complexity (ECCC),
(010), 2002.
[ bib ]
|
|
[49]
|
Hélène Fargier, Emma Rollon, and Nic Wilson.
Enabling local computation for partially ordered preferences.
Constraints, 15(4):516-539, 2010.
[ bib ]
|
|
[50]
|
Roberto Javier Asín Achá, Robert Nieuwenhuis, Albert Oliveras, and
Enric Rodríguez-Carbonell.
Practical algorithms for unsatisfiability proof and core generation
in sat solvers.
AI Commun., 23(2-3):145-157, 2010.
[ bib ]
|
|
[51]
|
Stefano Bistarelli, Fabio Gadducci, Javier Larrosa, Emma Rollon, and Francesco
Santini.
Extending soft arc consistency algorithms to non-invertible
semirings.
In Sidorov et al. [52], pages 386-398.
[ bib ]
|
|
[52]
|
Grigori Sidorov, Arturo Hernández Aguirre, and Carlos A. Reyes García,
editors.
Advances in Artificial Intelligence - 9th Mexican International
Conference on Artificial Intelligence, MICAI 2010, Pachuca, Mexico, November
8-13, 2010, Proceedings, Part I, volume 6437 of Lecture Notes in
Computer Science. Springer, 2010.
[ bib ]
|
|
[53]
|
Javier Larrosa, Albert Oliveras, and Enric Rodríguez-Carbonell.
Semiring-induced propositional logic: Definition and basic
algorithms.
In Clarke and Voronkov [54], pages 332-347.
[ bib ]
|
|
[54]
|
Edmund M. Clarke and Andrei Voronkov, editors.
Logic for Programming, Artificial Intelligence, and Reasoning -
16th International Conference, LPAR-16, Dakar, Senegal, April 25-May 1, 2010,
Revised Selected Papers, volume 6355 of Lecture Notes in Computer
Science. Springer, 2010.
[ bib ]
|
|
[55]
|
Emma Rollon and Rina Dechter.
Evaluating partition strategies for mini-bucket elimination.
In ISAIM [56].
[ bib ]
|
|
[56]
|
International Symposium on Artificial Intelligence and Mathematics (ISAIM
2010), Fort Lauderdale, Florida, USA, January 6-8, 2010, 2010.
[ bib ]
|
|
[57]
|
Robert Nieuwenhuis.
Sat modulo theories: Getting the best of sat and global constraint
filtering.
In Cohen [58], pages 1-2.
[ bib ]
|
|
[58]
|
David Cohen, editor.
Principles and Practice of Constraint Programming - CP 2010 -
16th International Conference, CP 2010, St. Andrews, Scotland, UK, September
6-10, 2010. Proceedings, volume 6308 of Lecture Notes in Computer
Science. Springer, 2010.
[ bib ]
|
|
[59]
|
Emma Rollon and Rina Dechter.
New mini-bucket partitioning heuristics for bounding the probability
of evidence.
In Fox and Poole [61].
[ bib ]
|
|
[60]
|
Carlos Ansótegui, Maria Luisa Bonet, and Jordi Levy.
A new algorithm for weighted partial maxsat.
In Fox and Poole [61].
[ bib ]
|
|
[61]
|
Maria Fox and David Poole, editors.
Proceedings of the Twenty-Fourth AAAI Conference on Artificial
Intelligence, AAAI 2010, Atlanta, Georgia, USA, July 11-15, 2010. AAAI
Press, 2010.
[ bib ]
|
|
[62]
|
Miquel Bofill and Albert Rubio.
Paramodulation with well-founded orderings.
J. Log. Comput., 19(2):263-302, 2009.
[ bib ]
|
|
[63]
|
Robert Nieuwenhuis.
Sat modulo theories: Enhancing sat with special-purpose algorithms.
In Kullmann [65], page 1.
[ bib ]
|
|
[64]
|
Javier Larrosa, Robert Nieuwenhuis, Albert Oliveras, and Enric
Rodríguez-Carbonell.
Branch and bound for boolean optimization and the generation of
optimality certificates.
In Kullmann [65], pages 453-466.
[ bib ]
|
|
[65]
|
Oliver Kullmann, editor.
Theory and Applications of Satisfiability Testing - SAT 2009,
12th International Conference, SAT 2009, Swansea, UK, June 30 - July 3, 2009.
Proceedings, volume 5584 of Lecture Notes in Computer Science.
Springer, 2009.
[ bib ]
|
|
[66]
|
Maria Luisa Bonet and Katherine St. John.
Efficiently calculating evolutionary tree measures using sat.
In Kullmann [65], pages 4-17.
[ bib ]
|
|
[67]
|
Roberto Asín, Robert Nieuwenhuis, Albert Oliveras, and Enric
Rodríguez-Carbonell.
Cardinality networks and their applications.
In Kullmann [65], pages 167-180.
[ bib ]
|
|
[68]
|
Carlos Ansótegui, Maria Luisa Bonet, and Jordi Levy.
Solving (weighted) partial maxsat through satisfiability testing.
In Kullmann [65], pages 427-440.
[ bib ]
|
|
[69]
|
Carlos Ansótegui, Maria Luisa Bonet, and Jordi Levy.
Towards industrial-like random sat instances.
In Boutilier [70], pages 387-392.
[ bib ]
|
|
[70]
|
Craig Boutilier, editor.
IJCAI 2009, Proceedings of the 21st International Joint
Conference on Artificial Intelligence, Pasadena, California, USA, July 11-17,
2009, 2009.
[ bib ]
|
|
[71]
|
Javier Larrosa and Barry O'Sullivan, editors.
Recent Advances in Constraints - 14th Annual ERCIM International
Workshop on Constraint Solving and Constraint Logic Programming, CSCLP 2009,
Barcelona, Spain, June 15-17, 2009, Revised Selected Papers, volume 6384 of
Lecture Notes in Computer Science. Springer, 2011.
[ bib ]
|
|
[72]
|
Carlos Ansótegui, Maria Luisa Bonet, and Jordi Levy.
On the structure of industrial sat instances.
In Gent [73], pages 127-141.
[ bib ]
|
|
[73]
|
Ian P. Gent, editor.
Principles and Practice of Constraint Programming - CP 2009,
15th International Conference, CP 2009, Lisbon, Portugal, September 20-24,
2009, Proceedings, volume 5732 of Lecture Notes in Computer Science.
Springer, 2009.
[ bib ]
|
|
[74]
|
Carlos Ansótegui, Maria Luisa Bonet, and Jordi Levy.
On solving maxsat through sat.
In Sandri et al. [75], pages 284-292.
[ bib ]
|
|
[75]
|
Sandra Sandri, Miquel Sànchez-Marrè, and Ulises Cortés, editors.
Artificial Intelligence Research and Development, Proceedings of
the 12th International Conference of the Catalan Association for Artificial
Intelligence, CCIA 2009, October 21-23, 2009, Vilar Rural de Cardona (El
Bages), Cardona, Spain, volume 202 of Frontiers in Artificial
Intelligence and Applications. IOS Press, 2009.
[ bib ]
|
|
[76]
|
Cristina Borralleras, Salvador Lucas, Rafael Navarro-Marset, Enric
Rodríguez-Carbonell, and Albert Rubio.
Solving non-linear polynomial arithmetic via sat modulo linear
arithmetic.
In Schmidt [77], pages 294-305.
[ bib ]
|
|
[77]
|
Renate A. Schmidt, editor.
Automated Deduction - CADE-22, 22nd International Conference on
Automated Deduction, Montreal, Canada, August 2-7, 2009. Proceedings, volume
5663 of Lecture Notes in Computer Science. Springer, 2009.
[ bib ]
|
|
[78]
|
Federico Heras, Javier Larrosa, Simon de Givry, and Thomas Schiex.
2006 and 2007 max-sat evaluations: Contributed instances.
JSAT, 4(2-4):239-250, 2008.
[ bib ]
|
|
[79]
|
Federico Heras, Javier Larrosa, and Albert Oliveras.
Minimaxsat: An efficient weighted max-sat solver.
J. Artif. Intell. Res. (JAIR), 31:1-32, 2008.
[ bib ]
|
|
[80]
|
Clark Barrett, Morgan Deters, Albert Oliveras, and Aaron Stump.
Design and results of the 3rd annual satisfiability modulo theories
competition (smt-comp 2007).
International Journal on Artificial Intelligence Tools,
17(4):569-606, 2008.
[ bib ]
|
|
[81]
|
Sava Krstic and Albert Oliveras.
Preface.
Electr. Notes Theor. Comput. Sci., 198(2):1-2, 2008.
[ bib ]
|
|
[82]
|
Marc Bezem, Robert Nieuwenhuis, and Enric Rodríguez-Carbonell.
Exponential behaviour of the butkovic-zimmermann algorithm for
solving two-sided linear systems in max-algebra.
Discrete Applied Mathematics, 156(18):3506-3509, 2008.
[ bib ]
|
|
[83]
|
Javier Larrosa, Federico Heras, and Simon de Givry.
A logical approach to efficient max-sat solving.
Artif. Intell., 172(2-3):204-233, 2008.
[ bib ]
|
|
[84]
|
Federico Heras and Javier Larrosa.
A max-sat inference-based pre-processing for max-clique.
In Büning and Zhao [85], pages 139-152.
[ bib ]
|
|
[85]
|
Hans Kleine Büning and Xishun Zhao, editors.
Theory and Applications of Satisfiability Testing - SAT 2008,
11th International Conference, SAT 2008, Guangzhou, China, May 12-15, 2008.
Proceedings, volume 4996 of Lecture Notes in Computer Science.
Springer, 2008.
[ bib ]
|
|
[86]
|
Germain Faure, Robert Nieuwenhuis, Albert Oliveras, and Enric
Rodríguez-Carbonell.
Sat modulo the theory of linear arithmetic: Exact, inexact and
commercial solvers.
In Büning and Zhao [85], pages 77-90.
[ bib ]
|
|
[87]
|
Marc Bezem, Robert Nieuwenhuis, and Enric Rodríguez-Carbonell.
The max-atom problem and its relevance.
In Cervesato et al. [88], pages 47-61.
[ bib ]
|
|
[88]
|
Iliano Cervesato, Helmut Veith, and Andrei Voronkov, editors.
Logic for Programming, Artificial Intelligence, and Reasoning,
15th International Conference, LPAR 2008, Doha, Qatar, November 22-27, 2008.
Proceedings, volume 5330 of Lecture Notes in Computer Science.
Springer, 2008.
[ bib ]
|
|
[89]
|
Roberto Asín, Robert Nieuwenhuis, Albert Oliveras, and Enric
Rodríguez-Carbonell.
Efficient generation of unsatisfiability proofs and cores in sat.
In Cervesato et al. [88], pages 16-30.
[ bib ]
|
|
[90]
|
Stefano Bistarelli, Fabio Gadducci, Javier Larrosa, and Emma Rollon.
A soft approach to multi-objective optimization.
In de la Banda and Pontelli [91], pages
764-768.
[ bib ]
|
|
[91]
|
Maria Garcia de la Banda and Enrico Pontelli, editors.
Logic Programming, 24th International Conference, ICLP 2008,
Udine, Italy, December 9-13 2008, Proceedings, volume 5366 of Lecture
Notes in Computer Science. Springer, 2008.
[ bib ]
|
|
[92]
|
Miquel Bofill, Robert Nieuwenhuis, Albert Oliveras, Enric
Rodríguez-Carbonell, and Albert Rubio.
A write-based solver for sat modulo the theory of arrays.
In Cimatti and Jones [93], pages 1-8.
[ bib ]
|
|
[93]
|
Alessandro Cimatti and Robert B. Jones, editors.
Formal Methods in Computer-Aided Design, FMCAD 2008, Portland,
Oregon, USA, 17-20 November 2008. IEEE, 2008.
[ bib ]
|
|
[94]
|
Frédéric Blanqui, Jean-Pierre Jouannaud, and Albert Rubio.
The computability path ordering: The end of a quest.
In Kaminski and Martini [95], pages 1-14.
[ bib ]
|
|
[95]
|
Michael Kaminski and Simone Martini, editors.
Computer Science Logic, 22nd International Workshop, CSL 2008,
17th Annual Conference of the EACSL, Bertinoro, Italy, September 16-19, 2008.
Proceedings, volume 5213 of Lecture Notes in Computer Science.
Springer, 2008.
[ bib ]
|
|
[96]
|
Carlos Ansótegui, Maria Luisa Bonet, and Jordi Levy.
Random sat instances à la carte.
In Alsinet et al. [97], pages 109-117.
[ bib ]
|
|
[97]
|
Teresa Alsinet, Josep Puyol-Gruart, and Carme Torras, editors.
Artificial Intelligence Research and Development, Proceedings of
the 11th International Conference of the Catalan Association for Artificial
Intelligence, CCIA 2008, October 22-24, 2008, Sant Martí d'Empúries,
Spain, volume 184 of Frontiers in Artificial Intelligence and
Applications. IOS Press, 2008.
[ bib ]
|
|
[98]
|
Miquel Bofill, Robert Nieuwenhuis, Albert Oliveras, Enric
Rodríguez-Carbonell, and Albert Rubio.
The barcelogic smt solver.
In Gupta and Malik [99], pages 294-298.
[ bib ]
|
|
[99]
|
Aarti Gupta and Sharad Malik, editors.
Computer Aided Verification, 20th International Conference, CAV
2008, Princeton, NJ, USA, July 7-14, 2008, Proceedings, volume 5123 of
Lecture Notes in Computer Science. Springer, 2008.
[ bib ]
|
|
[100]
|
Carlos Ansótegui, Maria Luisa Bonet, Jordi Levy, and Felip Manyà.
Measuring the hardness of sat instances.
In Fox and Gomes [101], pages 222-228.
[ bib ]
|
|
[101]
|
Dieter Fox and Carla P. Gomes, editors.
Proceedings of the Twenty-Third AAAI Conference on Artificial
Intelligence, AAAI 2008, Chicago, Illinois, USA, July 13-17, 2008. AAAI
Press, 2008.
[ bib ]
|
|
[102]
|
Franz Baader, Byron Cook, Jürgen Giesl, and Robert Nieuwenhuis.
07401 abstracts collection - deduction and decision procedures.
In Deduction and Decision Procedures
[103].
[ bib ]
|
|
[103]
|
Franz Baader, Byron Cook, Jürgen Giesl, and Robert Nieuwenhuis, editors.
Deduction and Decision Procedures, 30.09. - 05.10.2007, volume
07401 of Dagstuhl Seminar Proceedings. Internationales Begegnungs- und
Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany, 2007.
[ bib ]
|
|
[104]
|
Enric Rodríguez-Carbonell and Deepak Kapur.
Automatic generation of polynomial invariants of bounded degree using
abstract interpretation.
Sci. Comput. Program., 64(1):54-75, 2007.
[ bib ]
|
|
[105]
|
Enric Rodríguez-Carbonell and Deepak Kapur.
Generating all polynomial invariants in simple loops.
J. Symb. Comput., 42(4):443-476, 2007.
[ bib ]
|
|
[106]
|
Jean-Pierre Jouannaud and Albert Rubio.
Polymorphic higher-order recursive path orderings.
J. ACM, 54(1), 2007.
[ bib ]
|
|
[107]
|
Robert Nieuwenhuis and Albert Oliveras.
Fast congruence closure and extensions.
Inf. Comput., 205(4):557-580, 2007.
[ bib ]
|
|
[108]
|
Maria Luisa Bonet, Jordi Levy, and Felip Manyà.
Resolution for max-sat.
Artif. Intell., 171(8-9):606-618, 2007.
[ bib ]
|
|
[109]
|
Federico Heras, Javier Larrosa, and Albert Oliveras.
Minimaxsat: A new weighted max-sat solver.
In Marques-Silva and Sakallah [110], pages
41-55.
[ bib ]
|
|
[110]
|
João Marques-Silva and Karem A. Sakallah, editors.
Theory and Applications of Satisfiability Testing - SAT 2007,
10th International Conference, Lisbon, Portugal, May 28-31, 2007,
Proceedings, volume 4501 of Lecture Notes in Computer Science.
Springer, 2007.
[ bib ]
|
|
[111]
|
Carlos Ansótegui, Maria Luisa Bonet, Jordi Levy, and Felip Manyà.
Mapping csp into many-valued sat.
In Marques-Silva and Sakallah [110], pages
10-15.
[ bib ]
|
|
[112]
|
Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, and Albert
Rubio.
Challenges in satisfiability modulo theories.
In Baader [113], pages 2-18.
[ bib ]
|
|
[113]
|
Franz Baader, editor.
Term Rewriting and Applications, 18th International Conference,
RTA 2007, Paris, France, June 26-28, 2007, Proceedings, volume 4533 of
Lecture Notes in Computer Science. Springer, 2007.
[ bib ]
|
|
[114]
|
Frédéric Blanqui, Jean-Pierre Jouannaud, and Albert Rubio.
Horpo with computability closure: A reconstruction.
In Dershowitz and Voronkov [115], pages
138-150.
[ bib ]
|
|
[115]
|
Nachum Dershowitz and Andrei Voronkov, editors.
Logic for Programming, Artificial Intelligence, and Reasoning,
14th International Conference, LPAR 2007, Yerevan, Armenia, October 15-19,
2007, Proceedings, volume 4790 of Lecture Notes in Computer Science.
Springer, 2007.
[ bib ]
|
|
[116]
|
Carlos Ansótegui, Maria Luisa Bonet, Jordi Levy, and Felip Manyà.
A complete resolution calculus for signed max-sat.
In ISMVL [117], page 22.
[ bib ]
|
|
[117]
|
37th International Symposium on Multiple-Valued Logic, ISMVL 2007, 13-16
May 2007, Oslo, Norway. IEEE Computer Society, 2007.
[ bib ]
|
|
[118]
|
Carlos Ansótegui, Maria Luisa Bonet, Jordi Levy, and Felip Manyà.
The logic behind weighted csp.
In Veloso [119], pages 32-37.
[ bib ]
|
|
[119]
|
Manuela M. Veloso, editor.
IJCAI 2007, Proceedings of the 20th International Joint
Conference on Artificial Intelligence, Hyderabad, India, January 6-12, 2007,
2007.
[ bib ]
|
|
[120]
|
Franz Baader, Byron Cook, Jürgen Giesl, and Robert Nieuwenhuis.
07401 executive summary - deduction and decision procedures.
In Deduction and Decision Procedures
[103].
[ bib ]
|
|
[121]
|
Carlos Ansótegui, Maria Luisa Bonet, Jordi Levy, and Felip Manyà.
What is a real-world sat instance?
In Angulo and Godo [122], pages 19-28.
[ bib ]
|
|
[122]
|
Cecilio Angulo and Lluis Godo, editors.
Artificial Intelligence Research and Development, Proceedings of
the 10th International Conference of the ACIA, CCIA 2007, October 25-26,
2007, Sant Julià de Lòria, Andorra, volume 163 of Frontiers in
Artificial Intelligence and Applications. IOS Press, 2007.
[ bib ]
|
|
[123]
|
Cristina Borralleras and Albert Rubio.
Orderings and constraints: Theory and practice of proving
termination.
In Comon-Lundh et al. [124], pages
28-43.
[ bib ]
|
|
[124]
|
Hubert Comon-Lundh, Claude Kirchner, and Hélène Kirchner, editors.
Rewriting, Computation and Proof, Essays Dedicated to Jean-
Pierre Jouannaud on the Occasion of His 60th Birthday, volume 4600 of
Lecture Notes in Computer Science. Springer, 2007.
[ bib ]
|
|
[125]
|
Emma Rollon and Javier Larrosa.
Multi-objective russian doll search.
In AAAI [126], pages 249-254.
[ bib ]
|
|
[126]
|
Proceedings of the Twenty-Second AAAI Conference on Artificial
Intelligence, July 22-26, 2007, Vancouver, British Columbia, Canada. AAAI
Press, 2007.
[ bib ]
|
|
[127]
|
Carlos Ansótegui, Maria Luisa Bonet, Jordi Levy, and Felip Manyà.
Inference rules for high-order consistency in weighted csp.
In AAAI [126], pages 167-172.
[ bib ]
|
|
[128]
|
Maria Luisa Bonet, Katherine St. John, Ruchi Mahindru, and Nina Amenta.
Approximating subtree distances between phylogenies.
Journal of Computational Biology, 13(8):1419-1434, 2006.
[ bib ]
|
|
[129]
|
Robert Nieuwenhuis, Albert Oliveras, and Cesare Tinelli.
Solving sat and sat modulo theories: From an abstract davis-
putnam-logemann-loveland procedure to dpll(t).
J. ACM, 53(6):937-977, 2006.
[ bib ]
|
|
[130]
|
Emma Rollon and Javier Larrosa.
Bucket elimination for multiobjective optimization problems.
J. Heuristics, 12(4-5):307-328, 2006.
[ bib ]
|
|
[131]
|
Federico Heras and Javier Larrosa.
Intelligent variable orderings and re-orderings in dac-based solvers
for wcsp.
J. Heuristics, 12(4-5):287-306, 2006.
[ bib ]
|
|
[132]
|
Robert Nieuwenhuis and Albert Oliveras.
On sat modulo theories and optimization problems.
In Biere and Gomes [133], pages 156-169.
[ bib ]
|
|
[133]
|
Armin Biere and Carla P. Gomes, editors.
Theory and Applications of Satisfiability Testing - SAT 2006,
9th International Conference, Seattle, WA, USA, August 12-15, 2006,
Proceedings, volume 4121 of Lecture Notes in Computer Science.
Springer, 2006.
[ bib ]
|
|
[134]
|
Maria Luisa Bonet, Jordi Levy, and Felip Manyà.
A complete calculus for max-sat.
In Biere and Gomes [133], pages 240-251.
[ bib ]
|
|
[135]
|
Jean-Pierre Jouannaud and Albert Rubio.
Higher-order orderings for normal rewriting.
In Pfenning [136], pages 387-399.
[ bib ]
|
|
[136]
|
Frank Pfenning, editor.
Term Rewriting and Applications, 17th International Conference,
RTA 2006, Seattle, WA, USA, August 12-14, 2006, Proceedings, volume 4098 of
Lecture Notes in Computer Science. Springer, 2006.
[ bib ]
|
|
[137]
|
Frédéric Blanqui, Jean-Pierre Jouannaud, and Albert Rubio.
Higher-order termination: From kruskal to computability.
In Hermann and Voronkov [138], pages 1-14.
[ bib ]
|
|
[138]
|
Miki Hermann and Andrei Voronkov, editors.
Logic for Programming, Artificial Intelligence, and Reasoning,
13th International Conference, LPAR 2006, Phnom Penh, Cambodia, November
13-17, 2006, Proceedings, volume 4246 of Lecture Notes in Computer
Science. Springer, 2006.
[ bib ]
|
|
[139]
|
Clark Barrett, Robert Nieuwenhuis, Albert Oliveras, and Cesare Tinelli.
Splitting on demand in sat modulo theories.
In Hermann and Voronkov [138], pages 512-526.
[ bib ]
|
|
[140]
|
Emma Rollon and Javier Larrosa.
Multi-objective propagation in constraint programming.
In Brewka et al. [141], pages 128-132.
[ bib ]
|
|
[141]
|
Gerhard Brewka, Silvia Coradeschi, Anna Perini, and Paolo Traverso, editors.
ECAI 2006, 17th European Conference on Artificial Intelligence,
August 29 - September 1, 2006, Riva del Garda, Italy, Including Prestigious
Applications of Intelligent Systems (PAIS 2006), Proceedings, volume 141 of
Frontiers in Artificial Intelligence and Applications. IOS Press, 2006.
[ bib ]
|
|
[142]
|
Emma Rollon and Javier Larrosa.
Mini-bucket elimination with bucket propagation.
In Benhamou [143], pages 484-498.
[ bib ]
|
|
[143]
|
Frédéric Benhamou, editor.
Principles and Practice of Constraint Programming - CP 2006,
12th International Conference, CP 2006, Nantes, France, September 25-29,
2006, Proceedings, volume 4204 of Lecture Notes in Computer Science.
Springer, 2006.
[ bib ]
|
|
[144]
|
Shuvendu K. Lahiri, Robert Nieuwenhuis, and Albert Oliveras.
Smt techniques for fast predicate abstraction.
In Ball and Jones [145], pages 424-437.
[ bib ]
|
|
[145]
|
Thomas Ball and Robert B. Jones, editors.
Computer Aided Verification, 18th International Conference, CAV
2006, Seattle, WA, USA, August 17-20, 2006, Proceedings, volume 4144 of
Lecture Notes in Computer Science. Springer, 2006.
[ bib ]
|
|
[146]
|
Federico Heras and Javier Larrosa.
New inference rules for efficient max-sat solving.
In AAAI [147], pages 68-73.
[ bib ]
|
|
[147]
|
Proceedings, The Twenty-First National Conference on Artificial
Intelligence and the Eighteenth Innovative Applications of Artificial
Intelligence Conference, July 16-20, 2006, Boston, Massachusetts, USA. AAAI
Press, 2006.
[ bib ]
|
|
[148]
|
Javier Larrosa, Enric Morancho, and David Niso.
On the practical use of variable elimination in constraint
optimization problems: 'still-life' as a case study.
J. Artif. Intell. Res. (JAIR), 23:421-440, 2005.
[ bib ]
|
|
[149]
|
Kalev Kask, Rina Dechter, Javier Larrosa, and Avi Dechter.
Unifying tree decompositions for reasoning in graphical models.
Artif. Intell., 166(1-2):165-193, 2005.
[ bib ]
|
|
[150]
|
Franz Baader, Peter Baumgartner, Robert Nieuwenhuis, and Andrei Voronkov,
editors.
Deduction and Applications, 23.-28. October 2005, volume 05431
of Dagstuhl Seminar Proceedings. Internationales Begegnungs- und
Forschungszentrum für Informatik (IBFI), Schloss Dagstuhl, Germany, 2006.
[ bib ]
|
|
[151]
|
Roberto Bagnara, Enric Rodríguez-Carbonell, and Enea Zaffanella.
Generation of basic semi-algebraic invariants using convex polyhedra.
In Hankin and Siveroni [152], pages 19-34.
[ bib ]
|
|
[152]
|
Chris Hankin and Igor Siveroni, editors.
Static Analysis, 12th International Symposium, SAS 2005, London,
UK, September 7-9, 2005, Proceedings, volume 3672 of Lecture Notes in
Computer Science. Springer, 2005.
[ bib ]
|
|
[153]
|
Robert Nieuwenhuis and Albert Oliveras.
Proof-producing congruence closure.
In Giesl [154], pages 453-468.
[ bib ]
|
|
[154]
|
Jürgen Giesl, editor.
Term Rewriting and Applications, 16th International Conference,
RTA 2005, Nara, Japan, April 19-21, 2005, Proceedings, volume 3467 of
Lecture Notes in Computer Science. Springer, 2005.
[ bib ]
|
|
[155]
|
Mirtha-Lina Fernández, Guillem Godoy, and Albert Rubio.
Orderings for innermost termination.
In Giesl [154], pages 17-31.
[ bib ]
|
|
[156]
|
Robert Nieuwenhuis and Albert Oliveras.
Decision procedures for sat, sat modulo theories and beyond. the
barcelogictools.
In Sutcliffe and Voronkov [157], pages 23-46.
[ bib ]
|
|
[157]
|
Geoff Sutcliffe and Andrei Voronkov, editors.
Logic for Programming, Artificial Intelligence, and Reasoning,
12th International Conference, LPAR 2005, Montego Bay, Jamaica, December 2-6,
2005, Proceedings, volume 3835 of Lecture Notes in Computer Science.
Springer, 2005.
[ bib ]
|
|
[158]
|
Mirtha-Lina Fernández, Guillem Godoy, and Albert Rubio.
Recursive path orderings can also be incremental.
In Sutcliffe and Voronkov [157], pages 230-245.
[ bib ]
|
|
[159]
|
Martí Sánchez, Javier Larrosa, and Pedro Meseguer.
Improving tree decomposition methods with function filtering.
In Kaelbling and Saffiotti [160], pages
1537-1538.
[ bib ]
|
|
[160]
|
Leslie Pack Kaelbling and Alessandro Saffiotti, editors.
IJCAI-05, Proceedings of the Nineteenth International Joint
Conference on Artificial Intelligence, Edinburgh, Scotland, UK, July
30-August 5, 2005. Professional Book Center, 2005.
[ bib ]
|
|
[161]
|
Javier Larrosa and Federico Heras.
Resolution in max-sat and its relation to local consistency in
weighted csps.
In Kaelbling and Saffiotti [160], pages
193-198.
[ bib ]
|
|
[162]
|
Simon de Givry, Federico Heras, Matthias Zytnicki, and Javier Larrosa.
Existential arc consistency: Getting closer to full arc consistency
in weighted csps.
In Kaelbling and Saffiotti [160], pages 84-89.
[ bib ]
|
|
[163]
|
Enric Rodríguez-Carbonell and Ashish Tiwari.
Generating polynomial invariants for hybrid systems.
In Morari and Thiele [164], pages 590-605.
[ bib ]
|
|
[164]
|
Manfred Morari and Lothar Thiele, editors.
Hybrid Systems: Computation and Control, 8th International
Workshop, HSCC 2005, Zurich, Switzerland, March 9-11, 2005, Proceedings,
volume 3414 of Lecture Notes in Computer Science. Springer, 2005.
[ bib ]
|
|
[165]
|
Franz Baader, Peter Baumgartner, Robert Nieuwenhuis, and Andrei Voronkov.
05431 executive summary - deduction and applications.
In Deduction and Applications
[150].
[ bib ]
|
|
[166]
|
Martí Sánchez, Javier Larrosa, and Pedro Meseguer.
Tree decomposition with function filtering.
In van Beek [167], pages 593-606.
[ bib ]
|
|
[167]
|
Peter van Beek, editor.
Principles and Practice of Constraint Programming - CP 2005,
11th International Conference, CP 2005, Sitges, Spain, October 1-5, 2005,
Proceedings, volume 3709 of Lecture Notes in Computer Science.
Springer, 2005.
[ bib ]
|
|
[168]
|
Emma Rollon and Javier Larrosa.
Depth-first mini-bucket elimination.
In van Beek [167], pages 563-577.
[ bib ]
|
|
[169]
|
Federico Heras and Javier Larrosa.
Local consistency in weighted csps and inference in max-sat.
In van Beek [167], page 849.
[ bib ]
|
|
[170]
|
Robert Nieuwenhuis and Albert Oliveras.
Dpll(t) with exhaustive theory propagation and its application to
difference logic.
In Etessami and Rajamani [171], pages 321-334.
[ bib ]
|
|
[171]
|
Kousha Etessami and Sriram K. Rajamani, editors.
Computer Aided Verification, 17th International Conference, CAV
2005, Edinburgh, Scotland, UK, July 6-10, 2005, Proceedings, volume 3576 of
Lecture Notes in Computer Science. Springer, 2005.
[ bib ]
|
|
[172]
|
Robert Nieuwenhuis, editor.
Automated Deduction - CADE-20, 20th International Conference on
Automated Deduction, Tallinn, Estonia, July 22-27, 2005, Proceedings, volume
3632 of Lecture Notes in Computer Science. Springer, 2005.
[ bib ]
|
|
[173]
|
Robert Clarisó, Enric Rodríguez-Carbonell, and Jordi Cortadella.
Derivation of non-structural invariants of petri nets using abstract
interpretation.
In Ciardo and Darondeau [174], pages 188-207.
[ bib ]
|
|
[174]
|
Gianfranco Ciardo and Philippe Darondeau, editors.
Applications and Theory of Petri Nets 2005, 26th International
Conference, ICATPN 2005, Miami, USA, June 20-25, 2005, Proceedings, volume
3536 of Lecture Notes in Computer Science. Springer, 2005.
[ bib ]
|
|
[175]
|
Franz Baader, Peter Baumgartner, Robert Nieuwenhuis, and Andrei Voronkov.
05431 abstracts collection - deduction and applications.
In Deduction and Applications
[150].
[ bib ]
|
|
[176]
|
Guillem Godoy, Robert Nieuwenhuis, and Ashish Tiwari.
Classes of term rewrite systems with polynomial confluence problems.
ACM Trans. Comput. Log., 5(2):321-331, 2004.
[ bib ]
|
|
[177]
|
Juan Luis Esteban, Nicola Galesi, and Jochen Messner.
On the complexity of resolution with bounded conjunctions.
Theor. Comput. Sci., 321(2-3):347-370, 2004.
[ bib ]
|
|
[178]
|
Guillem Godoy and Robert Nieuwenhuis.
Superposition with completely built-in abelian groups.
J. Symb. Comput., 37(1):1-33, 2004.
[ bib ]
|
|
[179]
|
Harald Ganzinger, Robert Nieuwenhuis, and Pilar Nivela.
Fast term indexing with coded context trees.
J. Autom. Reasoning, 32(2):103-120, 2004.
[ bib ]
|
|
[180]
|
Albert Atserias and Maria Luisa Bonet.
On the automatizability of resolution and related propositional proof
systems.
Inf. Comput., 189(2):182-201, 2004.
[ bib ]
|
|
[181]
|
Guillem Godoy and Robert Nieuwenhuis.
Constraint solving for term orderings compatible with abelian
semigroups, monoids and groups.
Constraints, 9(3):167-192, 2004.
[ bib ]
|
|
[182]
|
Maria Luisa Bonet, Carlos Domingo, Ricard Gavaldà, Alexis Maciel, and
Toniann Pitassi.
Non-automatizability of bounded-depth frege proofs.
Computational Complexity, 13(1-2):47-68, 2004.
[ bib ]
|
|
[183]
|
Javier Larrosa and Thomas Schiex.
Solving weighted csp by maintaining arc consistency.
Artif. Intell., 159(1-2):1-26, 2004.
[ bib ]
|
|
[184]
|
Enric Rodríguez-Carbonell and Deepak Kapur.
An abstract interpretation approach for automatic generation of
polynomial invariants.
In Giacobazzi [185], pages 280-295.
[ bib ]
|
|
[185]
|
Roberto Giacobazzi, editor.
Static Analysis, 11th International Symposium, SAS 2004, Verona,
Italy, August 26-28, 2004, Proceedings, volume 3148 of Lecture Notes in
Computer Science. Springer, 2004.
[ bib ]
|
|
[186]
|
Robert Nieuwenhuis, Albert Oliveras, and Cesare Tinelli.
Abstract dpll and abstract dpll modulo theories.
In Baader and Voronkov [187], pages 36-50.
[ bib ]
|
|
[187]
|
Franz Baader and Andrei Voronkov, editors.
Logic for Programming, Artificial Intelligence, and Reasoning,
11th International Conference, LPAR 2004, Montevideo, Uruguay, March 14-18,
2005, Proceedings, volume 3452 of Lecture Notes in Computer Science.
Springer, 2005.
[ bib ]
|
|
[188]
|
Enric Rodríguez-Carbonell and Deepak Kapur.
Automatic generation of polynomial loop.
In Gutierrez [189], pages 266-273.
[ bib ]
|
|
[189]
|
Jaime Gutierrez, editor.
Symbolic and Algebraic Computation, International Symposium
ISSAC 2004, Santander, Spain, July 4-7, 2004, Proceedings. ACM, 2004.
[ bib ]
|
|
[190]
|
Enric Rodríguez-Carbonell and Deepak Kapur.
Program verification using automatic generation of invariants.
In Liu and Araki [191], pages 325-340.
[ bib ]
|
|
[191]
|
Zhiming Liu and Keijiro Araki, editors.
Theoretical Aspects of Computing - ICTAC 2004, First
International Colloquium, Guiyang, China, September 20-24, 2004, Revised
Selected Papers, volume 3407 of Lecture Notes in Computer Science.
Springer, 2005.
[ bib ]
|
|
[192]
|
Martí Sánchez, Pedro Meseguer, and Javier Larrosa.
Using constraints with memory to implement variable elimination.
In de Mántaras and Saitta [193], pages
216-220.
[ bib ]
|
|
[193]
|
Ramon López de Mántaras and Lorenza Saitta, editors.
Proceedings of the 16th Eureopean Conference on Artificial
Intelligence, ECAI'2004, including Prestigious Applicants of Intelligent
Systems, PAIS 2004, Valencia, Spain, August 22-27, 2004. IOS Press, 2004.
[ bib ]
|
|
[194]
|
Martí Sánchez, Pedro Meseguer, and Javier Larrosa.
Improving the applicability of adaptive consistency: Preliminary
results.
In Wallace [195], pages 757-761.
[ bib ]
|
|
[195]
|
Mark Wallace, editor.
Principles and Practice of Constraint Programming - CP 2004,
10th International Conference, CP 2004, Toronto, Canada, September 27 -
October 1, 2004, Proceedings, volume 3258 of Lecture Notes in Computer
Science. Springer, 2004.
[ bib ]
|
|
[196]
|
Harald Ganzinger, George Hagen, Robert Nieuwenhuis, Albert Oliveras, and Cesare
Tinelli.
Dpll( t): Fast decision procedures.
In Alur and Peled [197], pages 175-188.
[ bib ]
|
|
[197]
|
Rajeev Alur and Doron Peled, editors.
Computer Aided Verification, 16th International Conference, CAV
2004, Boston, MA, USA, July 13-17, 2004, Proceedings, volume 3114 of
Lecture Notes in Computer Science. Springer, 2004.
[ bib ]
|
|
[198]
|
Miquel Bofill and Albert Rubio.
Redundancy notions for paramodulation with non-monotonic orderings.
In Basin and Rusinowitch [199], pages 107-121.
[ bib ]
|
|
[199]
|
David A. Basin and Michaël Rusinowitch, editors.
Automated Reasoning - Second International Joint Conference,
IJCAR 2004, Cork, Ireland, July 4-8, 2004, Proceedings, volume 3097 of
Lecture Notes in Computer Science. Springer, 2004.
[ bib ]
|
|
[200]
|
Hubert Comon, Paliath Narendran, Robert Nieuwenhuis, and Michaël
Rusinowitch.
Deciding the confluence of ordered term rewrite systems.
ACM Trans. Comput. Log., 4(1):33-55, 2003.
[ bib ]
|
|
[201]
|
Anatoli Degtyarev, Robert Nieuwenhuis, and Andrei Voronkov.
Stratified resolution.
J. Symb. Comput., 36(1-2):79-99, 2003.
[ bib ]
|
|
[202]
|
Miquel Bofill, Guillem Godoy, Robert Nieuwenhuis, and Albert Rubio.
Paramodulation and knuth-bendix completion with nontotal and
nonmonotonic orderings.
J. Autom. Reasoning, 30(1):99-120, 2003.
[ bib ]
|
|
[203]
|
Juan Luis Esteban and Jacobo Torán.
A combinatorial characterization of treelike resolution space.
Inf. Process. Lett., 87(6):295-300, 2003.
[ bib ]
|
|
[204]
|
Javier Larrosa and Rina Dechter.
Boosting search with variable elimination in constraint optimization
and constraint satisfaction problems.
Constraints, 8(3):303-326, 2003.
[ bib ]
|
|
[205]
|
Maria Luisa Bonet and Nicola Galesi.
Degree complexity for a modified pigeonhole principle.
Arch. Math. Log., 42(5):403-414, 2003.
[ bib ]
|
|
[206]
|
Javier Larrosa and Pedro Meseguer.
Algoritmos para satisfacción de restricciones.
Inteligencia Artificial, Revista Iberoamericana de Inteligencia
Artificial, 7(20):31-42, 2003.
[ bib ]
|
|
[207]
|
Cristina Borralleras and Albert Rubio.
Monotonic ac-compatible semantic path orderings.
In Nieuwenhuis [208], pages 279-295.
[ bib ]
|
|
[208]
|
Robert Nieuwenhuis, editor.
Rewriting Techniques and Applications, 14th International
Conference, RTA 2003, Valencia, Spain, June 9-11, 2003, Proceedings, volume
2706 of Lecture Notes in Computer Science. Springer, 2003.
[ bib ]
|
|
[209]
|
Robert Nieuwenhuis and Albert Oliveras.
Congruence closure with integer offsets.
In Vardi and Voronkov [210], pages 78-90.
[ bib ]
|
|
[210]
|
Moshe Y. Vardi and Andrei Voronkov, editors.
Logic for Programming, Artificial Intelligence, and Reasoning,
10th International Conference, LPAR 2003, Almaty, Kazakhstan, September
22-26, 2003, Proceedings, volume 2850 of Lecture Notes in Computer
Science. Springer, 2003.
[ bib ]
|
|
[211]
|
Javier Larrosa and Thomas Schiex.
In the quest of the best form of local consistency for weighted csp.
In Gottlob and Walsh [212], pages 239-244.
[ bib ]
|
|
[212]
|
Georg Gottlob and Toby Walsh, editors.
IJCAI-03, Proceedings of the Eighteenth International Joint
Conference on Artificial Intelligence, Acapulco, Mexico, August 9-15, 2003.
Morgan Kaufmann, 2003.
[ bib ]
|
|
[213]
|
Javier Larrosa and Enric Morancho.
Solving 'still life' with soft constraints and bucket elimination.
In Rossi [214], pages 466-479.
[ bib ]
|
|
[214]
|
Francesca Rossi, editor.
Principles and Practice of Constraint Programming - CP 2003, 9th
International Conference, CP 2003, Kinsale, Ireland, September 29 - October
3, 2003, Proceedings, volume 2833 of Lecture Notes in Computer
Science. Springer, 2003.
[ bib ]
|
|
[215]
|
Simon de Givry, Javier Larrosa, Pedro Meseguer, and Thomas Schiex.
Solving max-sat as weighted csp.
In Rossi [214], pages 363-376.
[ bib ]
|
|
[216]
|
Javier Larrosa and Gabriel Valiente.
Constraint satisfaction algorithms for graph pattern matching.
Mathematical Structures in Computer Science, 12(4):403-422,
2002.
[ bib ]
|
|
[217]
|
Albert Rubio.
A fully syntactic ac-rpo.
Inf. Comput., 178(2):515-533, 2002.
[ bib ]
|
|
[218]
|
Robert Nieuwenhuis and José Miguel Rivero.
Practical algorithms for deciding path ordering constraint
satisfaction.
Inf. Comput., 178(2):422-440, 2002.
[ bib ]
|
|
[219]
|
Albert Atserias, Maria Luisa Bonet, and Juan Luis Esteban.
Lower bounds for the weak pigeonhole principle and random formulas
beyond resolution.
Inf. Comput., 176(2):136-152, 2002.
[ bib ]
|
|
[220]
|
Javier Larrosa and Pedro Meseguer.
Partition-based lower bound for max-csp.
Constraints, 7(3-4):407-419, 2002.
[ bib ]
|
|
[221]
|
Robert Nieuwenhuis.
The impact of casc in the development of automated deduction systems.
AI Commun., 15(2-3):77-78, 2002.
[ bib ]
|
|
[222]
|
Christian Bessière, Pedro Meseguer, Eugene C. Freuder, and Javier Larrosa.
On forward checking for non-binary constraint satisfaction.
Artif. Intell., 141(1/2):205-224, 2002.
[ bib ]
|
|
[223]
|
Juan Luis Esteban, Nicola Galesi, and Jochen Messner.
On the complexity of resolution with bounded conjunctions.
In Widmayer et al. [224], pages 220-231.
[ bib ]
|
|
[224]
|
Peter Widmayer, Francisco Triguero Ruiz, Rafael Morales Bueno, Matthew
Hennessy, Stephan Eidenbenz, and Ricardo Conejo, editors.
Automata, Languages and Programming, 29th International
Colloquium, ICALP 2002, Malaga, Spain, July 8-13, 2002, Proceedings, volume
2380 of Lecture Notes in Computer Science. Springer, 2002.
[ bib ]
|
|
[225]
|
Javier Larrosa, Pedro Meseguer, and Martí Sánchez.
Pseudo-tree search with soft constraints.
In van Harmelen [226], pages 131-135.
[ bib ]
|
|
[226]
|
Frank van Harmelen, editor.
Proceedings of the 15th Eureopean Conference on Artificial
Intelligence, ECAI'2002, Lyon, France, July 2002. IOS Press, 2002.
[ bib ]
|
|
[227]
|
Albert Atserias and Maria Luisa Bonet.
On the automatizability of resolution and related propositional proof
systems.
In Bradfield [228], pages 569-583.
[ bib ]
|
|
[228]
|
Julian C. Bradfield, editor.
Computer Science Logic, 16th International Workshop, CSL 2002,
11th Annual Conference of the EACSL, Edinburgh, Scotland, UK, September
22-25, 2002, Proceedings, volume 2471 of Lecture Notes in Computer
Science. Springer, 2002.
[ bib ]
|
|
[229]
|
Cristina Borralleras, Salvador Lucas, and Albert Rubio.
Recursive path orderings can be context-sensitive.
In Voronkov [230], pages 314-331.
[ bib ]
|
|
[230]
|
Andrei Voronkov, editor.
Automated Deduction - CADE-18, 18th International Conference on
Automated Deduction, Copenhagen, Denmark, July 27-30, 2002, Proceedings,
volume 2392 of Lecture Notes in Computer Science. Springer, 2002.
[ bib ]
|
|
[231]
|
Miquel Bofill and Albert Rubio.
Well-foundedness is sufficient for completeness of ordered
paramodulation.
In Voronkov [230], pages 456-470.
[ bib ]
|
|
[232]
|
Steven Willmott, Monique Calisti, and Emma Rollon.
Challenges in large-scale open agent mediated economies.
In Padget et al. [233], pages 325-340.
[ bib ]
|
|
[233]
|
Julian A. Padget, Onn Shehory, David C. Parkes, Norman M. Sadeh, and William E.
Walsh, editors.
Agent-Mediated Electronic Commerce IV, Designing Mechanisms and
Systems, AAMAS 2002 Workshop on Agent Mediated Electronic Commerce, Bologna,
Italy, July 16, 2002, Revised Papers, volume 2531 of Lecture Notes in
Computer Science. Springer, 2002.
[ bib ]
|
|
[234]
|
Javier Larrosa.
Node and arc consistency in weighted csp.
In Dechter and Sutton [235], pages 48-53.
[ bib ]
|
|
[235]
|
Rina Dechter and Richard S. Sutton, editors.
Proceedings of the Eighteenth National Conference on Artificial
Intelligence and Fourteenth Conference on Innovative Applications of
Artificial Intelligence, July 28 - August 1, 2002, Edmonton, Alberta,
Canada. AAAI Press / The MIT Press, 2002.
[ bib ]
|
|
[236]
|
Juan Luis Esteban and Jacobo Torán.
Space bounds for resolution.
Inf. Comput., 171(1):84-97, 2001.
[ bib ]
|
|
[237]
|
S. Baumer, Juan Luis Esteban, and Jacobo Torán.
Minimally unsatisfiable cnf formulas.
Bulletin of the EATCS, 74:190-192, 2001.
[ bib ]
|
|
[238]
|
Maria Luisa Bonet and Nicola Galesi.
Optimality of size-width tradeoffs for resolution.
Computational Complexity, 10(4):261-276, 2001.
[ bib ]
|
|
[239]
|
Cristina Borralleras and Albert Rubio.
A monotonic higher-order semantic path ordering.
In Nieuwenhuis and Voronkov [240], pages
531-547.
[ bib ]
|
|
[240]
|
Robert Nieuwenhuis and Andrei Voronkov, editors.
Logic for Programming, Artificial Intelligence, and Reasoning,
8th International Conference, LPAR 2001, Havana, Cuba, December 3-7, 2001,
Proceedings, volume 2250 of Lecture Notes in Computer Science.
Springer, 2001.
[ bib ]
|
|
[241]
|
Guillem Godoy and Robert Nieuwenhuis.
On ordering constraints for deduction with built-in abelian
semigroups, monoids and groups.
In LICS [242], pages 38-47.
[ bib ]
|
|
[242]
|
16th Annual IEEE Symposium on Logic in Computer Science, Boston,
Massachusetts, USA, June 16-19, 2001, Proceedings. IEEE Computer Society,
2001.
[ bib ]
|
|
[243]
|
Albert Atserias, Maria Luisa Bonet, and Juan Luis Esteban.
Lower bounds for the weak pigeonhole principle beyond resolution.
In Orejas et al. [244], pages 1005-1016.
[ bib ]
|
|
[244]
|
Fernando Orejas, Paul G. Spirakis, and Jan van Leeuwen, editors.
Automata, Languages and Programming, 28th International
Colloquium, ICALP 2001, Crete, Greece, July 8-12, 2001, Proceedings, volume
2076 of Lecture Notes in Computer Science. Springer, 2001.
[ bib ]
|
|
[245]
|
Hubert Comon, Guillem Godoy, and Robert Nieuwenhuis.
The confluence of ground term rewrite systems is decidable in
polynomial time.
In FOCS [246], pages 298-307.
[ bib ]
|
|
[246]
|
42nd Annual Symposium on Foundations of Computer Science, FOCS 2001, 14-17
October 2001, Las Vegas, Nevada, USA. IEEE Computer Society, 2001.
[ bib ]
|
|
[247]
|
Pedro Meseguer, Javier Larrosa, and Martí Sánchez.
Lower bounds for non-binary constraint optimization problems.
In Walsh [248], pages 317-331.
[ bib ]
|
|
[248]
|
Toby Walsh, editor.
Principles and Practice of Constraint Programming - CP 2001, 7th
International Conference, CP 2001, Paphos, Cyprus, November 26 - December 1,
2001, Proceedings, volume 2239 of Lecture Notes in Computer Science.
Springer, 2001.
[ bib ]
|
|
[249]
|
Rina Dechter, Kalev Kask, and Javier Larrosa.
A general scheme for multiple lower bound computation in constraint
optimization.
In Walsh [248], pages 346-360.
[ bib ]
|
|
[250]
|
Robert Nieuwenhuis, Thomas Hillenbrand, Alexandre Riazanov, and Andrei
Voronkov.
On the evaluation of indexing techniques for theorem proving.
In Goré et al. [251], pages 257-271.
[ bib ]
|
|
[251]
|
Rajeev Goré, Alexander Leitsch, and Tobias Nipkow, editors.
Automated Reasoning, First International Joint Conference, IJCAR
2001, Siena, Italy, June 18-23, 2001, Proceedings, volume 2083 of
Lecture Notes in Computer Science. Springer, 2001.
[ bib ]
|
|
[252]
|
Harald Ganzinger, Robert Nieuwenhuis, and Pilar Nivela.
Context trees.
In Goré et al. [251], pages 242-256.
[ bib ]
|
|
[253]
|
Maria Luisa Bonet, Toniann Pitassi, and Ran Raz.
On interpolation and automatization for frege systems.
SIAM J. Comput., 29(6):1939-1967, 2000.
[ bib ]
|
|
[254]
|
Maria Luisa Bonet, Juan Luis Esteban, Nicola Galesi, and Jan Johannsen.
On the relative complexity of resolution refinements and cutting
planes proof systems.
SIAM J. Comput., 30(5):1462-1484, 2000.
[ bib ]
|
|
[255]
|
Hubert Comon and Robert Nieuwenhuis.
Induction=i-axiomatization+first-order consistency.
Inf. Comput., 159(1-2):151-186, 2000.
[ bib ]
|
|
[256]
|
Guillem Godoy and Robert Nieuwenhuis.
Paramodulation with built-in abelian groups.
In LICS [257], pages 413-424.
[ bib ]
|
|
[257]
|
15th Annual IEEE Symposium on Logic in Computer Science, Santa Barbara,
California, USA, June 26-29, 2000. IEEE Computer Society, 2000.
[ bib ]
|
|
[258]
|
Miquel Bofill, Guillem Godoy, Robert Nieuwenhuis, and Albert Rubio.
Modular redundancy for theorem proving.
In Kirchner and Ringeissen [259], pages
186-199.
[ bib ]
|
|
[259]
|
Hélène Kirchner and Christophe Ringeissen, editors.
Frontiers of Combining Systems, Third International Workshop,
FroCoS 2000, Nancy, France, March 22-24, 2000, Proceedings, volume 1794 of
Lecture Notes in Computer Science. Springer, 2000.
[ bib ]
|
|
[260]
|
Sergio Díaz, Juan Luis Esteban, and Mitsunori Ogihara.
A dna-based random walk method for solving k-sat.
In Condon and Rozenberg [261], pages 209-219.
[ bib ]
|
|
[261]
|
Anne Condon and Grzegorz Rozenberg, editors.
DNA Computing, 6th International Workshop on DNA-Based
Computers, DNA 2000, Leiden, The Netherlands, June 13-17, 2000, Revised
Papers, volume 2054 of Lecture Notes in Computer Science. Springer,
2001.
[ bib ]
|
|
[262]
|
Javier Larrosa.
Boosting search with variable elimination.
In Dechter [263], pages 291-305.
[ bib ]
|
|
[263]
|
Rina Dechter, editor.
Principles and Practice of Constraint Programming - CP 2000, 6th
International Conference, Singapore, September 18-21, 2000, Proceedings,
volume 1894 of Lecture Notes in Computer Science. Springer, 2000.
[ bib ]
|
|
[264]
|
Cristina Borralleras, Maria Ferreira, and Albert Rubio.
Complete monotonic semantic path orderings.
In McAllester [265], pages 346-364.
[ bib ]
|
|
[265]
|
David A. McAllester, editor.
Automated Deduction - CADE-17, 17th International Conference on
Automated Deduction, Pittsburgh, PA, USA, June 17-20, 2000, Proceedings,
volume 1831 of Lecture Notes in Computer Science. Springer, 2000.
[ bib ]
|
|
[266]
|
Maria Luisa Bonet, Cynthia A. Phillips, Tandy Warnow, and Shibu Yooseph.
Constructing evolutionary trees in the presence of polymorphic
characters.
SIAM J. Comput., 29(1):103-131, 1999.
[ bib ]
|
|
[267]
|
Javier Larrosa, Pedro Meseguer, and Thomas Schiex.
Maintaining reversible dac for max-csp.
Artif. Intell., 107(1):149-163, 1999.
[ bib ]
|
|
[268]
|
Juan Luis Esteban and Jacobo Torán.
Space bounds for resolution.
In Meinel and Tison [269], pages 551-560.
[ bib ]
|
|
[269]
|
Christoph Meinel and Sophie Tison, editors.
STACS 99, 16th Annual Symposium on Theoretical Aspects of
Computer Science, Trier, Germany, March 4-6, 1999, Proceedings, volume 1563
of Lecture Notes in Computer Science. Springer, 1999.
[ bib ]
|
|
[270]
|
Albert Rubio.
A fully syntactic ac-rpo.
In Narendran and Rusinowitch [271], pages
133-147.
[ bib ]
|
|
[271]
|
Paliath Narendran and Michaël Rusinowitch, editors.
Rewriting Techniques and Applications, 10th International
Conference, RTA-99, Trento, Italy, July 2-4, 1999, Proceedings, volume 1631
of Lecture Notes in Computer Science. Springer, 1999.
[ bib ]
|
|
[272]
|
Robert Nieuwenhuis and José Miguel Rivero.
Solved forms for path ordering constraints.
In Narendran and Rusinowitch [271], pages 1-15.
[ bib ]
|
|
[273]
|
Jean-Pierre Jouannaud and Albert Rubio.
The higher-order recursive path ordering.
In LICS [274], pages 402-411.
[ bib ]
|
|
[274]
|
14th Annual IEEE Symposium on Logic in Computer Science, Trento, Italy,
July 2-5, 1999. IEEE Computer Society, 1999.
[ bib ]
|
|
[275]
|
Miquel Bofill, Guillem Godoy, Robert Nieuwenhuis, and Albert Rubio.
Paramodulation with non-monotonic orderings.
In LICS [274], pages 225-233.
[ bib ]
|
|
[276]
|
Maria Luisa Bonet and Nicola Galesi.
A study of proof search algorithms for resolution and polynomial
calculus.
In FOCS [277], pages 422-432.
[ bib ]
|
|
[277]
|
40th Annual Symposium on Foundations of Computer Science, FOCS '99, 17-18
October, 1999, New York, NY, USA. IEEE Computer Society, 1999.
[ bib ]
|
|
[278]
|
Javier Larrosa and Pedro Meseguer.
Partition-based lower bound for max-csp.
In Jaffar [279], pages 303-315.
[ bib ]
|
|
[279]
|
Joxan Jaffar, editor.
Principles and Practice of Constraint Programming - CP'99, 5th
International Conference, Alexandria, Virginia, USA, October 11-14, 1999,
Proceedings, volume 1713 of Lecture Notes in Computer Science.
Springer, 1999.
[ bib ]
|
|
[280]
|
Christian Bessière, Pedro Meseguer, Eugene C. Freuder, and Javier Larrosa.
On forward checking for non-binary constraint satisfaction.
In Jaffar [279], pages 88-102.
[ bib ]
|
|
[281]
|
Maria Luisa Bonet, Carlos Domingo, Ricard Gavaldà, Alexis Maciel, and
Toniann Pitassi.
Non-automatizability of bounded-depth frege proofs.
In IEEE Conference on Computational Complexity
[282], pages 15-23.
[ bib ]
|
|
[282]
|
Proceedings of the 14th Annual IEEE Conference on Computational
Complexity, Atlanta, Georgia, USA, May 4-6, 1999. IEEE Computer Society,
1999.
[ bib ]
|
|
[283]
|
Harald Ganzinger and Robert Nieuwenhuis.
Constraints and theorem proving.
In Comon et al. [284], pages 159-201.
[ bib ]
|
|
[284]
|
Hubert Comon, Claude Marché, and Ralf Treinen, editors.
Constraints in Computational Logics: Theory and Applications,
International Summer School, CCL'99 Gif-sur-Yvette, France, September 5-8,
1999, Revised Lectures, volume 2002 of Lecture Notes in Computer
Science. Springer, 2001.
[ bib ]
|
|
[285]
|
Robert Nieuwenhuis.
Invited talk: Rewrite-based deduction and symbolic constraints.
In Ganzinger [286], pages 302-313.
[ bib ]
|
|
[286]
|
Harald Ganzinger, editor.
Automated Deduction - CADE-16, 16th International Conference on
Automated Deduction, Trento, Italy, July 7-10, 1999, Proceedings, volume
1632 of Lecture Notes in Computer Science. Springer, 1999.
[ bib ]
|
|
[287]
|
Jean-Pierre Jouannaud and Albert Rubio.
Rewrite orderings for higher-order terms in eta-long beta-normal form
and recursive path ordering.
Theor. Comput. Sci., 208(1-2):33-58, 1998.
[ bib ]
|
|
[288]
|
Maria Luisa Bonet, Mike A. Steel, Tandy Warnow, and Shibu Yooseph.
Better methods for solving parsimony and compatibility.
Journal of Computational Biology, 5(3):391-407, 1998.
[ bib ]
|
|
[289]
|
Robert Nieuwenhuis.
Decidability and complexity analysis by basic paramodulation.
Inf. Comput., 147(1):1-21, 1998.
[ bib ]
|
|
[290]
|
Maria Luisa Bonet, Mike A. Steel, Tandy Warnow, and Shibu Yooseph.
Better methods for solving parsimony and compatibility.
In RECOMB, pages 40-49, 1998.
[ bib ]
|
|
[291]
|
Hubert Comon, Paliath Narendran, Robert Nieuwenhuis, and Michaël
Rusinowitch.
Decision problems in ordered rewriting.
In LICS [292], pages 276-286.
[ bib ]
|
|
[292]
|
Thirteenth Annual IEEE Symposium on Logic in Computer Science,
Indianapolis, Indiana, USA, June 21-24, 1998. IEEE Computer Society, 1998.
[ bib ]
|
|
[293]
|
Javier Larrosa and Pedro Meseguer.
Generic csp techniques for the job-shop problem.
In Pobil et al. [294], pages 46-55.
[ bib ]
|
|
[294]
|
Angel P. Del Pobil, José Mira, and Moonis Ali, editors.
Tasks and Methods in Applied Artificial Intelligence, 11th
International Conference on Industrial and Engineering Applications of
Artificial In telligence and Expert Systems, IEA/AIE-98, Castellón,
Spain, June 1-4, 1998, Proceedings, Volume II, volume 1416 of Lecture
Notes in Computer Science. Springer, 1998.
[ bib ]
|
|
[295]
|
Maria Luisa Bonet, Juan Luis Esteban, Nicola Galesi, and Jan Johannsen.
Exponential separations between restricted resolution and cutting
planes proof systems.
In FOCS [296], pages 638-647.
[ bib ]
|
|
[296]
|
39th Annual Symposium on Foundations of Computer Science, FOCS '98,
November 8-11, 1998, Palo Alto, California, USA. IEEE Computer Society,
1998.
[ bib ]
|
|
[297]
|
Javier Larrosa and Pedro Meseguer.
Partial lazy forward checking for max-csp.
In ECAI, pages 229-233, 1998.
[ bib ]
|
|
[298]
|
Javier Larrosa, Pedro Meseguer, Thomas Schiex, and Gérard Verfaillie.
Reversible dac and other improvements for solving max-csp.
In Mostow and Rich [299], pages 347-352.
[ bib ]
|
|
[299]
|
Jack Mostow and Chuck Rich, editors.
Proceedings of the Fifteenth National Conference on Artificial
Intelligence and Tenth Innovative Applications of Artificial Intelligence
Conference, AAAI 98, IAAI 98, July 26-30, 1998, Madison, Wisconsin, USA.
AAAI Press / The MIT Press, 1998.
[ bib ]
|
|
[300]
|
Maria Luisa Bonet, Toniann Pitassi, and Ran Raz.
Lower bounds for cutting planes proofs with small coefficients.
J. Symb. Log., 62(3):708-728, 1997.
[ bib ]
|
|
[301]
|
Robert Nieuwenhuis and Albert Rubio.
Paramodulation with built-in ac-theories and symbolic constraints.
J. Symb. Comput., 23(1):1-21, 1997.
[ bib ]
|
|
[302]
|
Robert Nieuwenhuis, José Miguel Rivero, and Miguel Ángel Vallejo.
Barcelona.
J. Autom. Reasoning, 18(2):171-176, 1997.
[ bib ]
|
|
[303]
|
Javier Larrosa.
Merging constraint satisfaction subproblems to avoid redundant
search.
In IJCAI (1) [304], pages 424-433.
[ bib ]
|
|
[304]
|
Proceedings of the Fifteenth International Joint Conference on Artificial
Intelligence, IJCAI 97, Nagoya, Japan, August 23-29, 1997, 2 Volumes. Morgan
Kaufmann, 1997.
[ bib ]
|
|
[305]
|
Maria Luisa Bonet, Toniann Pitassi, and Ran Raz.
No feasible interpolation for tc0-frege proofs.
In FOCS [306], pages 254-263.
[ bib ]
|
|
[306]
|
38th Annual Symposium on Foundations of Computer Science, FOCS '97, Miami
Beach, Florida, USA, October 19-22, 1997. IEEE Computer Society, 1997.
[ bib ]
|
|
[307]
|
Maria Luisa Bonet and Nicola Galesi.
Linear lower bounds and simulations in frege systems with
substitutions.
In Nielsen and Thomas [308], pages 115-128.
[ bib ]
|
|
[308]
|
Mogens Nielsen and Wolfgang Thomas, editors.
Computer Science Logic, 11th International Workshop, CSL '97,
Annual Conference of the EACSL, Aarhus, Denmark, August 23-29, 1997, Selected
Papers, volume 1414 of Lecture Notes in Computer Science. Springer,
1998.
[ bib ]
|
|
[309]
|
Robert Nieuwenhuis, José Miguel Rivero, and Miguel Ángel Vallejo.
Dedan: A kernel of data structures and algorithms for automated
deduction with equality clauses.
In McCune [310], pages 49-52.
[ bib ]
|
|
[310]
|
William McCune, editor.
Automated Deduction - CADE-14, 14th International Conference on
Automated Deduction, Townsville, North Queensland, Australia, July 13-17,
1997, Proceedings, volume 1249 of Lecture Notes in Computer Science.
Springer, 1997.
[ bib ]
|
|
[311]
|
Maria Luisa Bonet, Cynthia A. Phillips, Tandy Warnow, and Shibu Yooseph.
Constructing evolutionary trees in the presence of polymorphic
characters.
In Miller [312], pages 220-229.
[ bib ]
|
|
[312]
|
Gary L. Miller, editor.
Proceedings of the Twenty-Eighth Annual ACM Symposium on the
Theory of Computing, Philadelphia, Pennsylvania, USA, May 22-24, 1996. ACM,
1996.
[ bib ]
|
|
[313]
|
Jean-Pierre Jouannaud and Albert Rubio.
A recursive path ordering for higher-order terms in eta- long
beta-normal form.
In Ganzinger [314], pages 108-122.
[ bib ]
|
|
[314]
|
Harald Ganzinger, editor.
Rewriting Techniques and Applications, 7th International
Conference, RTA-96, New Brunswick, NJ, USA, July 27-30, 1996, Proceedings,
volume 1103 of Lecture Notes in Computer Science. Springer, 1996.
[ bib ]
|
|
[315]
|
Robert Nieuwenhuis.
Basic paramodulation and decidable theories (extended abstract).
In LICS [316], pages 473-482.
[ bib ]
|
|
[316]
|
Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, New
Brunswick, New Jersey, USA, July 27-30, 1996. IEEE Computer Society, 1996.
[ bib ]
|
|
[317]
|
Javier Larrosa and Pedro Meseguer.
Phase transition in max-csp.
In Wahlster [318], pages 190-194.
[ bib ]
|
|
[318]
|
Wolfgang Wahlster, editor.
12th European Conference on Artificial Intelligence, Budapest,
Hungary, August 11-16, 1996, Proceedings. John Wiley and Sons, Chichester,
1996.
[ bib ]
|
|
[319]
|
Javier Larrosa and Pedro Meseguer.
Exploiting the use of dac in max-csp.
In Freuder [320], pages 308-322.
[ bib ]
|
|
[320]
|
Eugene C. Freuder, editor.
Proceedings of the Second International Conference on Principles
and Practice of Constraint Programming, Cambridge, Massachusetts, USA, August
19-22, 1996, volume 1118 of Lecture Notes in Computer Science.
Springer, 1996.
[ bib ]
|
|
[321]
|
Robert Nieuwenhuis, José Miguel Rivero, and Miguel Ángel Vallejo.
An implementation kernel for theorem proving with equality clauses.
In Lucio et al. [322], pages 89-104.
[ bib ]
|
|
[322]
|
Paqui Lucio, Maurizio Martelli, and Marisa Navarro, editors.
1996 Joint Conf. on Declarative Programming, APPIA-GULP-
PRODE'96, Donostia-San Sebastian, Spain, July 15-18, 1996, 1996.
[ bib ]
|
|
[323]
|
Albert Rubio and Robert Nieuwenhuis.
A total ac-compatible ordering based on rpo.
Theor. Comput. Sci., 142(2):209-227, 1995.
[ bib ]
|
|
[324]
|
Maria Luisa Bonet and Samuel R. Buss.
The serial transitive closure problem for trees.
SIAM J. Comput., 24(1):109-122, 1995.
[ bib ]
|
|
[325]
|
Robert Nieuwenhuis and Albert Rubio.
Theorem proving with ordering and equality constrained clauses.
J. Symb. Comput., 19(4):321-351, 1995.
[ bib ]
|
|
[326]
|
Javier Larrosa and Ulises Cortés.
A framework for abductive rule formation.
AI Commun., 8(2):91-100, 1995.
[ bib ]
|
|
[327]
|
Maria Luisa Bonet, Toniann Pitassi, and Ran Raz.
Lower bounds for cutting planes proofs with small coefficients.
In Leighton and Borodin [328], pages 575-584.
[ bib ]
|
|
[328]
|
Frank Thomson Leighton and Allan Borodin, editors.
Proceedings of the Twenty-Seventh Annual ACM Symposium on Theory
of Computing, 29 May-1 June 1995, Las Vegas, Nevada, USA. ACM, 1995.
[ bib ]
|
|
[329]
|
Robert Nieuwenhuis.
On narrowing, refutation proofs and constraints.
In Hsiang [330], pages 56-70.
[ bib ]
|
|
[330]
|
Jieh Hsiang, editor.
Rewriting Techniques and Applications, 6th International
Conference, RTA-95, Kaiserslautern, Germany, April 5-7, 1995, Proceedings,
volume 914 of Lecture Notes in Computer Science. Springer, 1995.
[ bib ]
|
|
[331]
|
Hubert Comon, Robert Nieuwenhuis, and Albert Rubio.
Orderings, ac-theories and symbolic constraint solving (extended
abstract).
In LICS [332], pages 375-385.
[ bib ]
|
|
[332]
|
Proceedings, 10th Annual IEEE Symposium on Logic in Computer Science, San
Diego, California, USA, June 26-29, 1995. IEEE Computer Society, 1995.
[ bib ]
|
|
[333]
|
Pedro Meseguer and Javier Larrosa.
Constraint satisfaction as global optimization.
In IJCAI (1) [334], pages 579-585.
[ bib ]
|
|
[334]
|
Proceedings of the Fourteenth International Joint Conference on Artificial
Intelligence, IJCAI 95, Montréal Québec, Canada, August 20-25 1995, 2
Volumes. Morgan Kaufmann, 1995.
[ bib ]
|
|
[335]
|
Albert Rubio.
Extension orderings.
In Fülöp and Gécseg [336], pages
511-522.
[ bib ]
|
|
[336]
|
Zoltán Fülöp and Ferenc Gécseg, editors.
Automata, Languages and Programming, 22nd International
Colloquium, ICALP95, Szeged, Hungary, July 10-14, 1995, Proceedings, volume
944 of Lecture Notes in Computer Science. Springer, 1995.
[ bib ]
|
|
[337]
|
Albert Rubio.
Theorem proving modulo associativity.
In Büning [338], pages 452-467.
[ bib ]
|
|
[338]
|
Hans Kleine Büning, editor.
Computer Science Logic, 9th International Workshop, CSL '95,
Annual Conference of the EACSL, Paderborn, Germany, September 22-29, 1995,
Selected Papers, volume 1092 of Lecture Notes in Computer Science.
Springer, 1996.
[ bib ]
|
|
[339]
|
Javier Larrosa and Pedro Meseguer.
Optimization-based heuristics for maximal constraint satisfaction.
In Montanari and Rossi [340], pages 103-120.
[ bib ]
|
|
[340]
|
Ugo Montanari and Francesca Rossi, editors.
Principles and Practice of Constraint Programming - CP'95, First
International Conference, CP'95, Cassis, France, September 19-22, 1995,
Proceedings, volume 976 of Lecture Notes in Computer Science.
Springer, 1995.
[ bib ]
|
|
[341]
|
Maria Luisa Bonet and Samuel R. Buss.
Size-depth tradeoffs for boolean fomulae.
Inf. Process. Lett., 49(3):151-155, 1994.
[ bib ]
|
|
[342]
|
Robert Nieuwenhuis and Albert Rubio.
Ac-superposition with constraints: No ac-unifiers needed.
In Bundy [343], pages 545-559.
[ bib ]
|
|
[343]
|
Alan Bundy, editor.
Automated Deduction - CADE-12, 12th International Conference on
Automated Deduction, Nancy, France, June 26 - July 1, 1994, Proceedings,
volume 814 of Lecture Notes in Computer Science. Springer, 1994.
[ bib ]
|
|
[344]
|
Maria Luisa Bonet and Samuel R. Buss.
The deduction rule and linear and near-linear proof simulations.
J. Symb. Log., 58(2):688-709, 1993.
[ bib ]
|
|
[345]
|
Robert Nieuwenhuis.
Simple lpo constraint solving methods.
Inf. Process. Lett., 47(2):65-69, 1993.
[ bib ]
|
|
[346]
|
Albert Rubio and Robert Nieuwenhuis.
A precedence-based total ac-compatible ordering.
In Kirchner [347], pages 374-388.
[ bib ]
|
|
[347]
|
Claude Kirchner, editor.
Rewriting Techniques and Applications, 5th International
Conference, RTA-93, Montreal, Canada, June 16-18, 1993, Proceedings, volume
690 of Lecture Notes in Computer Science. Springer, 1993.
[ bib ]
|
|
[348]
|
Pilar Nivela and Robert Nieuwenhuis.
Saturation of first-order (constrained) clauses with the
saturate system.
In Kirchner [347], pages 436-440.
[ bib ]
|
|
[349]
|
Hubert Bertling, Harald Ganzinger, Renate Schäfers, Robert Nieuwenhuis, and
Fernando Orejas.
Program development: Completion subsystem.
In Hoffmann and Krieg-Brückner [350],
pages 460-494.
[ bib ]
|
|
[350]
|
Berthold Hoffmann and Bernd Krieg-Brückner, editors.
Program Development by Specification and Transformation, The
PROSPECTRA Methodology, Language Family, and System, volume 680 of
Lecture Notes in Computer Science. Springer, 1993.
[ bib ]
|
|
[351]
|
Robert Nieuwenhuis and Albert Rubio.
Basic superposition is complete.
In Krieg-Brückner [352], pages 371-389.
[ bib ]
|
|
[352]
|
Bernd Krieg-Brückner, editor.
ESOP '92, 4th European Symposium on Programming, Rennes, France,
February 26-28, 1992, Proceedings, volume 582 of Lecture Notes in
Computer Science. Springer, 1992.
[ bib ]
|
|
[353]
|
Robert Nieuwenhuis and Albert Rubio.
Theorem proving with ordering constrained clauses.
In Kapur [354], pages 477-491.
[ bib ]
|
|
[354]
|
Deepak Kapur, editor.
Automated Deduction - CADE-11, 11th International Conference on
Automated Deduction, Saratoga Springs, NY, USA, June 15-18, 1992,
Proceedings, volume 607 of Lecture Notes in Computer Science.
Springer, 1992.
[ bib ]
|
|
[355]
|
Robert Nieuwenhuis and Pilar Nivela.
Efficient deduction in equality horn logic by horn-completion.
Inf. Process. Lett., 39(1):1-6, 1991.
[ bib ]
|
|
[356]
|
Maria Luisa Bonet and Samuel R. Buss.
On the deduction rule and the number of proof lines.
In LICS [357], pages 286-297.
[ bib ]
|
|
[357]
|
Proceedings of the Sixth Annual Symposium on Logic in Computer Science
(LICS '91), Amsterdam, The Netherlands, July 15-18, 1991. IEEE Computer
Society, 1991.
[ bib ]
|
|
[358]
|
Eduardo Lleida, José B. Mariño, Climent Nadeu, and Albert Oliveras.
Two level continuous speech recognition using demisyllable-based hmm
word spotting.
In EUROSPEECH [359].
[ bib ]
|
|
[359]
|
Second European Conference on Speech Communication and Technology,
EUROSPEECH 1991, Genova, Italy, September 24-26, 1991. ISCA, 1991.
[ bib ]
|
|
[360]
|
Robert Nieuwenhuis and Fernando Orejas.
Clausal rewriting.
In Kaplan and Okada [361], pages 246-258.
[ bib ]
|
|
[361]
|
Stéphane Kaplan and Mitsuhiro Okada, editors.
Conditional and Typed Rewriting Systems, 2nd International CTRS
Workshop, Montreal, Canada, June 11-14, 1990, Proceedings, volume 516 of
Lecture Notes in Computer Science. Springer, 1991.
[ bib ]
|
|
[362]
|
Robert Nieuwenhuis, Fernando Orejas, and Albert Rubio.
Trip: An implementation of clausal rewriting.
In Stickel [363], pages 667-668.
[ bib ]
|
|
[363]
|
Mark E. Stickel, editor.
10th International Conference on Automated Deduction,
Kaiserslautern, FRG, July 24-27, 1990, Proceedings, volume 449 of
Lecture Notes in Computer Science. Springer, 1990.
[ bib ]
|
|
[364]
|
Fernando Orejas and Pilar Nivela.
Constraints for behavioural specifications.
In Ehrig et al. [365], pages 220-245.
[ bib ]
|
|
[365]
|
Hartmut Ehrig, Klaus P. Jantke, Fernando Orejas, and Horst Reichel, editors.
Recent Trends in Data Type Specification, Proceedings 7th
Workshop on Abstract Data Types, Wusterhausen, Dosse, Germany, April 17-20,
1990, volume 534 of Lecture Notes in Computer Science. Springer, 1991.
[ bib ]
|
|
[366]
|
Robert Nieuwenhuis and Fernando Orejas.
Clausal rewriting: Applications and implementation.
In Ehrig et al. [365], pages 204-219.
[ bib ]
|
|
[367]
|
Fernando Orejas, Pilar Nivela, and Hartmut Ehrig.
Semantical constructions for categories of behavioural
specifications.
In Ehrig et al. [368], pages 220-243.
[ bib ]
|
|
[368]
|
Hartmut Ehrig, Horst Herrlich, Hans-Jörg Kreowski, and Gerhard Preuß,
editors.
Categorial Methods in Computer Science: With Aspects from
Topology [Workshop, September 1988, Berlin, Germany], volume 393 of
Lecture Notes in Computer Science. Springer, 1989.
[ bib ]
|
|
[369]
|
Fernando Orejas, Ana Sánchez, Marisa Navarro, Pilar Nivela, and Ricardo
Pena.
Term rewriting methods for partial specifications.
In ADT, 1988.
[ bib ]
|
|
[370]
|
Pilar Nivela and Fernando Orejas.
A module concept within the initial behaviour framework.
In ADT, 1988.
[ bib ]
|
|
[371]
|
Pilar Nivela and Fernando Orejas.
Initial behaviour semantics for algebraic specifications.
In Sannella and Tarlecki [372], pages 184-207.
[ bib ]
|
|
[372]
|
Donald Sannella and Andrzej Tarlecki, editors.
Recent Trends in Data Type Specification, 5th Workshop on
Abstract Data Types, Gullane, Scotland, September 1-4, 1987, Selected
Papers, volume 332 of Lecture Notes in Computer Science. Springer,
1987.
[ bib ]
|
|
[373]
|
Juan Luis Esteban and Jacobo Torán.
A combinatorial characterization of treelike resolution space.
Electronic Colloquium on Computational Complexity (ECCC),
(044), 2003.
[ bib ]
|
|
[374]
|
Albert Atserias, Maria Luisa Bonet, and Jordi Levy.
On chvatal rank and cutting planes proofs.
Electronic Colloquium on Computational Complexity (ECCC),
(041), 2003.
[ bib ]
|
|
[375]
|
Javier Larrosa and Pedro Meseguer.
Restricciones blanda: Modelos y algoritmos.
Inteligencia Artificial, Revista Iberoamericana de Inteligencia
Artificial, 7(20):69-82, 2003.
[ bib ]
|
|
[376]
|
Maria Luisa Bonet, Juan Luis Esteban, Nicola Galesi, and Jan Johannsen.
Exponential separations between restricted resolution and cutting
planes proof systems.
Electronic Colloquium on Computational Complexity (ECCC),
5(35), 1998.
[ bib ]
|
This file was generated by
bibtex2html 1.96.
|
|