@article{DBLP:journals/logcom/BofillBRR13,
author = {Miquel Bofill and
Cristina Borralleras and
Enric Rodr\'{\i}guez-Carbonell and
Albert Rubio},
title = {The recursive path and polynomial ordering for first-order
and higher-order terms},
journal = {J. Log. Comput.},
volume = {23},
number = {1},
year = {2013},
pages = {263-305},
ee = {http://dx.doi.org/10.1093/logcom/exs027},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/jar/BofillR13,
author = {Miquel Bofill and
Albert Rubio},
title = {Paramodulation with Non-Monotonic Orderings and Simplification},
journal = {J. Autom. Reasoning},
volume = {50},
number = {1},
year = {2013},
pages = {51-98},
ee = {http://dx.doi.org/10.1007/s10817-011-9244-z},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/jar/BarrettDMOS13,
author = {Clark Barrett and
Morgan Deters and
Leonardo Mendon\c{c}a de Moura and
Albert Oliveras and
Aaron Stump},
title = {6 Years of SMT-COMP},
journal = {J. Autom. Reasoning},
volume = {50},
number = {3},
year = {2013},
pages = {243-277},
ee = {http://dx.doi.org/10.1007/s10817-012-9246-5},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/isci/AnsoteguiBLM13,
author = {Carlos Ans{\'o}tegui and
Maria Luisa Bonet and
Jordi Levy and
Felip Many{\`a}},
title = {Resolution procedures for multiple-valued optimization},
journal = {Inf. Sci.},
volume = {227},
year = {2013},
pages = {43-59},
ee = {http://dx.doi.org/10.1016/j.ins.2012.12.004},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/ai/AnsoteguiBL13,
author = {Carlos Ans{\'o}tegui and
Maria Luisa Bonet and
Jordi Levy},
title = {SAT-based MaxSAT algorithms},
journal = {Artif. Intell.},
volume = {196},
year = {2013},
pages = {77-105},
ee = {http://dx.doi.org/10.1016/j.artint.2013.01.002},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/vmcai/LarrazRR13,
author = {Daniel Larraz and
Enric Rodr\'{\i}guez-Carbonell and
Albert Rubio},
title = {SMT-Based Array Invariant Generation},
booktitle = {VMCAI},
year = {2013},
pages = {169-188},
ee = {http://dx.doi.org/10.1007/978-3-642-35873-9_12},
crossref = {DBLP:conf/vmcai/2013},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/vmcai/2013,
editor = {Roberto Giacobazzi and
Josh Berdine and
Isabella Mastroeni},
title = {Verification, Model Checking, and Abstract Interpretation,
14th International Conference, VMCAI 2013, Rome, Italy,
January 20-22, 2013. Proceedings},
booktitle = {VMCAI},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {7737},
year = {2013},
isbn = {978-3-642-35872-2, 978-3-642-35873-9},
ee = {http://dx.doi.org/10.1007/978-3-642-35873-9},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/sac/LarrosaR13,
author = {Javier Larrosa and
Emma Rollon},
title = {Risk-neutral bounded max-sum for distributed constraint
optimization},
booktitle = {SAC},
year = {2013},
pages = {92-97},
ee = {http://doi.acm.org/10.1145/2480362.2480383},
crossref = {DBLP:conf/sac/2013},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/sac/2013,
editor = {Sung Y. Shin and
Jos{\'e} Carlos Maldonado},
title = {Proceedings of the 28th Annual ACM Symposium on Applied
Computing, SAC '13, Coimbra, Portugal, March 18-22, 2013},
booktitle = {SAC},
publisher = {ACM},
year = {2013},
isbn = {978-1-4503-1656-9},
ee = {http://dl.acm.org/citation.cfm?id=2480362},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/ijcai/RollonLD13,
author = {Emma Rollon and
Javier Larrosa and
Rina Dechter},
title = {Semiring-Based Mini-Bucket Partitioning Schemes},
booktitle = {IJCAI},
year = {2013},
ee = {http://www.aaai.org/ocs/index.php/IJCAI/IJCAI13/paper/view/
6818},
crossref = {DBLP:conf/ijcai/2013},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/ijcai/BonetB13,
author = {Maria Luisa Bonet and
Sam Buss},
title = {An Improved Separation of Regular Resolution from Pool
Resolution
and Clause Learning (Extended Abstract)},
booktitle = {IJCAI},
year = {2013},
ee = {http://www.aaai.org/ocs/index.php/IJCAI/IJCAI13/paper/view/
6768},
crossref = {DBLP:conf/ijcai/2013},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/ijcai/2013,
editor = {Francesca Rossi},
title = {IJCAI 2013, Proceedings of the 23rd International Joint
Conference on Artificial Intelligence, Beijing, China, August
3-9, 2013},
booktitle = {IJCAI},
publisher = {IJCAI/AAAI},
year = {2013},
isbn = {978-1-57735-633-2},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/cp/AnsoteguiBGL13,
author = {Carlos Ans{\'o}tegui and
Maria Luisa Bonet and
Joel Gab{\`a}s and
Jordi Levy},
title = {Improving WPM2 for (Weighted) Partial MaxSAT},
booktitle = {CP},
year = {2013},
pages = {117-132},
ee = {http://dx.doi.org/10.1007/978-3-642-40627-0_12},
crossref = {DBLP:conf/cp/2013},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/cp/AbioNORS13,
author = {Ignasi Ab\'{\i}o and
Robert Nieuwenhuis and
Albert Oliveras and
Enric Rodr\'{\i}guez-Carbonell and
Peter J. Stuckey},
title = {To Encode or to Propagate? The Best Choice for Each Constraint
in SAT},
booktitle = {CP},
year = {2013},
pages = {97-106},
ee = {http://dx.doi.org/10.1007/978-3-642-40627-0_10},
crossref = {DBLP:conf/cp/2013},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/cp/2013,
editor = {Christian Schulte},
title = {Principles and Practice of Constraint Programming - 19th
International Conference, CP 2013, Uppsala, Sweden, September
16-20, 2013. Proceedings},
booktitle = {CP},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {8124},
year = {2013},
isbn = {978-3-642-40626-3},
ee = {http://dx.doi.org/10.1007/978-3-642-40627-0},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/cp/AbioNOR13,
author = {Ignasi Ab\'{\i}o and
Robert Nieuwenhuis and
Albert Oliveras and
Enric Rodr\'{\i}guez-Carbonell},
title = {A Parametric Approach for Smaller and Better Encodings of
Cardinality Constraints},
booktitle = {CP},
year = {2013},
pages = {80-96},
ee = {http://dx.doi.org/10.1007/978-3-642-40627-0_9},
crossref = {DBLP:conf/cp/2013},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/birthday/KapurNVWW13,
author = {Deepak Kapur and
Robert Nieuwenhuis and
Andrei Voronkov and
Christoph Weidenbach and
Reinhard Wilhelm},
title = {Harald Ganzinger's Legacy: Contributions to Logics and
Programming},
booktitle = {Programming Logics},
year = {2013},
pages = {1-18},
ee = {http://dx.doi.org/10.1007/978-3-642-37651-1_1},
crossref = {DBLP:conf/birthday/2013ganzinger},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/birthday/2013ganzinger,
editor = {Andrei Voronkov and
Christoph Weidenbach},
title = {Programming Logics - Essays in Memory of Harald Ganzinger},
booktitle = {Programming Logics},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {7797},
year = {2013},
isbn = {978-3-642-37650-4},
ee = {http://dx.doi.org/10.1007/978-3-642-37651-1},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/tcbb/BonetLJ12,
author = {Maria Luisa Bonet and
Simone Linz and
Katherine St. John},
title = {The Complexity of Finding Multiple Solutions to Betweenness
and Quartet Compatibility},
journal = {IEEE/ACM Trans. Comput. Biology Bioinform.},
volume = {9},
number = {1},
year = {2012},
pages = {273-285},
ee = {http://doi.ieeecomputersociety.org/10.1109/TCBB.2011.108},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/jar/BorrallerasLORR12,
author = {Cristina Borralleras and
Salvador Lucas and
Albert Oliveras and
Enric Rodr\'{\i}guez-Carbonell and
Albert Rubio},
title = {SAT Modulo Linear Arithmetic for Solving Polynomial
Constraints},
journal = {J. Autom. Reasoning},
volume = {48},
number = {1},
year = {2012},
pages = {107-131},
ee = {http://dx.doi.org/10.1007/s10817-010-9196-8},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/jair/AbioNORM12,
author = {Ignasi Ab\'{\i}o and
Robert Nieuwenhuis and
Albert Oliveras and
Enric Rodr\'{\i}guez-Carbonell and
Valentin Mayer-Eichberger},
title = {A New Look at BDDs for Pseudo-Boolean Constraints},
journal = {J. Artif. Intell. Res. (JAIR)},
volume = {45},
year = {2012},
pages = {443-480},
ee = {http://dx.doi.org/10.1613/jair.3653},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/eswa/BistarelliGLRS12,
author = {Stefano Bistarelli and
Fabio Gadducci and
Javier Larrosa and
Emma Rollon and
Francesco Santini},
title = {Local arc consistency for non-invertible semirings, with
an application to multi-objective optimization},
journal = {Expert Syst. Appl.},
volume = {39},
number = {2},
year = {2012},
pages = {1708-1717},
ee = {http://dx.doi.org/10.1016/j.eswa.2011.06.062},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/sat/BonetB12,
author = {Maria Luisa Bonet and
Samuel R. Buss},
title = {An Improved Separation of Regular Resolution from Pool
Resolution
and Clause Learning},
booktitle = {SAT},
year = {2012},
pages = {44-57},
ee = {http://dx.doi.org/10.1007/978-3-642-31612-8_5},
crossref = {DBLP:conf/sat/2012},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/sat/2012,
editor = {Alessandro Cimatti and
Roberto Sebastiani},
title = {Theory and Applications of Satisfiability Testing - SAT
2012 - 15th International Conference, Trento, Italy, June
17-20, 2012. Proceedings},
booktitle = {SAT},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {7317},
year = {2012},
isbn = {978-3-642-31611-1},
ee = {http://dx.doi.org/10.1007/978-3-642-31612-8},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/icalp/FernandezR12,
author = {Maribel Fern{\'a}ndez and
Albert Rubio},
title = {Nominal Completion for Rewrite Systems with Binders},
booktitle = {ICALP (2)},
year = {2012},
pages = {201-213},
ee = {http://dx.doi.org/10.1007/978-3-642-31585-5_21},
crossref = {DBLP:conf/icalp/2012-2},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/icalp/2012-2,
editor = {Artur Czumaj and
Kurt Mehlhorn and
Andrew M. Pitts and
Roger Wattenhofer},
title = {Automata, Languages, and Programming - 39th International
Colloquium, ICALP 2012, Warwick, UK, July 9-13, 2012,
Proceedings,
Part II},
booktitle = {ICALP (2)},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {7392},
year = {2012},
isbn = {978-3-642-31584-8},
ee = {http://dx.doi.org/10.1007/978-3-642-31585-5},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/cp/RollonL12,
author = {Emma Rollon and
Javier Larrosa},
title = {Improved Bounded Max-Sum for Distributed Constraint
Optimization},
booktitle = {CP},
year = {2012},
pages = {624-632},
ee = {http://dx.doi.org/10.1007/978-3-642-33558-7_45},
crossref = {DBLP:conf/cp/2012},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/cp/AnsoteguiBGL12,
author = {Carlos Ans{\'o}tegui and
Maria Luisa Bonet and
Joel Gab{\`a}s and
Jordi Levy},
title = {Improving SAT-Based Weighted MaxSAT Solvers},
booktitle = {CP},
year = {2012},
pages = {86-101},
ee = {http://dx.doi.org/10.1007/978-3-642-33558-7_9},
crossref = {DBLP:conf/cp/2012},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/cp/2012,
editor = {Michela Milano},
title = {Principles and Practice of Constraint Programming - 18th
International Conference, CP 2012, Qu{\'e}bec City, QC,
Canada, October 8-12, 2012. Proceedings},
booktitle = {CP},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {7514},
year = {2012},
isbn = {978-3-642-33557-0},
ee = {http://dx.doi.org/10.1007/978-3-642-33558-7},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/ccia/AnsoteguiBLL12,
author = {Carlos Ans{\'o}tegui and
Maria Luisa Bonet and
Jordi Levy and
Chu Min Li},
title = {Analysis and Generation of Pseudo-Industrial MaxSAT Instances},
booktitle = {CCIA},
year = {2012},
pages = {173-184},
ee = {http://dx.doi.org/10.3233/978-1-61499-139-7-173},
crossref = {DBLP:conf/ccia/2012},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/ccia/2012,
editor = {David Ria{\~n}o and
Eva Onaindia and
Miguel Cazorla},
title = {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},
booktitle = {CCIA},
publisher = {IOS Press},
series = {Frontiers in Artificial Intelligence and Applications},
volume = {248},
year = {2012},
isbn = {978-1-61499-138-0},
ee = {http://www.booksonline.iospress.nl/Content/
View.aspx?piid=32596},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/cade/Nieuwenhuis12,
author = {Robert Nieuwenhuis},
title = {SAT and SMT Are Still Resolution: Questions and Challenges},
booktitle = {IJCAR},
year = {2012},
pages = {10-13},
ee = {http://dx.doi.org/10.1007/978-3-642-31365-3_3},
crossref = {DBLP:conf/cade/2012},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/cade/2012,
editor = {Bernhard Gramlich and
Dale Miller and
Uli Sattler},
title = {Automated Reasoning - 6th International Joint Conference,
IJCAR 2012, Manchester, UK, June 26-29, 2012. Proceedings},
booktitle = {IJCAR},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {7364},
year = {2012},
isbn = {978-3-642-31364-6},
ee = {http://dx.doi.org/10.1007/978-3-642-31365-3},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/jar/LarrosaNOR11,
author = {Javier Larrosa and
Robert Nieuwenhuis and
Albert Oliveras and
Enric Rodr\'{\i}guez-Carbonell},
title = {A Framework for Certified Boolean Branch-and-Bound
Optimization},
journal = {J. Autom. Reasoning},
volume = {46},
number = {1},
year = {2011},
pages = {81-102},
ee = {http://dx.doi.org/10.1007/s10817-010-9176-z},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/dagstuhl-reports/BjornerNVV11,
author = {Nikolaj Bj{\o}rner and
Robert Nieuwenhuis and
Helmut Veith and
Andrei Voronkov},
title = {Decision Procedures in Soft, Hard and Bio-ware - Follow
Up (Dagstuhl Seminar 11272)},
journal = {Dagstuhl Reports},
volume = {1},
number = {7},
year = {2011},
pages = {23-35},
ee = {http://dx.doi.org/10.4230/DagRep.1.7.23},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/constraints/AsinNOR11,
author = {Roberto As\'{\i}n and
Robert Nieuwenhuis and
Albert Oliveras and
Enric Rodr\'{\i}guez-Carbonell},
title = {Cardinality Networks: a theoretical and empirical study},
journal = {Constraints},
volume = {16},
number = {2},
year = {2011},
pages = {195-221},
ee = {http://dx.doi.org/10.1007/s10601-010-9105-0},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/sat/AbioNOR11,
author = {Ignasi Ab\'{\i}o and
Robert Nieuwenhuis and
Albert Oliveras and
Enric Rodr\'{\i}guez-Carbonell},
title = {BDDs for Pseudo-Boolean Constraints - Revisited},
booktitle = {SAT},
year = {2011},
pages = {61-75},
ee = {http://dx.doi.org/10.1007/978-3-642-21581-0_7},
crossref = {DBLP:conf/sat/2011},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/sat/AbioDNS11,
author = {Ignasi Ab\'{\i}o and
Morgan Deters and
Robert Nieuwenhuis and
Peter J. Stuckey},
title = {Reducing Chaos in SAT-Like Search: Finding Solutions Close
to a Given One},
booktitle = {SAT},
year = {2011},
pages = {273-286},
ee = {http://dx.doi.org/10.1007/978-3-642-21581-0_22},
crossref = {DBLP:conf/sat/2011},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/sat/2011,
editor = {Karem A. Sakallah and
Laurent Simon},
title = {Theory and Applications of Satisfiability Testing - SAT
2011 - 14th International Conference, SAT 2011, Ann Arbor,
MI, USA, June 19-22, 2011. Proceedings},
booktitle = {SAT},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {6695},
year = {2011},
isbn = {978-3-642-21580-3},
ee = {http://dx.doi.org/10.1007/978-3-642-21581-0},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/gkr/FlerovaRD11,
author = {Natalia Flerova and
Emma Rollon and
Rina Dechter},
title = {Bucket and Mini-bucket Schemes for M Best Solutions over
Graphical Models},
booktitle = {GKR},
year = {2011},
pages = {91-118},
ee = {http://dx.doi.org/10.1007/978-3-642-29449-5_4},
crossref = {DBLP:conf/gkr/2012},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/gkr/2012,
editor = {Madalina Croitoru and
Sebastian Rudolph and
Nic Wilson and
John Howse and
Olivier Corby},
title = {Graph Structures for Knowledge Representation and Reasoning
- Second International Workshop, GKR 2011, Barcelona, Spain,
July 16, 2011. Revised Selected Papers},
booktitle = {GKR},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {7205},
year = {2012},
isbn = {978-3-642-29448-8},
ee = {http://dx.doi.org/10.1007/978-3-642-29449-5},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/cp/RollonL11,
author = {Emma Rollon and
Javier Larrosa},
title = {On Mini-Buckets and the Min-fill Elimination Ordering},
booktitle = {CP},
year = {2011},
pages = {759-773},
ee = {http://dx.doi.org/10.1007/978-3-642-23786-7_57},
crossref = {DBLP:conf/cp/2011},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/cp/2011,
editor = {Jimmy Ho-Man Lee},
title = {Principles and Practice of Constraint Programming - CP 2011
- 17th International Conference, CP 2011, Perugia, Italy,
September 12-16, 2011. Proceedings},
booktitle = {CP},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {6876},
year = {2011},
isbn = {978-3-642-23785-0},
ee = {http://dx.doi.org/10.1007/978-3-642-23786-7},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/tcbb/BonetJ10,
author = {Maria Luisa Bonet and
Katherine St. John},
title = {On the Complexity of uSPR Distance},
journal = {IEEE/ACM Trans. Comput. Biology Bioinform.},
volume = {7},
number = {3},
year = {2010},
pages = {572-576},
ee = {http://doi.acm.org/10.1145/1843144.1843160},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/jair/BidyukDR10,
author = {Bozhena Bidyuk and
Rina Dechter and
Emma Rollon},
title = {Active Tuples-based Scheme for Bounding Posterior Beliefs},
journal = {J. Artif. Intell. Res. (JAIR)},
volume = {39},
year = {2010},
pages = {335-371},
ee = {http://dx.doi.org/10.1613/jair.2945},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/ipl/BezemNR10,
author = {Marc Bezem and
Robert Nieuwenhuis and
Enric Rodr\'{\i}guez-Carbonell},
title = {Hard problems in max-algebra, control theory, hypergraphs
and other areas},
journal = {Inf. Process. Lett.},
volume = {110},
number = {4},
year = {2010},
pages = {133-138},
ee = {http://dx.doi.org/10.1016/j.ipl.2009.11.007},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/entcs/MineR10,
author = {Antoine Min{\'e} and
Enric Rodr\'{\i}guez-Carbonell},
title = {Preface},
journal = {Electr. Notes Theor. Comput. Sci.},
volume = {267},
number = {1},
year = {2010},
pages = {1-2},
ee = {http://dx.doi.org/10.1016/j.entcs.2010.09.001},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/eccc/ECCC-TR02-010,
author = {Albert Atserias and
Maria Luisa Bonet},
title = {On the Automatizability of Resolution and Related Propositional
Proof Systems},
journal = {Electronic Colloquium on Computational Complexity (ECCC)},
number = {010},
year = {2002},
ee = {http://eccc.hpi-web.de/eccc-reports/2002/TR02-010/index.html},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/constraints/FargierRW10,
author = {H{\'e}l{\`e}ne Fargier and
Emma Rollon and
Nic Wilson},
title = {Enabling local computation for partially ordered preferences},
journal = {Constraints},
volume = {15},
number = {4},
year = {2010},
pages = {516-539},
ee = {http://dx.doi.org/10.1007/s10601-010-9094-z},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/aicom/AchaNOR10,
author = {Roberto Javier As\'{\i}n Ach{\'a} and
Robert Nieuwenhuis and
Albert Oliveras and
Enric Rodr\'{\i}guez-Carbonell},
title = {Practical algorithms for unsatisfiability proof and core
generation in SAT solvers},
journal = {AI Commun.},
volume = {23},
number = {2-3},
year = {2010},
pages = {145-157},
ee = {http://dx.doi.org/10.3233/AIC-2010-0462},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/micai/BistarelliGLRS10,
author = {Stefano Bistarelli and
Fabio Gadducci and
Javier Larrosa and
Emma Rollon and
Francesco Santini},
title = {Extending Soft Arc Consistency Algorithms to Non-invertible
Semirings},
booktitle = {MICAI (1)},
year = {2010},
pages = {386-398},
ee = {http://dx.doi.org/10.1007/978-3-642-16761-4_34},
crossref = {DBLP:conf/micai/2010-1},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/micai/2010-1,
editor = {Grigori Sidorov and
Arturo Hern{\'a}ndez Aguirre and
Carlos A. Reyes Garc\'{\i}a},
title = {Advances in Artificial Intelligence - 9th Mexican International
Conference on Artificial Intelligence, MICAI 2010, Pachuca,
Mexico, November 8-13, 2010, Proceedings, Part I},
booktitle = {MICAI (1)},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {6437},
year = {2010},
isbn = {978-3-642-16760-7},
ee = {http://dx.doi.org/10.1007/978-3-642-16761-4},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/lpar/LarrosaOR10,
author = {Javier Larrosa and
Albert Oliveras and
Enric Rodr\'{\i}guez-Carbonell},
title = {Semiring-Induced Propositional Logic: Definition and Basic
Algorithms},
booktitle = {LPAR (Dakar)},
year = {2010},
pages = {332-347},
ee = {http://dx.doi.org/10.1007/978-3-642-17511-4_19},
crossref = {DBLP:conf/lpar/2010d},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/lpar/2010d,
editor = {Edmund M. Clarke and
Andrei Voronkov},
title = {Logic for Programming, Artificial Intelligence, and Reasoning
- 16th International Conference, LPAR-16, Dakar, Senegal,
April 25-May 1, 2010, Revised Selected Papers},
booktitle = {LPAR (Dakar)},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {6355},
year = {2010},
isbn = {978-3-642-17510-7},
ee = {http://dx.doi.org/10.1007/978-3-642-17511-4},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/isaim/RollonD10,
author = {Emma Rollon and
Rina Dechter},
title = {Evaluating partition strategies for mini-bucket elimination},
booktitle = {ISAIM},
year = {2010},
ee = {http://gauss.ececs.uc.edu/Workshops/isaim2010/papers/
rollon.pdf},
crossref = {DBLP:conf/isaim/2010},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/isaim/2010,
title = {International Symposium on Artificial Intelligence and
Mathematics
(ISAIM 2010), Fort Lauderdale, Florida, USA, January 6-8,
2010},
booktitle = {ISAIM},
year = {2010},
ee = {http://gauss.ececs.uc.edu/Workshops/isaim2010/proceedings.html},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/cp/Nieuwenhuis10,
author = {Robert Nieuwenhuis},
title = {SAT Modulo Theories: Getting the Best of SAT and Global
Constraint Filtering},
booktitle = {CP},
year = {2010},
pages = {1-2},
ee = {http://dx.doi.org/10.1007/978-3-642-15396-9_1},
crossref = {DBLP:conf/cp/2010},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/cp/2010,
editor = {David Cohen},
title = {Principles and Practice of Constraint Programming - CP 2010
- 16th International Conference, CP 2010, St. Andrews, Scotland,
UK, September 6-10, 2010. Proceedings},
booktitle = {CP},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {6308},
year = {2010},
isbn = {978-3-642-15395-2},
ee = {http://dx.doi.org/10.1007/978-3-642-15396-9},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/aaai/RollonD10,
author = {Emma Rollon and
Rina Dechter},
title = {New Mini-Bucket Partitioning Heuristics for Bounding the
Probability of Evidence},
booktitle = {AAAI},
year = {2010},
ee = {http://www.aaai.org/ocs/index.php/AAAI/AAAI10/paper/view/1891},
crossref = {DBLP:conf/aaai/2010},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/aaai/AnsoteguiBL10,
author = {Carlos Ans{\'o}tegui and
Maria Luisa Bonet and
Jordi Levy},
title = {A New Algorithm for Weighted Partial MaxSAT},
booktitle = {AAAI},
year = {2010},
ee = {http://www.aaai.org/ocs/index.php/AAAI/AAAI10/paper/view/1774},
crossref = {DBLP:conf/aaai/2010},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/aaai/2010,
editor = {Maria Fox and
David Poole},
title = {Proceedings of the Twenty-Fourth AAAI Conference on Artificial
Intelligence, AAAI 2010, Atlanta, Georgia, USA, July 11-15,
2010},
booktitle = {AAAI},
publisher = {AAAI Press},
year = {2010},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/logcom/BofillR09,
author = {Miquel Bofill and
Albert Rubio},
title = {Paramodulation with Well-founded Orderings},
journal = {J. Log. Comput.},
volume = {19},
number = {2},
year = {2009},
pages = {263-302},
ee = {http://dx.doi.org/10.1093/logcom/exn073},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/sat/Nieuwenhuis09,
author = {Robert Nieuwenhuis},
title = {SAT Modulo Theories: Enhancing SAT with Special-Purpose
Algorithms},
booktitle = {SAT},
year = {2009},
pages = {1},
ee = {http://dx.doi.org/10.1007/978-3-642-02777-2_1},
crossref = {DBLP:conf/sat/2009},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/sat/LarrosaNOR09,
author = {Javier Larrosa and
Robert Nieuwenhuis and
Albert Oliveras and
Enric Rodr\'{\i}guez-Carbonell},
title = {Branch and Bound for Boolean Optimization and the Generation
of Optimality Certificates},
booktitle = {SAT},
year = {2009},
pages = {453-466},
ee = {http://dx.doi.org/10.1007/978-3-642-02777-2_42},
crossref = {DBLP:conf/sat/2009},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/sat/2009,
editor = {Oliver Kullmann},
title = {Theory and Applications of Satisfiability Testing - SAT
2009, 12th International Conference, SAT 2009, Swansea,
UK, June 30 - July 3, 2009. Proceedings},
booktitle = {SAT},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {5584},
year = {2009},
isbn = {978-3-642-02776-5},
ee = {http://dx.doi.org/10.1007/978-3-642-02777-2},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/sat/BonetJ09,
author = {Maria Luisa Bonet and
Katherine St. John},
title = {Efficiently Calculating Evolutionary Tree Measures Using
SAT},
booktitle = {SAT},
year = {2009},
pages = {4-17},
ee = {http://dx.doi.org/10.1007/978-3-642-02777-2_3},
crossref = {DBLP:conf/sat/2009},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/sat/AsinNOR09,
author = {Roberto As\'{\i}n and
Robert Nieuwenhuis and
Albert Oliveras and
Enric Rodr\'{\i}guez-Carbonell},
title = {Cardinality Networks and Their Applications},
booktitle = {SAT},
year = {2009},
pages = {167-180},
ee = {http://dx.doi.org/10.1007/978-3-642-02777-2_18},
crossref = {DBLP:conf/sat/2009},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/sat/AnsoteguiBL09,
author = {Carlos Ans{\'o}tegui and
Maria Luisa Bonet and
Jordi Levy},
title = {Solving (Weighted) Partial MaxSAT through Satisfiability
Testing},
booktitle = {SAT},
year = {2009},
pages = {427-440},
ee = {http://dx.doi.org/10.1007/978-3-642-02777-2_39},
crossref = {DBLP:conf/sat/2009},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/ijcai/AnsoteguiBL09,
author = {Carlos Ans{\'o}tegui and
Maria Luisa Bonet and
Jordi Levy},
title = {Towards Industrial-Like Random SAT Instances},
booktitle = {IJCAI},
year = {2009},
pages = {387-392},
ee = {http://ijcai.org/papers09/Papers/IJCAI09-072.pdf},
crossref = {DBLP:conf/ijcai/2009},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/ijcai/2009,
editor = {Craig Boutilier},
title = {IJCAI 2009, Proceedings of the 21st International Joint
Conference on Artificial Intelligence, Pasadena, California,
USA, July 11-17, 2009},
booktitle = {IJCAI},
year = {2009},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/csclp/2009,
editor = {Javier Larrosa and
Barry O'Sullivan},
title = {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},
booktitle = {CSCLP},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {6384},
year = {2011},
isbn = {978-3-642-19485-6},
ee = {http://dx.doi.org/10.1007/978-3-642-19486-3},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/cp/AnsoteguiBL09,
author = {Carlos Ans{\'o}tegui and
Maria Luisa Bonet and
Jordi Levy},
title = {On the Structure of Industrial SAT Instances},
booktitle = {CP},
year = {2009},
pages = {127-141},
ee = {http://dx.doi.org/10.1007/978-3-642-04244-7_13},
crossref = {DBLP:conf/cp/2009},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/cp/2009,
editor = {Ian P. Gent},
title = {Principles and Practice of Constraint Programming - CP 2009,
15th International Conference, CP 2009, Lisbon, Portugal,
September 20-24, 2009, Proceedings},
booktitle = {CP},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {5732},
year = {2009},
isbn = {978-3-642-04243-0},
ee = {http://dx.doi.org/10.1007/978-3-642-04244-7},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/ccia/AnsoteguiBL09,
author = {Carlos Ans{\'o}tegui and
Maria Luisa Bonet and
Jordi Levy},
title = {On Solving MaxSAT Through SAT},
booktitle = {CCIA},
year = {2009},
pages = {284-292},
ee = {http://dx.doi.org/10.3233/978-1-60750-061-2-284},
crossref = {DBLP:conf/ccia/2009},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/ccia/2009,
editor = {Sandra Sandri and
Miquel S{\`a}nchez-Marr{\`e} and
Ulises Cort{\'e}s},
title = {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},
booktitle = {CCIA},
publisher = {IOS Press},
series = {Frontiers in Artificial Intelligence and Applications},
volume = {202},
year = {2009},
isbn = {978-1-60750-061-2},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/cade/BorrallerasLNRR09,
author = {Cristina Borralleras and
Salvador Lucas and
Rafael Navarro-Marset and
Enric Rodr\'{\i}guez-Carbonell and
Albert Rubio},
title = {Solving Non-linear Polynomial Arithmetic via SAT Modulo
Linear Arithmetic},
booktitle = {CADE},
year = {2009},
pages = {294-305},
ee = {http://dx.doi.org/10.1007/978-3-642-02959-2_23},
crossref = {DBLP:conf/cade/2009},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/cade/2009,
editor = {Renate A. Schmidt},
title = {Automated Deduction - CADE-22, 22nd International Conference
on Automated Deduction, Montreal, Canada, August 2-7, 2009.
Proceedings},
booktitle = {CADE},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {5663},
year = {2009},
isbn = {978-3-642-02958-5},
ee = {http://dx.doi.org/10.1007/978-3-642-02959-2},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/jsat/HerasLGS08,
author = {Federico Heras and
Javier Larrosa and
Simon de Givry and
Thomas Schiex},
title = {2006 and 2007 Max-SAT Evaluations: Contributed Instances},
journal = {JSAT},
volume = {4},
number = {2-4},
year = {2008},
pages = {239-250},
ee = {http://jsat.ewi.tudelft.nl/content/volume4/JSAT4_12_Heras.pdf},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/jair/HerasLO08,
author = {Federico Heras and
Javier Larrosa and
Albert Oliveras},
title = {MiniMaxSAT: An Efficient Weighted Max-SAT solver},
journal = {J. Artif. Intell. Res. (JAIR)},
volume = {31},
year = {2008},
pages = {1-32},
ee = {http://dx.doi.org/10.1613/jair.2347},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/ijait/BarrettDOS08,
author = {Clark Barrett and
Morgan Deters and
Albert Oliveras and
Aaron Stump},
title = {Design and Results of the 3rd Annual Satisfiability Modulo
Theories Competition (SMT-Comp 2007)},
journal = {International Journal on Artificial Intelligence Tools},
volume = {17},
number = {4},
year = {2008},
pages = {569-606},
ee = {http://dx.doi.org/10.1142/S0218213008004060},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/entcs/KrsticO08,
author = {Sava Krstic and
Albert Oliveras},
title = {Preface},
journal = {Electr. Notes Theor. Comput. Sci.},
volume = {198},
number = {2},
year = {2008},
pages = {1-2},
ee = {http://dx.doi.org/10.1016/j.entcs.2008.04.076},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/dam/BezemNR08,
author = {Marc Bezem and
Robert Nieuwenhuis and
Enric Rodr\'{\i}guez-Carbonell},
title = {Exponential behaviour of the Butkovic-Zimmermann algorithm
for solving two-sided linear systems in max-algebra},
journal = {Discrete Applied Mathematics},
volume = {156},
number = {18},
year = {2008},
pages = {3506-3509},
ee = {http://dx.doi.org/10.1016/j.dam.2008.03.016},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/ai/LarrosaHG08,
author = {Javier Larrosa and
Federico Heras and
Simon de Givry},
title = {A logical approach to efficient Max-SAT solving},
journal = {Artif. Intell.},
volume = {172},
number = {2-3},
year = {2008},
pages = {204-233},
ee = {http://dx.doi.org/10.1016/j.artint.2007.05.006},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/sat/HerasL08,
author = {Federico Heras and
Javier Larrosa},
title = {A Max-SAT Inference-Based Pre-processing for Max-Clique},
booktitle = {SAT},
year = {2008},
pages = {139-152},
ee = {http://dx.doi.org/10.1007/978-3-540-79719-7_13},
crossref = {DBLP:conf/sat/2008},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/sat/2008,
editor = {Hans Kleine B{\"u}ning and
Xishun Zhao},
title = {Theory and Applications of Satisfiability Testing - SAT
2008, 11th International Conference, SAT 2008, Guangzhou,
China, May 12-15, 2008. Proceedings},
booktitle = {SAT},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {4996},
year = {2008},
isbn = {978-3-540-79718-0},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/sat/FaureNOR08,
author = {Germain Faure and
Robert Nieuwenhuis and
Albert Oliveras and
Enric Rodr\'{\i}guez-Carbonell},
title = {SAT Modulo the Theory of Linear Arithmetic: Exact, Inexact
and Commercial Solvers},
booktitle = {SAT},
year = {2008},
pages = {77-90},
ee = {http://dx.doi.org/10.1007/978-3-540-79719-7_8},
crossref = {DBLP:conf/sat/2008},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/lpar/BezemNR08,
author = {Marc Bezem and
Robert Nieuwenhuis and
Enric Rodr\'{\i}guez-Carbonell},
title = {The Max-Atom Problem and Its Relevance},
booktitle = {LPAR},
year = {2008},
pages = {47-61},
ee = {http://dx.doi.org/10.1007/978-3-540-89439-1_4},
crossref = {DBLP:conf/lpar/2008},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/lpar/2008,
editor = {Iliano Cervesato and
Helmut Veith and
Andrei Voronkov},
title = {Logic for Programming, Artificial Intelligence, and Reasoning,
15th International Conference, LPAR 2008, Doha, Qatar, November
22-27, 2008. Proceedings},
booktitle = {LPAR},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {5330},
year = {2008},
isbn = {978-3-540-89438-4},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/lpar/AsinNOR08,
author = {Roberto As\'{\i}n and
Robert Nieuwenhuis and
Albert Oliveras and
Enric Rodr\'{\i}guez-Carbonell},
title = {Efficient Generation of Unsatisfiability Proofs and Cores
in SAT},
booktitle = {LPAR},
year = {2008},
pages = {16-30},
ee = {http://dx.doi.org/10.1007/978-3-540-89439-1_2},
crossref = {DBLP:conf/lpar/2008},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/iclp/BistarelliGLR08,
author = {Stefano Bistarelli and
Fabio Gadducci and
Javier Larrosa and
Emma Rollon},
title = {A Soft Approach to Multi-objective Optimization},
booktitle = {ICLP},
year = {2008},
pages = {764-768},
ee = {http://dx.doi.org/10.1007/978-3-540-89982-2_73},
crossref = {DBLP:conf/iclp/2008},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/iclp/2008,
editor = {Maria Garcia de la Banda and
Enrico Pontelli},
title = {Logic Programming, 24th International Conference, ICLP 2008,
Udine, Italy, December 9-13 2008, Proceedings},
booktitle = {ICLP},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {5366},
year = {2008},
isbn = {978-3-540-89981-5},
ee = {http://dx.doi.org/10.1007/978-3-540-89982-2},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/fmcad/BofillNORR08,
author = {Miquel Bofill and
Robert Nieuwenhuis and
Albert Oliveras and
Enric Rodr\'{\i}guez-Carbonell and
Albert Rubio},
title = {A Write-Based Solver for SAT Modulo the Theory of Arrays},
booktitle = {FMCAD},
year = {2008},
pages = {1-8},
ee = {http://dx.doi.org/10.1109/FMCAD.2008.ECP.18},
crossref = {DBLP:conf/fmcad/2008},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/fmcad/2008,
editor = {Alessandro Cimatti and
Robert B. Jones},
title = {Formal Methods in Computer-Aided Design, FMCAD 2008, Portland,
Oregon, USA, 17-20 November 2008},
booktitle = {FMCAD},
publisher = {IEEE},
year = {2008},
isbn = {978-1-4244-2735-2},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/csl/BlanquiJR08,
author = {Fr{\'e}d{\'e}ric Blanqui and
Jean-Pierre Jouannaud and
Albert Rubio},
title = {The Computability Path Ordering: The End of a Quest},
booktitle = {CSL},
year = {2008},
pages = {1-14},
ee = {http://dx.doi.org/10.1007/978-3-540-87531-4_1},
crossref = {DBLP:conf/csl/2008},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/csl/2008,
editor = {Michael Kaminski and
Simone Martini},
title = {Computer Science Logic, 22nd International Workshop, CSL
2008, 17th Annual Conference of the EACSL, Bertinoro, Italy,
September 16-19, 2008. Proceedings},
booktitle = {CSL},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {5213},
year = {2008},
isbn = {978-3-540-87530-7},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/ccia/AnsoteguiBL08,
author = {Carlos Ans{\'o}tegui and
Maria Luisa Bonet and
Jordi Levy},
title = {Random SAT Instances {\`a} la Carte},
booktitle = {CCIA},
year = {2008},
pages = {109-117},
ee = {http://dx.doi.org/10.3233/978-1-58603-925-7-109},
crossref = {DBLP:conf/ccia/2008},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/ccia/2008,
editor = {Teresa Alsinet and
Josep Puyol-Gruart and
Carme Torras},
title = {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\'{\i} d'Emp{\'u}ries, Spain},
booktitle = {CCIA},
publisher = {IOS Press},
series = {Frontiers in Artificial Intelligence and Applications},
volume = {184},
year = {2008},
isbn = {978-1-58603-925-7},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/cav/BofillNORR08,
author = {Miquel Bofill and
Robert Nieuwenhuis and
Albert Oliveras and
Enric Rodr\'{\i}guez-Carbonell and
Albert Rubio},
title = {The Barcelogic SMT Solver},
booktitle = {CAV},
year = {2008},
pages = {294-298},
ee = {http://dx.doi.org/10.1007/978-3-540-70545-1_27},
crossref = {DBLP:conf/cav/2008},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/cav/2008,
editor = {Aarti Gupta and
Sharad Malik},
title = {Computer Aided Verification, 20th International Conference,
CAV 2008, Princeton, NJ, USA, July 7-14, 2008, Proceedings},
booktitle = {CAV},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {5123},
year = {2008},
isbn = {978-3-540-70543-7},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/aaai/AnsoteguiBLM08,
author = {Carlos Ans{\'o}tegui and
Maria Luisa Bonet and
Jordi Levy and
Felip Many{\`a}},
title = {Measuring the Hardness of SAT Instances},
booktitle = {AAAI},
year = {2008},
pages = {222-228},
ee = {http://www.aaai.org/Library/AAAI/2008/aaai08-035.php},
crossref = {DBLP:conf/aaai/2008},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/aaai/2008,
editor = {Dieter Fox and
Carla P. Gomes},
title = {Proceedings of the Twenty-Third AAAI Conference on Artificial
Intelligence, AAAI 2008, Chicago, Illinois, USA, July 13-17,
2008},
booktitle = {AAAI},
publisher = {AAAI Press},
year = {2008},
isbn = {978-1-57735-368-3},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/dagstuhl/BaaderCGN07a,
author = {Franz Baader and
Byron Cook and
J{\"u}rgen Giesl and
Robert Nieuwenhuis},
title = {07401 Abstracts Collection -- Deduction and Decision
Procedures},
booktitle = {Deduction and Decision Procedures},
year = {2007},
ee = {http://drops.dagstuhl.de/opus/volltexte/2007/1252},
crossref = {DBLP:conf/dagstuhl/2007P7401},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/dagstuhl/2007P7401,
editor = {Franz Baader and
Byron Cook and
J{\"u}rgen Giesl and
Robert Nieuwenhuis},
title = {Deduction and Decision Procedures, 30.09. - 05.10.2007},
booktitle = {Deduction and Decision Procedures},
publisher = {Internationales Begegnungs- und Forschungszentrum fuer
Informatik
(IBFI), Schloss Dagstuhl, Germany},
series = {Dagstuhl Seminar Proceedings},
volume = {07401},
year = {2007},
ee = {http://drops.dagstuhl.de/portals/07401/},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/scp/Rodriguez-CarbonellK07,
author = {Enric Rodr\'{\i}guez-Carbonell and
Deepak Kapur},
title = {Automatic generation of polynomial invariants of bounded
degree using abstract interpretation},
journal = {Sci. Comput. Program.},
volume = {64},
number = {1},
year = {2007},
pages = {54-75},
ee = {http://dx.doi.org/10.1016/j.scico.2006.03.003},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/jsc/Rodriguez-CarbonellK07,
author = {Enric Rodr\'{\i}guez-Carbonell and
Deepak Kapur},
title = {Generating all polynomial invariants in simple loops},
journal = {J. Symb. Comput.},
volume = {42},
number = {4},
year = {2007},
pages = {443-476},
ee = {http://dx.doi.org/10.1016/j.jsc.2007.01.002},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/jacm/JouannaudR07,
author = {Jean-Pierre Jouannaud and
Albert Rubio},
title = {Polymorphic higher-order recursive path orderings},
journal = {J. ACM},
volume = {54},
number = {1},
year = {2007},
ee = {http://doi.acm.org/10.1145/1206035.1206037},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/iandc/NieuwenhuisO07,
author = {Robert Nieuwenhuis and
Albert Oliveras},
title = {Fast congruence closure and extensions},
journal = {Inf. Comput.},
volume = {205},
number = {4},
year = {2007},
pages = {557-580},
ee = {http://dx.doi.org/10.1016/j.ic.2006.08.009},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/ai/BonetLM07,
author = {Maria Luisa Bonet and
Jordi Levy and
Felip Many{\`a}},
title = {Resolution for Max-SAT},
journal = {Artif. Intell.},
volume = {171},
number = {8-9},
year = {2007},
pages = {606-618},
ee = {http://dx.doi.org/10.1016/j.artint.2007.03.001},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/sat/HerasLO07,
author = {Federico Heras and
Javier Larrosa and
Albert Oliveras},
title = {MiniMaxSat: A New Weighted Max-SAT Solver},
booktitle = {SAT},
year = {2007},
pages = {41-55},
ee = {http://dx.doi.org/10.1007/978-3-540-72788-0_8},
crossref = {DBLP:conf/sat/2007},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/sat/2007,
editor = {Jo{\~a}o Marques-Silva and
Karem A. Sakallah},
title = {Theory and Applications of Satisfiability Testing - SAT
2007, 10th International Conference, Lisbon, Portugal, May
28-31, 2007, Proceedings},
booktitle = {SAT},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {4501},
year = {2007},
isbn = {978-3-540-72787-3},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/sat/AnsoteguiBLM07,
author = {Carlos Ans{\'o}tegui and
Maria Luisa Bonet and
Jordi Levy and
Felip Many{\`a}},
title = {Mapping CSP into Many-Valued SAT},
booktitle = {SAT},
year = {2007},
pages = {10-15},
ee = {http://dx.doi.org/10.1007/978-3-540-72788-0_4},
crossref = {DBLP:conf/sat/2007},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/rta/NieuwenhuisORR07,
author = {Robert Nieuwenhuis and
Albert Oliveras and
Enric Rodr\'{\i}guez-Carbonell and
Albert Rubio},
title = {Challenges in Satisfiability Modulo Theories},
booktitle = {RTA},
year = {2007},
pages = {2-18},
ee = {http://dx.doi.org/10.1007/978-3-540-73449-9_2},
crossref = {DBLP:conf/rta/2007},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/rta/2007,
editor = {Franz Baader},
title = {Term Rewriting and Applications, 18th International Conference,
RTA 2007, Paris, France, June 26-28, 2007, Proceedings},
booktitle = {RTA},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {4533},
year = {2007},
isbn = {978-3-540-73447-5},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/lpar/BlanquiJR07,
author = {Fr{\'e}d{\'e}ric Blanqui and
Jean-Pierre Jouannaud and
Albert Rubio},
title = {HORPO with Computability Closure: A Reconstruction},
booktitle = {LPAR},
year = {2007},
pages = {138-150},
ee = {http://dx.doi.org/10.1007/978-3-540-75560-9_12},
crossref = {DBLP:conf/lpar/2007},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/lpar/2007,
editor = {Nachum Dershowitz and
Andrei Voronkov},
title = {Logic for Programming, Artificial Intelligence, and Reasoning,
14th International Conference, LPAR 2007, Yerevan, Armenia,
October 15-19, 2007, Proceedings},
booktitle = {LPAR},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {4790},
year = {2007},
isbn = {978-3-540-75558-6},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/ismvl/AnsoteguiBLM07,
author = {Carlos Ans{\'o}tegui and
Maria Luisa Bonet and
Jordi Levy and
Felip Many{\`a}},
title = {A Complete Resolution Calculus for Signed Max-SAT},
booktitle = {ISMVL},
year = {2007},
pages = {22},
ee = {http://dx.doi.org/10.1109/ISMVL.2007.2},
crossref = {DBLP:conf/ismvl/2007},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/ismvl/2007,
title = {37th International Symposium on Multiple-Valued Logic, ISMVL
2007, 13-16 May 2007, Oslo, Norway},
booktitle = {ISMVL},
publisher = {IEEE Computer Society},
year = {2007},
isbn = {978-0-7695-2831-1},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/ijcai/AnsoteguiBLM07,
author = {Carlos Ans{\'o}tegui and
Maria Luisa Bonet and
Jordi Levy and
Felip Many{\`a}},
title = {The Logic Behind Weighted CSP},
booktitle = {IJCAI},
year = {2007},
pages = {32-37},
ee = {http://dli.iiit.ac.in/ijcai/IJCAI-2007/PDF/IJCAI07-003.pdf},
crossref = {DBLP:conf/ijcai/2007},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/ijcai/2007,
editor = {Manuela M. Veloso},
title = {IJCAI 2007, Proceedings of the 20th International Joint
Conference on Artificial Intelligence, Hyderabad, India,
January 6-12, 2007},
booktitle = {IJCAI},
year = {2007},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/dagstuhl/BaaderCGN07,
author = {Franz Baader and
Byron Cook and
J{\"u}rgen Giesl and
Robert Nieuwenhuis},
title = {07401 Executive Summary -- Deduction and Decision Procedures},
booktitle = {Deduction and Decision Procedures},
year = {2007},
ee = {http://drops.dagstuhl.de/opus/volltexte/2007/1251},
crossref = {DBLP:conf/dagstuhl/2007P7401},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/ccia/AnsoteguiBLM07,
author = {Carlos Ans{\'o}tegui and
Maria Luisa Bonet and
Jordi Levy and
Felip Many{\`a}},
title = {What Is a Real-World SAT Instance?},
booktitle = {CCIA},
year = {2007},
pages = {19-28},
ee = {http://www.booksonline.iospress.nl/Content/View.aspx?piid=7644},
crossref = {DBLP:conf/ccia/2007},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/ccia/2007,
editor = {Cecilio Angulo and
Lluis Godo},
title = {Artificial Intelligence Research and Development, Proceedings
of the 10th International Conference of the ACIA, CCIA 2007,
October 25-26, 2007, Sant Juli{\`a} de L{\`o}ria,
Andorra},
booktitle = {CCIA},
publisher = {IOS Press},
series = {Frontiers in Artificial Intelligence and Applications},
volume = {163},
year = {2007},
isbn = {978-1-58603-798-7},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/birthday/BorrallerasR07,
author = {Cristina Borralleras and
Albert Rubio},
title = {Orderings and Constraints: Theory and Practice of Proving
Termination},
booktitle = {Rewriting, Computation and Proof},
year = {2007},
pages = {28-43},
ee = {http://dx.doi.org/10.1007/978-3-540-73147-4_2},
crossref = {DBLP:conf/birthday/2007jouannaud},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/birthday/2007jouannaud,
editor = {Hubert Comon-Lundh and
Claude Kirchner and
H{\'e}l{\`e}ne Kirchner},
title = {Rewriting, Computation and Proof, Essays Dedicated to Jean-
Pierre
Jouannaud on the Occasion of His 60th Birthday},
booktitle = {Rewriting, Computation and Proof},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {4600},
year = {2007},
isbn = {978-3-540-73146-7},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/aaai/RollonL07,
author = {Emma Rollon and
Javier Larrosa},
title = {Multi-Objective Russian Doll Search},
booktitle = {AAAI},
year = {2007},
pages = {249-254},
ee = {http://www.aaai.org/Library/AAAI/2007/aaai07-038.php},
crossref = {DBLP:conf/aaai/2007},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/aaai/2007,
title = {Proceedings of the Twenty-Second AAAI Conference on Artificial
Intelligence, July 22-26, 2007, Vancouver, British Columbia,
Canada},
booktitle = {AAAI},
publisher = {AAAI Press},
year = {2007},
isbn = {978-1-57735-323-2},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/aaai/AnsoteguiBLM07,
author = {Carlos Ans{\'o}tegui and
Maria Luisa Bonet and
Jordi Levy and
Felip Many{\`a}},
title = {Inference Rules for High-Order Consistency in Weighted CSP},
booktitle = {AAAI},
year = {2007},
pages = {167-172},
ee = {http://www.aaai.org/Library/AAAI/2007/aaai07-025.php},
crossref = {DBLP:conf/aaai/2007},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/jcb/BonetJMA06,
author = {Maria Luisa Bonet and
Katherine St. John and
Ruchi Mahindru and
Nina Amenta},
title = {Approximating Subtree Distances Between Phylogenies},
journal = {Journal of Computational Biology},
volume = {13},
number = {8},
year = {2006},
pages = {1419-1434},
ee = {http://dx.doi.org/10.1089/cmb.2006.13.1419},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/jacm/NieuwenhuisOT06,
author = {Robert Nieuwenhuis and
Albert Oliveras and
Cesare Tinelli},
title = {Solving SAT and SAT Modulo Theories: From an abstract Davis--
Putnam--Logemann--Loveland
procedure to DPLL({\it T})},
journal = {J. ACM},
volume = {53},
number = {6},
year = {2006},
pages = {937-977},
ee = {http://doi.acm.org/10.1145/1217856.1217859},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/heuristics/RollonL06,
author = {Emma Rollon and
Javier Larrosa},
title = {Bucket elimination for multiobjective optimization problems},
journal = {J. Heuristics},
volume = {12},
number = {4-5},
year = {2006},
pages = {307-328},
ee = {http://dx.doi.org/10.1007/s10732-006-6726-y},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/heuristics/HerasL06,
author = {Federico Heras and
Javier Larrosa},
title = {Intelligent variable orderings and re-orderings in DAC-based
solvers for WCSP},
journal = {J. Heuristics},
volume = {12},
number = {4-5},
year = {2006},
pages = {287-306},
ee = {http://dx.doi.org/10.1007/s10732-006-8248-z},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/sat/NieuwenhuisO06,
author = {Robert Nieuwenhuis and
Albert Oliveras},
title = {On SAT Modulo Theories and Optimization Problems},
booktitle = {SAT},
year = {2006},
pages = {156-169},
ee = {http://dx.doi.org/10.1007/11814948_18},
crossref = {DBLP:conf/sat/2006},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/sat/2006,
editor = {Armin Biere and
Carla P. Gomes},
title = {Theory and Applications of Satisfiability Testing - SAT
2006, 9th International Conference, Seattle, WA, USA, August
12-15, 2006, Proceedings},
booktitle = {SAT},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {4121},
year = {2006},
isbn = {3-540-37206-7},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/sat/BonetLM06,
author = {Maria Luisa Bonet and
Jordi Levy and
Felip Many{\`a}},
title = {A Complete Calculus for Max-SAT},
booktitle = {SAT},
year = {2006},
pages = {240-251},
ee = {http://dx.doi.org/10.1007/11814948_24},
crossref = {DBLP:conf/sat/2006},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/rta/JouannaudR06,
author = {Jean-Pierre Jouannaud and
Albert Rubio},
title = {Higher-Order Orderings for Normal Rewriting},
booktitle = {RTA},
year = {2006},
pages = {387-399},
ee = {http://dx.doi.org/10.1007/11805618_29},
crossref = {DBLP:conf/rta/2006},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/rta/2006,
editor = {Frank Pfenning},
title = {Term Rewriting and Applications, 17th International Conference,
RTA 2006, Seattle, WA, USA, August 12-14, 2006, Proceedings},
booktitle = {RTA},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {4098},
year = {2006},
isbn = {3-540-36834-5},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/lpar/BlanquiJR06,
author = {Fr{\'e}d{\'e}ric Blanqui and
Jean-Pierre Jouannaud and
Albert Rubio},
title = {Higher-Order Termination: From Kruskal to Computability},
booktitle = {LPAR},
year = {2006},
pages = {1-14},
ee = {http://dx.doi.org/10.1007/11916277_1},
crossref = {DBLP:conf/lpar/2006},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/lpar/2006,
editor = {Miki Hermann and
Andrei Voronkov},
title = {Logic for Programming, Artificial Intelligence, and Reasoning,
13th International Conference, LPAR 2006, Phnom Penh, Cambodia,
November 13-17, 2006, Proceedings},
booktitle = {LPAR},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {4246},
year = {2006},
isbn = {3-540-48281-4},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/lpar/BarrettNOT06,
author = {Clark Barrett and
Robert Nieuwenhuis and
Albert Oliveras and
Cesare Tinelli},
title = {Splitting on Demand in SAT Modulo Theories},
booktitle = {LPAR},
year = {2006},
pages = {512-526},
ee = {http://dx.doi.org/10.1007/11916277_35},
crossref = {DBLP:conf/lpar/2006},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/ecai/RollonL06,
author = {Emma Rollon and
Javier Larrosa},
title = {Multi-Objective Propagation in Constraint Programming},
booktitle = {ECAI},
year = {2006},
pages = {128-132},
ee = {http://www.booksonline.iospress.nl/Content/View.aspx?piid=1660},
crossref = {DBLP:conf/ecai/2006},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/ecai/2006,
editor = {Gerhard Brewka and
Silvia Coradeschi and
Anna Perini and
Paolo Traverso},
title = {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},
booktitle = {ECAI},
publisher = {IOS Press},
series = {Frontiers in Artificial Intelligence and Applications},
volume = {141},
year = {2006},
isbn = {1-58603-642-4},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/cp/RollonL06,
author = {Emma Rollon and
Javier Larrosa},
title = {Mini-bucket Elimination with Bucket Propagation},
booktitle = {CP},
year = {2006},
pages = {484-498},
ee = {http://dx.doi.org/10.1007/11889205_35},
crossref = {DBLP:conf/cp/2006},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/cp/2006,
editor = {Fr{\'e}d{\'e}ric Benhamou},
title = {Principles and Practice of Constraint Programming - CP 2006,
12th International Conference, CP 2006, Nantes, France,
September 25-29, 2006, Proceedings},
booktitle = {CP},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {4204},
year = {2006},
isbn = {3-540-46267-8},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/cav/LahiriNO06,
author = {Shuvendu K. Lahiri and
Robert Nieuwenhuis and
Albert Oliveras},
title = {SMT Techniques for Fast Predicate Abstraction},
booktitle = {CAV},
year = {2006},
pages = {424-437},
ee = {http://dx.doi.org/10.1007/11817963_39},
crossref = {DBLP:conf/cav/2006},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/cav/2006,
editor = {Thomas Ball and
Robert B. Jones},
title = {Computer Aided Verification, 18th International Conference,
CAV 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings},
booktitle = {CAV},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {4144},
year = {2006},
isbn = {3-540-37406-X},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/aaai/HerasL06,
author = {Federico Heras and
Javier Larrosa},
title = {New Inference Rules for Efficient Max-SAT Solving},
booktitle = {AAAI},
year = {2006},
pages = {68-73},
ee = {http://www.aaai.org/Library/AAAI/2006/aaai06-011.php},
crossref = {DBLP:conf/aaai/2006},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/aaai/2006,
title = {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},
booktitle = {AAAI},
publisher = {AAAI Press},
year = {2006},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/jair/LarrosaMN05,
author = {Javier Larrosa and
Enric Morancho and
David Niso},
title = {On the Practical use of Variable Elimination in Constraint
Optimization Problems: 'Still-life' as a Case Study},
journal = {J. Artif. Intell. Res. (JAIR)},
volume = {23},
year = {2005},
pages = {421-440},
ee = {http://dx.doi.org/10.1613/jair.1541},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/ai/KaskDLD05,
author = {Kalev Kask and
Rina Dechter and
Javier Larrosa and
Avi Dechter},
title = {Unifying tree decompositions for reasoning in graphical
models},
journal = {Artif. Intell.},
volume = {166},
number = {1-2},
year = {2005},
pages = {165-193},
ee = {http://dx.doi.org/10.1016/j.artint.2005.04.004},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/dagstuhl/2005P5431,
editor = {Franz Baader and
Peter Baumgartner and
Robert Nieuwenhuis and
Andrei Voronkov},
title = {Deduction and Applications, 23.-28. October 2005},
booktitle = {Deduction and Applications},
publisher = {Internationales Begegnungs- und Forschungszentrum f{\"u}r
Informatik (IBFI), Schloss Dagstuhl, Germany},
series = {Dagstuhl Seminar Proceedings},
volume = {05431},
year = {2006},
ee = {http://drops.dagstuhl.de/portals/05431/},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/sas/BagnaraRZ05,
author = {Roberto Bagnara and
Enric Rodr\'{\i}guez-Carbonell and
Enea Zaffanella},
title = {Generation of Basic Semi-algebraic Invariants Using Convex
Polyhedra},
booktitle = {SAS},
year = {2005},
pages = {19-34},
ee = {http://dx.doi.org/10.1007/11547662_4},
crossref = {DBLP:conf/sas/2005},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/sas/2005,
editor = {Chris Hankin and
Igor Siveroni},
title = {Static Analysis, 12th International Symposium, SAS 2005,
London, UK, September 7-9, 2005, Proceedings},
booktitle = {SAS},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {3672},
year = {2005},
isbn = {3-540-28584-9},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/rta/NieuwenhuisO05,
author = {Robert Nieuwenhuis and
Albert Oliveras},
title = {Proof-Producing Congruence Closure},
booktitle = {RTA},
year = {2005},
pages = {453-468},
ee = {http://dx.doi.org/10.1007/978-3-540-32033-3_33},
crossref = {DBLP:conf/rta/2005},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/rta/2005,
editor = {J{\"u}rgen Giesl},
title = {Term Rewriting and Applications, 16th International Conference,
RTA 2005, Nara, Japan, April 19-21, 2005, Proceedings},
booktitle = {RTA},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {3467},
year = {2005},
isbn = {3-540-25596-6},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/rta/FernandezGR05,
author = {Mirtha-Lina Fern{\'a}ndez and
Guillem Godoy and
Albert Rubio},
title = {Orderings for Innermost Termination},
booktitle = {RTA},
year = {2005},
pages = {17-31},
ee = {http://dx.doi.org/10.1007/978-3-540-32033-3_3},
crossref = {DBLP:conf/rta/2005},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/lpar/NieuwenhuisO05,
author = {Robert Nieuwenhuis and
Albert Oliveras},
title = {Decision Procedures for SAT, SAT Modulo Theories and Beyond.
The BarcelogicTools},
booktitle = {LPAR},
year = {2005},
pages = {23-46},
ee = {http://dx.doi.org/10.1007/11591191_3},
crossref = {DBLP:conf/lpar/2005},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/lpar/2005,
editor = {Geoff Sutcliffe and
Andrei Voronkov},
title = {Logic for Programming, Artificial Intelligence, and Reasoning,
12th International Conference, LPAR 2005, Montego Bay, Jamaica,
December 2-6, 2005, Proceedings},
booktitle = {LPAR},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {3835},
year = {2005},
isbn = {3-540-30553-X},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/lpar/FernandezGR05,
author = {Mirtha-Lina Fern{\'a}ndez and
Guillem Godoy and
Albert Rubio},
title = {Recursive Path Orderings Can Also Be Incremental},
booktitle = {LPAR},
year = {2005},
pages = {230-245},
ee = {http://dx.doi.org/10.1007/11591191_17},
crossref = {DBLP:conf/lpar/2005},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/ijcai/SanchezLM05,
author = {Mart\'{\i} S{\'a}nchez and
Javier Larrosa and
Pedro Meseguer},
title = {Improving Tree Decomposition Methods With Function Filtering},
booktitle = {IJCAI},
year = {2005},
pages = {1537-1538},
ee = {http://www.ijcai.org/papers/post-0395.pdf},
crossref = {DBLP:conf/ijcai/2005},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/ijcai/2005,
editor = {Leslie Pack Kaelbling and
Alessandro Saffiotti},
title = {IJCAI-05, Proceedings of the Nineteenth International Joint
Conference on Artificial Intelligence, Edinburgh, Scotland,
UK, July 30-August 5, 2005},
booktitle = {IJCAI},
publisher = {Professional Book Center},
year = {2005},
isbn = {0938075934},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/ijcai/LarrosaH05,
author = {Javier Larrosa and
Federico Heras},
title = {Resolution in Max-SAT and its relation to local consistency
in weighted CSPs},
booktitle = {IJCAI},
year = {2005},
pages = {193-198},
ee = {http://www.ijcai.org/papers/0360.pdf},
crossref = {DBLP:conf/ijcai/2005},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/ijcai/GivryHZL05,
author = {Simon de Givry and
Federico Heras and
Matthias Zytnicki and
Javier Larrosa},
title = {Existential arc consistency: Getting closer to full arc
consistency in weighted CSPs},
booktitle = {IJCAI},
year = {2005},
pages = {84-89},
ee = {http://www.ijcai.org/papers/0827.pdf},
crossref = {DBLP:conf/ijcai/2005},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/hybrid/Rodriguez-CarbonellT05,
author = {Enric Rodr\'{\i}guez-Carbonell and
Ashish Tiwari},
title = {Generating Polynomial Invariants for Hybrid Systems},
booktitle = {HSCC},
year = {2005},
pages = {590-605},
ee = {http://dx.doi.org/10.1007/978-3-540-31954-2_38},
crossref = {DBLP:conf/hybrid/2005},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/hybrid/2005,
editor = {Manfred Morari and
Lothar Thiele},
title = {Hybrid Systems: Computation and Control, 8th International
Workshop, HSCC 2005, Zurich, Switzerland, March 9-11, 2005,
Proceedings},
booktitle = {HSCC},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {3414},
year = {2005},
isbn = {3-540-25108-1},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/dagstuhl/BaaderBNV05,
author = {Franz Baader and
Peter Baumgartner and
Robert Nieuwenhuis and
Andrei Voronkov},
title = {05431 Executive Summary - Deduction and Applications},
booktitle = {Deduction and Applications},
year = {2005},
ee = {http://drops.dagstuhl.de/opus/volltexte/2006/510},
crossref = {DBLP:conf/dagstuhl/2005P5431},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/cp/SanchezLM05,
author = {Mart\'{\i} S{\'a}nchez and
Javier Larrosa and
Pedro Meseguer},
title = {Tree Decomposition with Function Filtering},
booktitle = {CP},
year = {2005},
pages = {593-606},
ee = {http://dx.doi.org/10.1007/11564751_44},
crossref = {DBLP:conf/cp/2005},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/cp/2005,
editor = {Peter van Beek},
title = {Principles and Practice of Constraint Programming - CP 2005,
11th International Conference, CP 2005, Sitges, Spain, October
1-5, 2005, Proceedings},
booktitle = {CP},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {3709},
year = {2005},
isbn = {3-540-29238-1},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/cp/RollonL05,
author = {Emma Rollon and
Javier Larrosa},
title = {Depth-First Mini-Bucket Elimination},
booktitle = {CP},
year = {2005},
pages = {563-577},
ee = {http://dx.doi.org/10.1007/11564751_42},
crossref = {DBLP:conf/cp/2005},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/cp/HerasL05,
author = {Federico Heras and
Javier Larrosa},
title = {Local Consistency in Weighted CSPs and Inference in Max-SAT},
booktitle = {CP},
year = {2005},
pages = {849},
ee = {http://dx.doi.org/10.1007/11564751_87},
crossref = {DBLP:conf/cp/2005},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/cav/NieuwenhuisO05,
author = {Robert Nieuwenhuis and
Albert Oliveras},
title = {DPLL(T) with Exhaustive Theory Propagation and Its Application
to Difference Logic},
booktitle = {CAV},
year = {2005},
pages = {321-334},
ee = {http://dx.doi.org/10.1007/11513988_33},
crossref = {DBLP:conf/cav/2005},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/cav/2005,
editor = {Kousha Etessami and
Sriram K. Rajamani},
title = {Computer Aided Verification, 17th International Conference,
CAV 2005, Edinburgh, Scotland, UK, July 6-10, 2005,
Proceedings},
booktitle = {CAV},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {3576},
year = {2005},
isbn = {3-540-27231-3},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/cade/2005,
editor = {Robert Nieuwenhuis},
title = {Automated Deduction - CADE-20, 20th International Conference
on Automated Deduction, Tallinn, Estonia, July 22-27, 2005,
Proceedings},
booktitle = {CADE},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {3632},
year = {2005},
isbn = {3-540-28005-7},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/apn/ClarisoRC05,
author = {Robert Claris{\'o} and
Enric Rodr\'{\i}guez-Carbonell and
Jordi Cortadella},
title = {Derivation of Non-structural Invariants of Petri Nets Using
Abstract Interpretation},
booktitle = {ICATPN},
year = {2005},
pages = {188-207},
ee = {http://dx.doi.org/10.1007/11494744_12},
crossref = {DBLP:conf/apn/2005},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/apn/2005,
editor = {Gianfranco Ciardo and
Philippe Darondeau},
title = {Applications and Theory of Petri Nets 2005, 26th International
Conference, ICATPN 2005, Miami, USA, June 20-25, 2005,
Proceedings},
booktitle = {ICATPN},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {3536},
year = {2005},
isbn = {3-540-26301-2},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/dagstuhl/BaaderBNV05a,
author = {Franz Baader and
Peter Baumgartner and
Robert Nieuwenhuis and
Andrei Voronkov},
title = {05431 Abstracts Collection - Deduction and Applications},
booktitle = {Deduction and Applications},
year = {2005},
ee = {http://drops.dagstuhl.de/opus/volltexte/2006/562},
crossref = {DBLP:conf/dagstuhl/2005P5431},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/tocl/GodoyNT04,
author = {Guillem Godoy and
Robert Nieuwenhuis and
Ashish Tiwari},
title = {Classes of term rewrite systems with polynomial confluence
problems},
journal = {ACM Trans. Comput. Log.},
volume = {5},
number = {2},
year = {2004},
pages = {321-331},
ee = {http://doi.acm.org/10.1145/976706.976712},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/tcs/EstebanGM04,
author = {Juan Luis Esteban and
Nicola Galesi and
Jochen Messner},
title = {On the complexity of resolution with bounded conjunctions},
journal = {Theor. Comput. Sci.},
volume = {321},
number = {2-3},
year = {2004},
pages = {347-370},
ee = {http://dx.doi.org/10.1016/j.tcs.2004.04.004},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/jsc/GodoyN04,
author = {Guillem Godoy and
Robert Nieuwenhuis},
title = {Superposition with completely built-in Abelian groups},
journal = {J. Symb. Comput.},
volume = {37},
number = {1},
year = {2004},
pages = {1-33},
ee = {http://dx.doi.org/10.1016/S0747-7171(03)00070-1},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/jar/GanzingerNN04,
author = {Harald Ganzinger and
Robert Nieuwenhuis and
Pilar Nivela},
title = {Fast Term Indexing with Coded Context Trees},
journal = {J. Autom. Reasoning},
volume = {32},
number = {2},
year = {2004},
pages = {103-120},
ee = {http://dx.doi.org/10.1023/B:JARS.0000029963.64213.ac},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/iandc/AtseriasB04,
author = {Albert Atserias and
Maria Luisa Bonet},
title = {On the automatizability of resolution and related propositional
proof systems},
journal = {Inf. Comput.},
volume = {189},
number = {2},
year = {2004},
pages = {182-201},
ee = {http://dx.doi.org/10.1016/j.ic.2003.10.004},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/constraints/GodoyN04,
author = {Guillem Godoy and
Robert Nieuwenhuis},
title = {Constraint Solving for Term Orderings Compatible with Abelian
Semigroups, Monoids and Groups},
journal = {Constraints},
volume = {9},
number = {3},
year = {2004},
pages = {167-192},
ee = {http://dx.doi.org/10.1023/B:CONS.0000036021.31386.cc},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/cc/BonetDGMP04,
author = {Maria Luisa Bonet and
Carlos Domingo and
Ricard Gavald{\`a} and
Alexis Maciel and
Toniann Pitassi},
title = {Non-Automatizability of Bounded-Depth Frege Proofs},
journal = {Computational Complexity},
volume = {13},
number = {1-2},
year = {2004},
pages = {47-68},
ee = {http://dx.doi.org/10.1007/s00037-004-0183-5},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/ai/LarrosaS04,
author = {Javier Larrosa and
Thomas Schiex},
title = {Solving weighted CSP by maintaining arc consistency},
journal = {Artif. Intell.},
volume = {159},
number = {1-2},
year = {2004},
pages = {1-26},
ee = {http://dx.doi.org/10.1016/j.artint.2004.05.004},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/sas/Rodriguez-CarbonellK04,
author = {Enric Rodr\'{\i}guez-Carbonell and
Deepak Kapur},
title = {An Abstract Interpretation Approach for Automatic Generation
of Polynomial Invariants},
booktitle = {SAS},
year = {2004},
pages = {280-295},
ee = {http://dx.doi.org/10.1007/978-3-540-27864-1_21},
crossref = {DBLP:conf/sas/2004},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/sas/2004,
editor = {Roberto Giacobazzi},
title = {Static Analysis, 11th International Symposium, SAS 2004,
Verona, Italy, August 26-28, 2004, Proceedings},
booktitle = {SAS},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {3148},
year = {2004},
isbn = {3-540-22791-1},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/lpar/NieuwenhuisOT04,
author = {Robert Nieuwenhuis and
Albert Oliveras and
Cesare Tinelli},
title = {Abstract DPLL and Abstract DPLL Modulo Theories},
booktitle = {LPAR},
year = {2004},
pages = {36-50},
ee = {http://dx.doi.org/10.1007/978-3-540-32275-7_3},
crossref = {DBLP:conf/lpar/2004},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/lpar/2004,
editor = {Franz Baader and
Andrei Voronkov},
title = {Logic for Programming, Artificial Intelligence, and Reasoning,
11th International Conference, LPAR 2004, Montevideo, Uruguay,
March 14-18, 2005, Proceedings},
booktitle = {LPAR},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {3452},
year = {2005},
isbn = {3-540-25236-3},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/issac/Rodriguez-CarbonellK04,
author = {Enric Rodr\'{\i}guez-Carbonell and
Deepak Kapur},
title = {Automatic generation of polynomial loop},
booktitle = {ISSAC},
year = {2004},
pages = {266-273},
ee = {http://doi.acm.org/10.1145/1005285.1005324},
crossref = {DBLP:conf/issac/2004},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/issac/2004,
editor = {Jaime Gutierrez},
title = {Symbolic and Algebraic Computation, International Symposium
ISSAC 2004, Santander, Spain, July 4-7, 2004, Proceedings},
booktitle = {ISSAC},
publisher = {ACM},
year = {2004},
isbn = {1-58113-827-X},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/ictac/Rodriguez-CarbonellK04,
author = {Enric Rodr\'{\i}guez-Carbonell and
Deepak Kapur},
title = {Program Verification Using Automatic Generation of Invariants},
booktitle = {ICTAC},
year = {2004},
pages = {325-340},
ee = {http://dx.doi.org/10.1007/978-3-540-31862-0_24},
crossref = {DBLP:conf/ictac/2004},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/ictac/2004,
editor = {Zhiming Liu and
Keijiro Araki},
title = {Theoretical Aspects of Computing - ICTAC 2004, First
International
Colloquium, Guiyang, China, September 20-24, 2004, Revised
Selected Papers},
booktitle = {ICTAC},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {3407},
year = {2005},
isbn = {3-540-25304-1},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/ecai/SanchezML04,
author = {Mart\'{\i} S{\'a}nchez and
Pedro Meseguer and
Javier Larrosa},
title = {Using Constraints with Memory to Implement Variable
Elimination},
booktitle = {ECAI},
year = {2004},
pages = {216-220},
crossref = {DBLP:conf/ecai/2004},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/ecai/2004,
editor = {Ramon L{\'o}pez de M{\'a}ntaras and
Lorenza Saitta},
title = {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},
booktitle = {ECAI},
publisher = {IOS Press},
year = {2004},
isbn = {1-58603-452-9},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/cp/SanchezML04,
author = {Mart\'{\i} S{\'a}nchez and
Pedro Meseguer and
Javier Larrosa},
title = {Improving the Applicability of Adaptive Consistency: Preliminary
Results},
booktitle = {CP},
year = {2004},
pages = {757-761},
ee = {http://dx.doi.org/10.1007/978-3-540-30201-8_61},
crossref = {DBLP:conf/cp/2004},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/cp/2004,
editor = {Mark Wallace},
title = {Principles and Practice of Constraint Programming - CP 2004,
10th International Conference, CP 2004, Toronto, Canada,
September 27 - October 1, 2004, Proceedings},
booktitle = {CP},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {3258},
year = {2004},
isbn = {3-540-23241-9},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/cav/GanzingerHNOT04,
author = {Harald Ganzinger and
George Hagen and
Robert Nieuwenhuis and
Albert Oliveras and
Cesare Tinelli},
title = {DPLL( T): Fast Decision Procedures},
booktitle = {CAV},
year = {2004},
pages = {175-188},
ee = {http://dx.doi.org/10.1007/978-3-540-27813-9_14},
crossref = {DBLP:conf/cav/2004},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/cav/2004,
editor = {Rajeev Alur and
Doron Peled},
title = {Computer Aided Verification, 16th International Conference,
CAV 2004, Boston, MA, USA, July 13-17, 2004, Proceedings},
booktitle = {CAV},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {3114},
year = {2004},
isbn = {3-540-22342-8},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/cade/BofillR04,
author = {Miquel Bofill and
Albert Rubio},
title = {Redundancy Notions for Paramodulation with Non-monotonic
Orderings},
booktitle = {IJCAR},
year = {2004},
pages = {107-121},
ee = {http://dx.doi.org/10.1007/978-3-540-25984-8_6},
crossref = {DBLP:conf/cade/2004},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/cade/2004,
editor = {David A. Basin and
Micha{\"e}l Rusinowitch},
title = {Automated Reasoning - Second International Joint Conference,
IJCAR 2004, Cork, Ireland, July 4-8, 2004, Proceedings},
booktitle = {IJCAR},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {3097},
year = {2004},
isbn = {3-540-22345-2},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/tocl/ComonNNR03,
author = {Hubert Comon and
Paliath Narendran and
Robert Nieuwenhuis and
Micha{\"e}l Rusinowitch},
title = {Deciding the confluence of ordered term rewrite systems},
journal = {ACM Trans. Comput. Log.},
volume = {4},
number = {1},
year = {2003},
pages = {33-55},
ee = {http://doi.acm.org/10.1145/601775.601777},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/jsc/DegtyarevNV03,
author = {Anatoli Degtyarev and
Robert Nieuwenhuis and
Andrei Voronkov},
title = {Stratified resolution},
journal = {J. Symb. Comput.},
volume = {36},
number = {1-2},
year = {2003},
pages = {79-99},
ee = {http://dx.doi.org/10.1016/S0747-7171(03)00036-1},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/jar/BofillGNR03,
author = {Miquel Bofill and
Guillem Godoy and
Robert Nieuwenhuis and
Albert Rubio},
title = {Paramodulation and Knuth-Bendix Completion with Nontotal
and Nonmonotonic Orderings},
journal = {J. Autom. Reasoning},
volume = {30},
number = {1},
year = {2003},
pages = {99-120},
ee = {http://dx.doi.org/10.1023/A:1022515030222},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/ipl/EstebanT03,
author = {Juan Luis Esteban and
Jacobo Tor{\'a}n},
title = {A combinatorial characterization of treelike resolution
space},
journal = {Inf. Process. Lett.},
volume = {87},
number = {6},
year = {2003},
pages = {295-300},
ee = {http://dx.doi.org/10.1016/S0020-0190(03)00345-4},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/constraints/LarrosaD03,
author = {Javier Larrosa and
Rina Dechter},
title = {Boosting Search with Variable Elimination in Constraint
Optimization and Constraint Satisfaction Problems},
journal = {Constraints},
volume = {8},
number = {3},
year = {2003},
pages = {303-326},
ee = {http://dx.doi.org/10.1023/A:1025627211942},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/aml/BonetG03,
author = {Maria Luisa Bonet and
Nicola Galesi},
title = {Degree complexity for a modified pigeonhole principle},
journal = {Arch. Math. Log.},
volume = {42},
number = {5},
year = {2003},
pages = {403-414},
ee = {http://dx.doi.org/10.1007/s001530200141},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/aepia/LarrosaM03,
author = {Javier Larrosa and
Pedro Meseguer},
title = {Algoritmos para Satisfacci{\'o}n de Restricciones},
journal = {Inteligencia Artificial, Revista Iberoamericana de Inteligencia
Artificial},
volume = {7},
number = {20},
year = {2003},
pages = {31-42},
ee = {http://polar.lsi.uned.es/revista/index.php/ia/article/view/373},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/rta/BorrallerasR03,
author = {Cristina Borralleras and
Albert Rubio},
title = {Monotonic AC-Compatible Semantic Path Orderings},
booktitle = {RTA},
year = {2003},
pages = {279-295},
ee = {http://dx.doi.org/10.1007/3-540-44881-0_20},
crossref = {DBLP:conf/rta/2003},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/rta/2003,
editor = {Robert Nieuwenhuis},
title = {Rewriting Techniques and Applications, 14th International
Conference, RTA 2003, Valencia, Spain, June 9-11, 2003,
Proceedings},
booktitle = {RTA},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {2706},
year = {2003},
isbn = {3-540-40254-3},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/lpar/NieuwenhuisO03,
author = {Robert Nieuwenhuis and
Albert Oliveras},
title = {Congruence Closure with Integer Offsets},
booktitle = {LPAR},
year = {2003},
pages = {78-90},
ee = {http://dx.doi.org/10.1007/978-3-540-39813-4_5},
crossref = {DBLP:conf/lpar/2003},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/lpar/2003,
editor = {Moshe Y. Vardi and
Andrei Voronkov},
title = {Logic for Programming, Artificial Intelligence, and Reasoning,
10th International Conference, LPAR 2003, Almaty, Kazakhstan,
September 22-26, 2003, Proceedings},
booktitle = {LPAR},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {2850},
year = {2003},
isbn = {3-540-20101-7},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/ijcai/LarrosaS03,
author = {Javier Larrosa and
Thomas Schiex},
title = {In the quest of the best form of local consistency for Weighted
CSP},
booktitle = {IJCAI},
year = {2003},
pages = {239-244},
crossref = {DBLP:conf/ijcai/2003},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/ijcai/2003,
editor = {Georg Gottlob and
Toby Walsh},
title = {IJCAI-03, Proceedings of the Eighteenth International Joint
Conference on Artificial Intelligence, Acapulco, Mexico,
August 9-15, 2003},
booktitle = {IJCAI},
publisher = {Morgan Kaufmann},
year = {2003},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/cp/LarrosaM03,
author = {Javier Larrosa and
Enric Morancho},
title = {Solving 'Still Life' with Soft Constraints and Bucket
Elimination},
booktitle = {CP},
year = {2003},
pages = {466-479},
ee = {http://dx.doi.org/10.1007/978-3-540-45193-8_32},
crossref = {DBLP:conf/cp/2003},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/cp/2003,
editor = {Francesca Rossi},
title = {Principles and Practice of Constraint Programming - CP 2003,
9th International Conference, CP 2003, Kinsale, Ireland,
September 29 - October 3, 2003, Proceedings},
booktitle = {CP},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {2833},
year = {2003},
isbn = {3-540-20202-1},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/cp/GivryLMS03,
author = {Simon de Givry and
Javier Larrosa and
Pedro Meseguer and
Thomas Schiex},
title = {Solving Max-SAT as Weighted CSP},
booktitle = {CP},
year = {2003},
pages = {363-376},
ee = {http://dx.doi.org/10.1007/978-3-540-45193-8_25},
crossref = {DBLP:conf/cp/2003},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/mscs/LarrosaV02,
author = {Javier Larrosa and
Gabriel Valiente},
title = {Constraint Satisfaction Algorithms for Graph Pattern Matching},
journal = {Mathematical Structures in Computer Science},
volume = {12},
number = {4},
year = {2002},
pages = {403-422},
ee = {http://dx.doi.org/10.1017/S0960129501003577},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/iandc/Rubio02,
author = {Albert Rubio},
title = {A Fully Syntactic AC-RPO},
journal = {Inf. Comput.},
volume = {178},
number = {2},
year = {2002},
pages = {515-533},
ee = {http://dx.doi.org/10.1006/inco.2002.3158},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/iandc/NieuwenhuisR02,
author = {Robert Nieuwenhuis and
Jos{\'e} Miguel Rivero},
title = {Practical Algorithms for Deciding Path Ordering Constraint
Satisfaction},
journal = {Inf. Comput.},
volume = {178},
number = {2},
year = {2002},
pages = {422-440},
ee = {http://dx.doi.org/10.1006/inco.2002.3146},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/iandc/AtseriasBE02,
author = {Albert Atserias and
Maria Luisa Bonet and
Juan Luis Esteban},
title = {Lower Bounds for the Weak Pigeonhole Principle and Random
Formulas beyond Resolution},
journal = {Inf. Comput.},
volume = {176},
number = {2},
year = {2002},
pages = {136-152},
ee = {http://dx.doi.org/10.1006/inco.2002.3114},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/constraints/LarrosaM02,
author = {Javier Larrosa and
Pedro Meseguer},
title = {Partition-Based Lower Bound for Max-CSP},
journal = {Constraints},
volume = {7},
number = {3-4},
year = {2002},
pages = {407-419},
ee = {http://dx.doi.org/10.1023/A:1020510611031},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/aicom/Nieuwenhuis02,
author = {Robert Nieuwenhuis},
title = {The impact of CASC in the development of automated deduction
systems},
journal = {AI Commun.},
volume = {15},
number = {2-3},
year = {2002},
pages = {77-78},
ee = {http://iospress.metapress.com/content/4xx3xllg03vjgax3/},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/ai/BessiereMFL02,
author = {Christian Bessi{\`e}re and
Pedro Meseguer and
Eugene C. Freuder and
Javier Larrosa},
title = {On forward checking for non-binary constraint satisfaction},
journal = {Artif. Intell.},
volume = {141},
number = {1/2},
year = {2002},
pages = {205-224},
ee = {http://dx.doi.org/10.1016/S0004-3702(02)00263-1},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/icalp/EstebanGM02,
author = {Juan Luis Esteban and
Nicola Galesi and
Jochen Messner},
title = {On the Complexity of Resolution with Bounded Conjunctions},
booktitle = {ICALP},
year = {2002},
pages = {220-231},
ee = {http://dx.doi.org/10.1007/3-540-45465-9_20},
crossref = {DBLP:conf/icalp/2002},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/icalp/2002,
editor = {Peter Widmayer and
Francisco Triguero Ruiz and
Rafael Morales Bueno and
Matthew Hennessy and
Stephan Eidenbenz and
Ricardo Conejo},
title = {Automata, Languages and Programming, 29th International
Colloquium, ICALP 2002, Malaga, Spain, July 8-13, 2002,
Proceedings},
booktitle = {ICALP},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {2380},
year = {2002},
isbn = {3-540-43864-5},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/ecai/LarrosaMS02,
author = {Javier Larrosa and
Pedro Meseguer and
Mart\'{\i} S{\'a}nchez},
title = {Pseudo-tree Search with Soft Constraints},
booktitle = {ECAI},
year = {2002},
pages = {131-135},
crossref = {DBLP:conf/ecai/2002},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/ecai/2002,
editor = {Frank van Harmelen},
title = {Proceedings of the 15th Eureopean Conference on Artificial
Intelligence, ECAI'2002, Lyon, France, July 2002},
booktitle = {ECAI},
publisher = {IOS Press},
year = {2002},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/csl/AtseriasB02,
author = {Albert Atserias and
Maria Luisa Bonet},
title = {On the Automatizability of Resolution and Related Propositional
Proof Systems},
booktitle = {CSL},
year = {2002},
pages = {569-583},
ee = {http://dx.doi.org/10.1007/3-540-45793-3_38},
crossref = {DBLP:conf/csl/2002},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/csl/2002,
editor = {Julian C. Bradfield},
title = {Computer Science Logic, 16th International Workshop, CSL
2002, 11th Annual Conference of the EACSL, Edinburgh, Scotland,
UK, September 22-25, 2002, Proceedings},
booktitle = {CSL},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {2471},
year = {2002},
isbn = {3-540-44240-5},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/cade/BorrallerasLR02,
author = {Cristina Borralleras and
Salvador Lucas and
Albert Rubio},
title = {Recursive Path Orderings Can Be Context-Sensitive},
booktitle = {CADE},
year = {2002},
pages = {314-331},
ee = {http://dx.doi.org/10.1007/3-540-45620-1_27},
crossref = {DBLP:conf/cade/2002},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/cade/2002,
editor = {Andrei Voronkov},
title = {Automated Deduction - CADE-18, 18th International Conference
on Automated Deduction, Copenhagen, Denmark, July 27-30,
2002, Proceedings},
booktitle = {CADE},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {2392},
year = {2002},
isbn = {3-540-43931-5},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/cade/BofillR02,
author = {Miquel Bofill and
Albert Rubio},
title = {Well-Foundedness Is Sufficient for Completeness of Ordered
Paramodulation},
booktitle = {CADE},
year = {2002},
pages = {456-470},
ee = {http://dx.doi.org/10.1007/3-540-45620-1_36},
crossref = {DBLP:conf/cade/2002},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/amec/WillmottCR02,
author = {Steven Willmott and
Monique Calisti and
Emma Rollon},
title = {Challenges in Large-Scale Open Agent Mediated Economies},
booktitle = {AMEC},
year = {2002},
pages = {325-340},
ee = {http://dx.doi.org/10.1007/3-540-36378-5_20},
crossref = {DBLP:conf/amec/2002},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/amec/2002,
editor = {Julian A. Padget and
Onn Shehory and
David C. Parkes and
Norman M. Sadeh and
William E. Walsh},
title = {Agent-Mediated Electronic Commerce IV, Designing Mechanisms
and Systems, AAMAS 2002 Workshop on Agent Mediated Electronic
Commerce, Bologna, Italy, July 16, 2002, Revised Papers},
booktitle = {AMEC},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {2531},
year = {2002},
isbn = {3-540-00327-4},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/aaai/Larrosa02,
author = {Javier Larrosa},
title = {Node and Arc Consistency in Weighted CSP},
booktitle = {AAAI/IAAI},
year = {2002},
pages = {48-53},
ee = {http://www.aaai.org/Library/AAAI/2002/aaai02-008.php},
crossref = {DBLP:conf/aaai/2002},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/aaai/2002,
editor = {Rina Dechter and
Richard S. Sutton},
title = {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},
booktitle = {AAAI},
publisher = {AAAI Press / The MIT Press},
year = {2002},
ee = {http://www.aaai.org/Conferences/AAAI/aaai02.php},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/iandc/EstebanT01,
author = {Juan Luis Esteban and
Jacobo Tor{\'a}n},
title = {Space Bounds for Resolution},
journal = {Inf. Comput.},
volume = {171},
number = {1},
year = {2001},
pages = {84-97},
ee = {http://dx.doi.org/10.1006/inco.2001.2921},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/eatcs/BaumerET01,
author = {S. Baumer and
Juan Luis Esteban and
Jacobo Tor{\'a}n},
title = {Minimally Unsatisfiable CNF Formulas},
journal = {Bulletin of the EATCS},
volume = {74},
year = {2001},
pages = {190-192},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/cc/BonetG01,
author = {Maria Luisa Bonet and
Nicola Galesi},
title = {Optimality of size-width tradeoffs for resolution},
journal = {Computational Complexity},
volume = {10},
number = {4},
year = {2001},
pages = {261-276},
ee = {http://dx.doi.org/10.1007/s000370100000},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/lpar/BorrallerasR01,
author = {Cristina Borralleras and
Albert Rubio},
title = {A Monotonic Higher-Order Semantic Path Ordering},
booktitle = {LPAR},
year = {2001},
pages = {531-547},
ee = {http://dx.doi.org/10.1007/3-540-45653-8_37},
crossref = {DBLP:conf/lpar/2001},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/lpar/2001,
editor = {Robert Nieuwenhuis and
Andrei Voronkov},
title = {Logic for Programming, Artificial Intelligence, and Reasoning,
8th International Conference, LPAR 2001, Havana, Cuba, December
3-7, 2001, Proceedings},
booktitle = {LPAR},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {2250},
year = {2001},
isbn = {3-540-42957-3},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/lics/GodoyN01,
author = {Guillem Godoy and
Robert Nieuwenhuis},
title = {On Ordering Constraints for Deduction with Built-In Abelian
Semigroups, Monoids and Groups},
booktitle = {LICS},
year = {2001},
pages = {38-47},
ee = {http://doi.ieeecomputersociety.org/10.1109/LICS.2001.932481},
crossref = {DBLP:conf/lics/2001},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/lics/2001,
title = {16th Annual IEEE Symposium on Logic in Computer Science,
Boston, Massachusetts, USA, June 16-19, 2001, Proceedings},
booktitle = {LICS},
publisher = {IEEE Computer Society},
year = {2001},
isbn = {0-7695-1281-X},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/icalp/AtseriasBE01,
author = {Albert Atserias and
Maria Luisa Bonet and
Juan Luis Esteban},
title = {Lower Bounds for the Weak Pigeonhole Principle Beyond
Resolution},
booktitle = {ICALP},
year = {2001},
pages = {1005-1016},
ee = {http://dx.doi.org/10.1007/3-540-48224-5_81},
crossref = {DBLP:conf/icalp/2001},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/icalp/2001,
editor = {Fernando Orejas and
Paul G. Spirakis and
Jan van Leeuwen},
title = {Automata, Languages and Programming, 28th International
Colloquium, ICALP 2001, Crete, Greece, July 8-12, 2001,
Proceedings},
booktitle = {ICALP},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {2076},
year = {2001},
isbn = {3-540-42287-0},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/focs/ComonGN01,
author = {Hubert Comon and
Guillem Godoy and
Robert Nieuwenhuis},
title = {The Confluence of Ground Term Rewrite Systems is Decidable
in Polynomial Time},
booktitle = {FOCS},
year = {2001},
pages = {298-307},
ee = {http://doi.ieeecomputersociety.org/10.1109/SFCS.2001.959904},
crossref = {DBLP:conf/focs/2001},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/focs/2001,
title = {42nd Annual Symposium on Foundations of Computer Science,
FOCS 2001, 14-17 October 2001, Las Vegas, Nevada, USA},
booktitle = {FOCS},
publisher = {IEEE Computer Society},
year = {2001},
isbn = {0-7695-1390-5},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/cp/MeseguerLS01,
author = {Pedro Meseguer and
Javier Larrosa and
Mart\'{\i} S{\'a}nchez},
title = {Lower Bounds for Non-binary Constraint Optimization Problems},
booktitle = {CP},
year = {2001},
pages = {317-331},
ee = {http://dx.doi.org/10.1007/3-540-45578-7_22},
crossref = {DBLP:conf/cp/2001},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/cp/2001,
editor = {Toby Walsh},
title = {Principles and Practice of Constraint Programming - CP 2001,
7th International Conference, CP 2001, Paphos, Cyprus, November
26 - December 1, 2001, Proceedings},
booktitle = {CP},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {2239},
year = {2001},
isbn = {3-540-42863-1},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/cp/DechterKL01,
author = {Rina Dechter and
Kalev Kask and
Javier Larrosa},
title = {A General Scheme for Multiple Lower Bound Computation in
Constraint Optimization},
booktitle = {CP},
year = {2001},
pages = {346-360},
ee = {http://dx.doi.org/10.1007/3-540-45578-7_24},
crossref = {DBLP:conf/cp/2001},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/cade/NieuwenhuisHRV01,
author = {Robert Nieuwenhuis and
Thomas Hillenbrand and
Alexandre Riazanov and
Andrei Voronkov},
title = {On the Evaluation of Indexing Techniques for Theorem Proving},
booktitle = {IJCAR},
year = {2001},
pages = {257-271},
ee = {http://dx.doi.org/10.1007/3-540-45744-5_19},
crossref = {DBLP:conf/cade/2001},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/cade/2001,
editor = {Rajeev Gor{\'e} and
Alexander Leitsch and
Tobias Nipkow},
title = {Automated Reasoning, First International Joint Conference,
IJCAR 2001, Siena, Italy, June 18-23, 2001, Proceedings},
booktitle = {IJCAR},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {2083},
year = {2001},
isbn = {3-540-42254-4},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/cade/GanzingerNN01,
author = {Harald Ganzinger and
Robert Nieuwenhuis and
Pilar Nivela},
title = {Context Trees},
booktitle = {IJCAR},
year = {2001},
pages = {242-256},
ee = {http://dx.doi.org/10.1007/3-540-45744-5_18},
crossref = {DBLP:conf/cade/2001},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/siamcomp/BonetPR00,
author = {Maria Luisa Bonet and
Toniann Pitassi and
Ran Raz},
title = {On Interpolation and Automatization for Frege Systems},
journal = {SIAM J. Comput.},
volume = {29},
number = {6},
year = {2000},
pages = {1939-1967},
ee = {http://dx.doi.org/10.1137/S0097539798353230},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/siamcomp/BonetEGJ00,
author = {Maria Luisa Bonet and
Juan Luis Esteban and
Nicola Galesi and
Jan Johannsen},
title = {On the Relative Complexity of Resolution Refinements and
Cutting Planes Proof Systems},
journal = {SIAM J. Comput.},
volume = {30},
number = {5},
year = {2000},
pages = {1462-1484},
ee = {http://dx.doi.org/10.1137/S0097539799352474},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/iandc/ComonN00,
author = {Hubert Comon and
Robert Nieuwenhuis},
title = {Induction=I-Axiomatization+First-Order Consistency},
journal = {Inf. Comput.},
volume = {159},
number = {1-2},
year = {2000},
pages = {151-186},
ee = {http://dx.doi.org/10.1006/inco.2000.2875},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/lics/GodoyN00,
author = {Guillem Godoy and
Robert Nieuwenhuis},
title = {Paramodulation with Built-in Abelian Groups},
booktitle = {LICS},
year = {2000},
pages = {413-424},
ee = {http://doi.ieeecomputersociety.org/10.1109/LICS.2000.855788},
crossref = {DBLP:conf/lics/2000},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/lics/2000,
title = {15th Annual IEEE Symposium on Logic in Computer Science,
Santa Barbara, California, USA, June 26-29, 2000},
booktitle = {LICS},
publisher = {IEEE Computer Society},
year = {2000},
isbn = {0-7695-0725-5},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/frocos/BofillGNR00,
author = {Miquel Bofill and
Guillem Godoy and
Robert Nieuwenhuis and
Albert Rubio},
title = {Modular Redundancy for Theorem Proving},
booktitle = {FroCoS},
year = {2000},
pages = {186-199},
ee = {http://dx.doi.org/10.1007/10720084_13},
crossref = {DBLP:conf/frocos/2000},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/frocos/2000,
editor = {H{\'e}l{\`e}ne Kirchner and
Christophe Ringeissen},
title = {Frontiers of Combining Systems, Third International Workshop,
FroCoS 2000, Nancy, France, March 22-24, 2000, Proceedings},
booktitle = {FroCoS},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {1794},
year = {2000},
isbn = {3-540-67281-8},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/dna/DiazEO00,
author = {Sergio D\'{\i}az and
Juan Luis Esteban and
Mitsunori Ogihara},
title = {A DNA-Based Random Walk Method for Solving k-SAT},
booktitle = {DNA Computing},
year = {2000},
pages = {209-219},
ee = {http://dx.doi.org/10.1007/3-540-44992-2_14},
crossref = {DBLP:conf/dna/2000},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/dna/2000,
editor = {Anne Condon and
Grzegorz Rozenberg},
title = {DNA Computing, 6th International Workshop on DNA-Based
Computers,
DNA 2000, Leiden, The Netherlands, June 13-17, 2000, Revised
Papers},
booktitle = {DNA},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {2054},
year = {2001},
isbn = {3-540-42076-2},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/cp/Larrosa00,
author = {Javier Larrosa},
title = {Boosting Search with Variable Elimination},
booktitle = {CP},
year = {2000},
pages = {291-305},
ee = {http://dx.doi.org/10.1007/3-540-45349-0_22},
crossref = {DBLP:conf/cp/2000},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/cp/2000,
editor = {Rina Dechter},
title = {Principles and Practice of Constraint Programming - CP 2000,
6th International Conference, Singapore, September 18-21,
2000, Proceedings},
booktitle = {CP},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {1894},
year = {2000},
isbn = {3-540-41053-8},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/cade/BorrallerasFR00,
author = {Cristina Borralleras and
Maria Ferreira and
Albert Rubio},
title = {Complete Monotonic Semantic Path Orderings},
booktitle = {CADE},
year = {2000},
pages = {346-364},
ee = {http://dx.doi.org/10.1007/10721959_27},
crossref = {DBLP:conf/cade/2000},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/cade/2000,
editor = {David A. McAllester},
title = {Automated Deduction - CADE-17, 17th International Conference
on Automated Deduction, Pittsburgh, PA, USA, June 17-20,
2000, Proceedings},
booktitle = {CADE},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {1831},
year = {2000},
isbn = {3-540-67664-3},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/siamcomp/BonetPWY99,
author = {Maria Luisa Bonet and
Cynthia A. Phillips and
Tandy Warnow and
Shibu Yooseph},
title = {Constructing Evolutionary Trees in the Presence of Polymorphic
Characters},
journal = {SIAM J. Comput.},
volume = {29},
number = {1},
year = {1999},
pages = {103-131},
ee = {http://dx.doi.org/10.1137/S0097539796324636},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/ai/LarrosaMS99,
author = {Javier Larrosa and
Pedro Meseguer and
Thomas Schiex},
title = {Maintaining Reversible DAC for Max-CSP},
journal = {Artif. Intell.},
volume = {107},
number = {1},
year = {1999},
pages = {149-163},
ee = {http://dx.doi.org/10.1016/S0004-3702(98)00108-8},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/stacs/EstebanT99,
author = {Juan Luis Esteban and
Jacobo Tor{\'a}n},
title = {Space Bounds for Resolution},
booktitle = {STACS},
year = {1999},
pages = {551-560},
ee = {http://dx.doi.org/10.1007/3-540-49116-3_52},
crossref = {DBLP:conf/stacs/1999},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/stacs/1999,
editor = {Christoph Meinel and
Sophie Tison},
title = {STACS 99, 16th Annual Symposium on Theoretical Aspects of
Computer Science, Trier, Germany, March 4-6, 1999, Proceedings},
booktitle = {STACS},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {1563},
year = {1999},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/rta/Rubio99,
author = {Albert Rubio},
title = {A Fully Syntactic AC-RPO},
booktitle = {RTA},
year = {1999},
pages = {133-147},
ee = {http://dx.doi.org/10.1007/3-540-48685-2_11},
crossref = {DBLP:conf/rta/1999},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/rta/1999,
editor = {Paliath Narendran and
Micha{\"e}l Rusinowitch},
title = {Rewriting Techniques and Applications, 10th International
Conference, RTA-99, Trento, Italy, July 2-4, 1999, Proceedings},
booktitle = {RTA},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {1631},
year = {1999},
isbn = {3-540-66201-4},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/rta/NieuwenhuisR99,
author = {Robert Nieuwenhuis and
Jos{\'e} Miguel Rivero},
title = {Solved Forms for Path Ordering Constraints},
booktitle = {RTA},
year = {1999},
pages = {1-15},
ee = {http://dx.doi.org/10.1007/3-540-48685-2_1},
crossref = {DBLP:conf/rta/1999},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/lics/JouannaudR99,
author = {Jean-Pierre Jouannaud and
Albert Rubio},
title = {The Higher-Order Recursive Path Ordering},
booktitle = {LICS},
year = {1999},
pages = {402-411},
ee = {http://doi.ieeecomputersociety.org/10.1109/LICS.1999.782635},
crossref = {DBLP:conf/lics/1999},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/lics/1999,
title = {14th Annual IEEE Symposium on Logic in Computer Science,
Trento, Italy, July 2-5, 1999},
booktitle = {LICS},
publisher = {IEEE Computer Society},
year = {1999},
isbn = {0-7695-0158-3},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/lics/BofillGNR99,
author = {Miquel Bofill and
Guillem Godoy and
Robert Nieuwenhuis and
Albert Rubio},
title = {Paramodulation with Non-Monotonic Orderings},
booktitle = {LICS},
year = {1999},
pages = {225-233},
ee = {http://doi.ieeecomputersociety.org/10.1109/LICS.1999.782618},
crossref = {DBLP:conf/lics/1999},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/focs/BonetG99,
author = {Maria Luisa Bonet and
Nicola Galesi},
title = {A Study of Proof Search Algorithms for Resolution and Polynomial
Calculus},
booktitle = {FOCS},
year = {1999},
pages = {422-432},
ee = {http://doi.ieeecomputersociety.org/10.1109/SFFCS.1999.814614},
crossref = {DBLP:conf/focs/1999},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/focs/1999,
title = {40th Annual Symposium on Foundations of Computer Science,
FOCS '99, 17-18 October, 1999, New York, NY, USA},
booktitle = {FOCS},
publisher = {IEEE Computer Society},
year = {1999},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/cp/LarrosaM99,
author = {Javier Larrosa and
Pedro Meseguer},
title = {Partition-Based Lower Bound for Max-CSP},
booktitle = {CP},
year = {1999},
pages = {303-315},
ee = {http://dx.doi.org/10.1007/978-3-540-48085-3_22},
crossref = {DBLP:conf/cp/1999},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/cp/1999,
editor = {Joxan Jaffar},
title = {Principles and Practice of Constraint Programming - CP'99,
5th International Conference, Alexandria, Virginia, USA,
October 11-14, 1999, Proceedings},
booktitle = {CP},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {1713},
year = {1999},
isbn = {3-540-66626-5},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/cp/BessiereMFL99,
author = {Christian Bessi{\`e}re and
Pedro Meseguer and
Eugene C. Freuder and
Javier Larrosa},
title = {On Forward Checking for Non-binary Constraint Satisfaction},
booktitle = {CP},
year = {1999},
pages = {88-102},
crossref = {DBLP:conf/cp/1999},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/coco/BonetDGMP99,
author = {Maria Luisa Bonet and
Carlos Domingo and
Ricard Gavald{\`a} and
Alexis Maciel and
Toniann Pitassi},
title = {Non-Automatizability of Bounded-Depth Frege Proofs},
booktitle = {IEEE Conference on Computational Complexity},
year = {1999},
pages = {15-23},
ee = {http://doi.ieeecomputersociety.org/10.1109/CCC.1999.766258},
crossref = {DBLP:conf/coco/1999},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/coco/1999,
title = {Proceedings of the 14th Annual IEEE Conference on Computational
Complexity, Atlanta, Georgia, USA, May 4-6, 1999},
booktitle = {IEEE Conference on Computational Complexity},
publisher = {IEEE Computer Society},
year = {1999},
isbn = {0-7695-0075-7},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/ccl/GanzingerN99,
author = {Harald Ganzinger and
Robert Nieuwenhuis},
title = {Constraints and Theorem Proving},
booktitle = {CCL},
year = {1999},
pages = {159-201},
ee = {http://dx.doi.org/10.1007/3-540-45406-3_4},
crossref = {DBLP:conf/ccl/1999},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/ccl/1999,
editor = {Hubert Comon and
Claude March{\'e} and
Ralf Treinen},
title = {Constraints in Computational Logics: Theory and Applications,
International Summer School, CCL'99 Gif-sur-Yvette, France,
September 5-8, 1999, Revised Lectures},
booktitle = {CCL},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {2002},
year = {2001},
isbn = {3-540-41950-0},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/cade/Nieuwenhuis99,
author = {Robert Nieuwenhuis},
title = {Invited Talk: Rewrite-based Deduction and Symbolic Constraints},
booktitle = {CADE},
year = {1999},
pages = {302-313},
ee = {http://dx.doi.org/10.1007/3-540-48660-7_28},
crossref = {DBLP:conf/cade/1999},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/cade/1999,
editor = {Harald Ganzinger},
title = {Automated Deduction - CADE-16, 16th International Conference
on Automated Deduction, Trento, Italy, July 7-10, 1999,
Proceedings},
booktitle = {CADE},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {1632},
year = {1999},
isbn = {3-540-66222-7},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/tcs/JouannaudR98,
author = {Jean-Pierre Jouannaud and
Albert Rubio},
title = {Rewrite Orderings for Higher-Order Terms in eta-Long beta-Normal
Form and Recursive Path Ordering},
journal = {Theor. Comput. Sci.},
volume = {208},
number = {1-2},
year = {1998},
pages = {33-58},
ee = {http://dx.doi.org/10.1016/S0304-3975(98)00078-4},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/jcb/BonetSWY98,
author = {Maria Luisa Bonet and
Mike A. Steel and
Tandy Warnow and
Shibu Yooseph},
title = {Better Methods for Solving Parsimony and Compatibility},
journal = {Journal of Computational Biology},
volume = {5},
number = {3},
year = {1998},
pages = {391-407},
ee = {http://dx.doi.org/10.1089/cmb.1998.5.391},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/iandc/Nieuwenhuis98,
author = {Robert Nieuwenhuis},
title = {Decidability and Complexity Analysis by Basic Paramodulation},
journal = {Inf. Comput.},
volume = {147},
number = {1},
year = {1998},
pages = {1-21},
ee = {http://dx.doi.org/10.1006/inco.1998.2730},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/recomb/BonetSWY98,
author = {Maria Luisa Bonet and
Mike A. Steel and
Tandy Warnow and
Shibu Yooseph},
title = {Better methods for solving parsimony and compatibility},
booktitle = {RECOMB},
year = {1998},
pages = {40-49},
ee = {http://doi.acm.org/10.1145/279069.279081},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/lics/ComonNNR98,
author = {Hubert Comon and
Paliath Narendran and
Robert Nieuwenhuis and
Micha{\"e}l Rusinowitch},
title = {Decision Problems in Ordered Rewriting},
booktitle = {LICS},
year = {1998},
pages = {276-286},
ee = {http://doi.ieeecomputersociety.org/10.1109/LICS.1998.705664},
crossref = {DBLP:conf/lics/1998},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/lics/1998,
title = {Thirteenth Annual IEEE Symposium on Logic in Computer Science,
Indianapolis, Indiana, USA, June 21-24, 1998},
booktitle = {LICS},
publisher = {IEEE Computer Society},
year = {1998},
isbn = {0-8186-8506-9},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/ieaaie/LarrosaM98,
author = {Javier Larrosa and
Pedro Meseguer},
title = {Generic CSP Techniques for the Job-Shop Problem},
booktitle = {IEA/AIE (Vol. 2)},
year = {1998},
pages = {46-55},
ee = {http://dx.doi.org/10.1007/3-540-64574-8_390},
crossref = {DBLP:conf/ieaaie/1998-2},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/ieaaie/1998-2,
editor = {Angel P. Del Pobil and
Jos{\'e} Mira and
Moonis Ali},
title = {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{\'o}n, Spain, June 1-4, 1998, Proceedings, Volume
II},
booktitle = {IEA/AIE (Vol. 2)},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {1416},
year = {1998},
isbn = {3-540-64574-8},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/focs/BonetEGJ98,
author = {Maria Luisa Bonet and
Juan Luis Esteban and
Nicola Galesi and
Jan Johannsen},
title = {Exponential Separations between Restricted Resolution and
Cutting Planes Proof Systems},
booktitle = {FOCS},
year = {1998},
pages = {638-647},
ee = {http://doi.ieeecomputersociety.org/10.1109/SFCS.1998.743514},
crossref = {DBLP:conf/focs/1998},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/focs/1998,
title = {39th Annual Symposium on Foundations of Computer Science,
FOCS '98, November 8-11, 1998, Palo Alto, California, USA},
booktitle = {FOCS},
publisher = {IEEE Computer Society},
year = {1998},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/ecai/LarrosaM98,
author = {Javier Larrosa and
Pedro Meseguer},
title = {Partial Lazy Forward Checking for MAX-CSP},
booktitle = {ECAI},
year = {1998},
pages = {229-233},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/aaai/LarrosaMSV98,
author = {Javier Larrosa and
Pedro Meseguer and
Thomas Schiex and
G{\'e}rard Verfaillie},
title = {Reversible DAC and Other Improvements for Solving Max-CSP},
booktitle = {AAAI/IAAI},
year = {1998},
pages = {347-352},
ee = {http://www.aaai.org/Library/AAAI/1998/aaai98-049.php},
crossref = {DBLP:conf/aaai/1998},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/aaai/1998,
editor = {Jack Mostow and
Chuck Rich},
title = {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},
booktitle = {AAAI},
publisher = {AAAI Press / The MIT Press},
year = {1998},
isbn = {0-262-51098-7},
ee = {http://www.aaai.org/Conferences/AAAI/aaai98.php},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/jsyml/BonetPR97,
author = {Maria Luisa Bonet and
Toniann Pitassi and
Ran Raz},
title = {Lower Bounds for Cutting Planes Proofs with Small Coefficients},
journal = {J. Symb. Log.},
volume = {62},
number = {3},
year = {1997},
pages = {708-728},
ee = {http://projecteuclid.org/euclid.jsl/1183745294},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/jsc/NieuwenhuisR97,
author = {Robert Nieuwenhuis and
Albert Rubio},
title = {Paramodulation with Built-in AC-Theories and Symbolic
Constraints},
journal = {J. Symb. Comput.},
volume = {23},
number = {1},
year = {1997},
pages = {1-21},
ee = {http://dx.doi.org/10.1006/jsco.1996.0074},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/jar/NieuwenhuisRV97,
author = {Robert Nieuwenhuis and
Jos{\'e} Miguel Rivero and
Miguel {\'A}ngel Vallejo},
title = {Barcelona},
journal = {J. Autom. Reasoning},
volume = {18},
number = {2},
year = {1997},
pages = {171-176},
ee = {http://dx.doi.org/10.1023/A:1005862710017},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/ijcai/Larrosa97,
author = {Javier Larrosa},
title = {Merging Constraint Satisfaction Subproblems to Avoid Redundant
Search},
booktitle = {IJCAI (1)},
year = {1997},
pages = {424-433},
crossref = {DBLP:conf/ijcai/1997},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/ijcai/1997,
title = {Proceedings of the Fifteenth International Joint Conference
on Artificial Intelligence, IJCAI 97, Nagoya, Japan, August
23-29, 1997, 2 Volumes},
booktitle = {IJCAI},
publisher = {Morgan Kaufmann},
year = {1997},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/focs/BonetPR97,
author = {Maria Luisa Bonet and
Toniann Pitassi and
Ran Raz},
title = {No Feasible Interpolation for TC0-Frege Proofs},
booktitle = {FOCS},
year = {1997},
pages = {254-263},
ee = {http://doi.ieeecomputersociety.org/10.1109/SFCS.1997.646114},
crossref = {DBLP:conf/focs/1997},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/focs/1997,
title = {38th Annual Symposium on Foundations of Computer Science,
FOCS '97, Miami Beach, Florida, USA, October 19-22, 1997},
booktitle = {FOCS},
publisher = {IEEE Computer Society},
year = {1997},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/csl/BonetG97,
author = {Maria Luisa Bonet and
Nicola Galesi},
title = {Linear Lower Bounds and Simulations in Frege Systems with
Substitutions},
booktitle = {CSL},
year = {1997},
pages = {115-128},
ee = {http://dx.doi.org/10.1007/BFb0028010},
crossref = {DBLP:conf/csl/1997},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/csl/1997,
editor = {Mogens Nielsen and
Wolfgang Thomas},
title = {Computer Science Logic, 11th International Workshop, CSL
'97, Annual Conference of the EACSL, Aarhus, Denmark, August
23-29, 1997, Selected Papers},
booktitle = {CSL},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {1414},
year = {1998},
isbn = {3-540-64570-5},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/cade/NieuwenhuisRV97,
author = {Robert Nieuwenhuis and
Jos{\'e} Miguel Rivero and
Miguel {\'A}ngel Vallejo},
title = {Dedan: A Kernel of Data Structures and Algorithms for Automated
Deduction with Equality Clauses},
booktitle = {CADE},
year = {1997},
pages = {49-52},
ee = {http://dx.doi.org/10.1007/3-540-63104-6_5},
crossref = {DBLP:conf/cade/1997},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/cade/1997,
editor = {William McCune},
title = {Automated Deduction - CADE-14, 14th International Conference
on Automated Deduction, Townsville, North Queensland, Australia,
July 13-17, 1997, Proceedings},
booktitle = {CADE},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {1249},
year = {1997},
isbn = {3-540-63104-6},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/stoc/BonetPWY96,
author = {Maria Luisa Bonet and
Cynthia A. Phillips and
Tandy Warnow and
Shibu Yooseph},
title = {Constructing Evolutionary Trees in the Presence of Polymorphic
Characters},
booktitle = {STOC},
year = {1996},
pages = {220-229},
ee = {http://doi.acm.org/10.1145/237814.237867},
crossref = {DBLP:conf/stoc/1996},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/stoc/1996,
editor = {Gary L. Miller},
title = {Proceedings of the Twenty-Eighth Annual ACM Symposium on
the Theory of Computing, Philadelphia, Pennsylvania, USA,
May 22-24, 1996},
booktitle = {STOC},
publisher = {ACM},
year = {1996},
isbn = {0-89791-785-5},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/rta/JouannaudR96,
author = {Jean-Pierre Jouannaud and
Albert Rubio},
title = {A Recursive Path Ordering for Higher-Order Terms in {\it eta}-
Long
{\it beta}-Normal Form},
booktitle = {RTA},
year = {1996},
pages = {108-122},
ee = {http://dx.doi.org/10.1007/3-540-61464-8_46},
crossref = {DBLP:conf/rta/1996},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/rta/1996,
editor = {Harald Ganzinger},
title = {Rewriting Techniques and Applications, 7th International
Conference, RTA-96, New Brunswick, NJ, USA, July 27-30,
1996, Proceedings},
booktitle = {RTA},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {1103},
year = {1996},
isbn = {3-540-61464-8},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/lics/Nieuwenhuis96,
author = {Robert Nieuwenhuis},
title = {Basic Paramodulation and Decidable Theories (Extended
Abstract)},
booktitle = {LICS},
year = {1996},
pages = {473-482},
ee = {http://doi.ieeecomputersociety.org/10.1109/LICS.1996.561464},
crossref = {DBLP:conf/lics/1996},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/lics/1996,
title = {Proceedings, 11th Annual IEEE Symposium on Logic in Computer
Science, New Brunswick, New Jersey, USA, July 27-30, 1996},
booktitle = {LICS},
publisher = {IEEE Computer Society},
year = {1996},
isbn = {0-8186-7463-6},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/ecai/LarrosaM96,
author = {Javier Larrosa and
Pedro Meseguer},
title = {Phase Transition in MAX-CSP},
booktitle = {ECAI},
year = {1996},
pages = {190-194},
crossref = {DBLP:conf/ecai/1996},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/ecai/1996,
editor = {Wolfgang Wahlster},
title = {12th European Conference on Artificial Intelligence, Budapest,
Hungary, August 11-16, 1996, Proceedings},
booktitle = {ECAI},
publisher = {John Wiley and Sons, Chichester},
year = {1996},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/cp/LarrosaM96,
author = {Javier Larrosa and
Pedro Meseguer},
title = {Exploiting the Use of DAC in MAX-CSP},
booktitle = {CP},
year = {1996},
pages = {308-322},
ee = {http://dx.doi.org/10.1007/3-540-61551-2_83},
crossref = {DBLP:conf/cp/1996},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/cp/1996,
editor = {Eugene C. Freuder},
title = {Proceedings of the Second International Conference on Principles
and Practice of Constraint Programming, Cambridge,
Massachusetts,
USA, August 19-22, 1996},
booktitle = {CP},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {1118},
year = {1996},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/agp/NieuwenhuisRV96,
author = {Robert Nieuwenhuis and
Jos{\'e} Miguel Rivero and
Miguel {\'A}ngel Vallejo},
title = {An Implementation Kernel for Theorem Proving with Equality
Clauses},
booktitle = {APPIA-GULP-PRODE},
year = {1996},
pages = {89-104},
crossref = {DBLP:conf/agp/1996},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/agp/1996,
editor = {Paqui Lucio and
Maurizio Martelli and
Marisa Navarro},
title = {1996 Joint Conf. on Declarative Programming, APPIA-GULP-
PRODE'96,
Donostia-San Sebastian, Spain, July 15-18, 1996},
booktitle = {APPIA-GULP-PRODE},
year = {1996},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/tcs/RubioN95,
author = {Albert Rubio and
Robert Nieuwenhuis},
title = {A Total AC-Compatible Ordering Based on RPO},
journal = {Theor. Comput. Sci.},
volume = {142},
number = {2},
year = {1995},
pages = {209-227},
ee = {http://dx.doi.org/10.1016/0304-3975(94)00276-2},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/siamcomp/BonetB95,
author = {Maria Luisa Bonet and
Samuel R. Buss},
title = {The Serial Transitive Closure Problem for Trees},
journal = {SIAM J. Comput.},
volume = {24},
number = {1},
year = {1995},
pages = {109-122},
ee = {http://dx.doi.org/10.1137/S0097539792225303},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/jsc/NieuwenhuisR95,
author = {Robert Nieuwenhuis and
Albert Rubio},
title = {Theorem Proving with Ordering and Equality Constrained Clauses},
journal = {J. Symb. Comput.},
volume = {19},
number = {4},
year = {1995},
pages = {321-351},
ee = {http://dx.doi.org/10.1006/jsco.1995.1020},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/aicom/LarrosaC95,
author = {Javier Larrosa and
Ulises Cort{\'e}s},
title = {A Framework for Abductive Rule Formation},
journal = {AI Commun.},
volume = {8},
number = {2},
year = {1995},
pages = {91-100},
ee = {http://dx.doi.org/10.3233/AIC-1995-8204},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/stoc/BonetPR95,
author = {Maria Luisa Bonet and
Toniann Pitassi and
Ran Raz},
title = {Lower bounds for cutting planes proofs with small coefficients},
booktitle = {STOC},
year = {1995},
pages = {575-584},
ee = {http://doi.acm.org/10.1145/225058.225275},
crossref = {DBLP:conf/stoc/STOC27},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/stoc/STOC27,
editor = {Frank Thomson Leighton and
Allan Borodin},
title = {Proceedings of the Twenty-Seventh Annual ACM Symposium on
Theory of Computing, 29 May-1 June 1995, Las Vegas, Nevada,
USA},
booktitle = {STOC},
publisher = {ACM},
year = {1995},
isbn = {0-89791-718-9},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/rta/Nieuwenhuis95,
author = {Robert Nieuwenhuis},
title = {On Narrowing, Refutation Proofs and Constraints},
booktitle = {RTA},
year = {1995},
pages = {56-70},
ee = {http://dx.doi.org/10.1007/3-540-59200-8_47},
crossref = {DBLP:conf/rta/1995},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/rta/1995,
editor = {Jieh Hsiang},
title = {Rewriting Techniques and Applications, 6th International
Conference, RTA-95, Kaiserslautern, Germany, April 5-7,
1995, Proceedings},
booktitle = {RTA},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {914},
year = {1995},
isbn = {3-540-59200-8},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/lics/ComonNR95,
author = {Hubert Comon and
Robert Nieuwenhuis and
Albert Rubio},
title = {Orderings, AC-Theories and Symbolic Constraint Solving (Extended
Abstract)},
booktitle = {LICS},
year = {1995},
pages = {375-385},
ee = {http://doi.ieeecomputersociety.org/10.1109/LICS.1995.523272},
crossref = {DBLP:conf/lics/1995},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/lics/1995,
title = {Proceedings, 10th Annual IEEE Symposium on Logic in Computer
Science, San Diego, California, USA, June 26-29, 1995},
booktitle = {LICS},
publisher = {IEEE Computer Society},
year = {1995},
isbn = {0-8186-7050-9},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/ijcai/MeseguerL95,
author = {Pedro Meseguer and
Javier Larrosa},
title = {Constraint Satisfaction as Global Optimization},
booktitle = {IJCAI (1)},
year = {1995},
pages = {579-585},
crossref = {DBLP:conf/ijcai/1995},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/ijcai/1995,
title = {Proceedings of the Fourteenth International Joint Conference
on Artificial Intelligence, IJCAI 95, Montr{\'e}al Qu{\'e}bec,
Canada, August 20-25 1995, 2 Volumes},
booktitle = {IJCAI},
publisher = {Morgan Kaufmann},
year = {1995},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/icalp/Rubio95,
author = {Albert Rubio},
title = {Extension Orderings},
booktitle = {ICALP},
year = {1995},
pages = {511-522},
ee = {http://dx.doi.org/10.1007/3-540-60084-1_101},
crossref = {DBLP:conf/icalp/1995},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/icalp/1995,
editor = {Zolt{\'a}n F{\"u}l{\"o}p and
Ferenc G{\'e}cseg},
title = {Automata, Languages and Programming, 22nd International
Colloquium, ICALP95, Szeged, Hungary, July 10-14, 1995,
Proceedings},
booktitle = {ICALP},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {944},
year = {1995},
isbn = {3-540-60084-1},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/csl/Rubio95,
author = {Albert Rubio},
title = {Theorem Proving modulo Associativity},
booktitle = {CSL},
year = {1995},
pages = {452-467},
ee = {http://dx.doi.org/10.1007/3-540-61377-3_53},
crossref = {DBLP:conf/csl/1995},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/csl/1995,
editor = {Hans Kleine B{\"u}ning},
title = {Computer Science Logic, 9th International Workshop, CSL
'95, Annual Conference of the EACSL, Paderborn, Germany,
September 22-29, 1995, Selected Papers},
booktitle = {CSL},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {1092},
year = {1996},
isbn = {3-540-61377-3},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/cp/LarrosaM95,
author = {Javier Larrosa and
Pedro Meseguer},
title = {Optimization-based Heuristics for Maximal Constraint
Satisfaction},
booktitle = {CP},
year = {1995},
pages = {103-120},
ee = {http://dx.doi.org/10.1007/3-540-60299-2_7},
crossref = {DBLP:conf/cp/1995},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/cp/1995,
editor = {Ugo Montanari and
Francesca Rossi},
title = {Principles and Practice of Constraint Programming - CP'95,
First International Conference, CP'95, Cassis, France, September
19-22, 1995, Proceedings},
booktitle = {CP},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {976},
year = {1995},
isbn = {3-540-60299-2},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/ipl/BonetB94,
author = {Maria Luisa Bonet and
Samuel R. Buss},
title = {Size-Depth Tradeoffs for Boolean Fomulae},
journal = {Inf. Process. Lett.},
volume = {49},
number = {3},
year = {1994},
pages = {151-155},
ee = {http://dx.doi.org/10.1016/0020-0190(94)90093-0},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/cade/NieuwenhuisR94,
author = {Robert Nieuwenhuis and
Albert Rubio},
title = {AC-Superposition with Constraints: No AC-Unifiers Needed},
booktitle = {CADE},
year = {1994},
pages = {545-559},
ee = {http://dx.doi.org/10.1007/3-540-58156-1_40},
crossref = {DBLP:conf/cade/1994},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/cade/1994,
editor = {Alan Bundy},
title = {Automated Deduction - CADE-12, 12th International Conference
on Automated Deduction, Nancy, France, June 26 - July 1,
1994, Proceedings},
booktitle = {CADE},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {814},
year = {1994},
isbn = {3-540-58156-1},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/jsyml/BonetB93,
author = {Maria Luisa Bonet and
Samuel R. Buss},
title = {The Deduction Rule and Linear and Near-Linear Proof
Simulations},
journal = {J. Symb. Log.},
volume = {58},
number = {2},
year = {1993},
pages = {688-709},
ee = {http://projecteuclid.org/euclid.jsl/1183744256},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/ipl/Nieuwenhuis93,
author = {Robert Nieuwenhuis},
title = {Simple LPO Constraint Solving Methods},
journal = {Inf. Process. Lett.},
volume = {47},
number = {2},
year = {1993},
pages = {65-69},
ee = {http://dx.doi.org/10.1016/0020-0190(93)90226-Y},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/rta/RubioN93,
author = {Albert Rubio and
Robert Nieuwenhuis},
title = {A Precedence-Based Total AC-Compatible Ordering},
booktitle = {RTA},
year = {1993},
pages = {374-388},
ee = {http://dx.doi.org/10.1007/3-540-56868-9_28},
crossref = {DBLP:conf/rta/1993},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/rta/1993,
editor = {Claude Kirchner},
title = {Rewriting Techniques and Applications, 5th International
Conference, RTA-93, Montreal, Canada, June 16-18, 1993,
Proceedings},
booktitle = {RTA},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {690},
year = {1993},
isbn = {3-540-56868-9},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/rta/NivelaN93,
author = {Pilar Nivela and
Robert Nieuwenhuis},
title = {Saturation of First-Order (Constrained) Clauses with the
{\it Saturate} System},
booktitle = {RTA},
year = {1993},
pages = {436-440},
ee = {http://dx.doi.org/10.1007/3-540-56868-9_33},
crossref = {DBLP:conf/rta/1993},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/prospectra/BertlingGSNO93,
author = {Hubert Bertling and
Harald Ganzinger and
Renate Sch{\"a}fers and
Robert Nieuwenhuis and
Fernando Orejas},
title = {Program Development: Completion Subsystem},
booktitle = {PROSPECTRA Book},
year = {1993},
pages = {460-494},
ee = {http://dx.doi.org/10.1007/3-540-56733-X_162},
crossref = {DBLP:conf/prospectra/1993},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/prospectra/1993,
editor = {Berthold Hoffmann and
Bernd Krieg-Br{\"u}ckner},
title = {Program Development by Specification and Transformation,
The PROSPECTRA Methodology, Language Family, and System},
booktitle = {PROSPECTRA Book},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {680},
year = {1993},
isbn = {3-540-56733-X},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/esop/NieuwenhuisR92,
author = {Robert Nieuwenhuis and
Albert Rubio},
title = {Basic Superposition is Complete},
booktitle = {ESOP},
year = {1992},
pages = {371-389},
ee = {http://dx.doi.org/10.1007/3-540-55253-7_22},
crossref = {DBLP:conf/esop/1992},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/esop/1992,
editor = {Bernd Krieg-Br{\"u}ckner},
title = {ESOP '92, 4th European Symposium on Programming, Rennes,
France, February 26-28, 1992, Proceedings},
booktitle = {ESOP},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {582},
year = {1992},
isbn = {3-540-55253-7},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/cade/NieuwenhuisR92,
author = {Robert Nieuwenhuis and
Albert Rubio},
title = {Theorem Proving with Ordering Constrained Clauses},
booktitle = {CADE},
year = {1992},
pages = {477-491},
ee = {http://dx.doi.org/10.1007/3-540-55602-8_186},
crossref = {DBLP:conf/cade/1992},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/cade/1992,
editor = {Deepak Kapur},
title = {Automated Deduction - CADE-11, 11th International Conference
on Automated Deduction, Saratoga Springs, NY, USA, June
15-18, 1992, Proceedings},
booktitle = {CADE},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {607},
year = {1992},
isbn = {3-540-55602-8},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/ipl/NieuwenhuisN91,
author = {Robert Nieuwenhuis and
Pilar Nivela},
title = {Efficient Deduction in Equality Horn Logic by Horn-Completion},
journal = {Inf. Process. Lett.},
volume = {39},
number = {1},
year = {1991},
pages = {1-6},
ee = {http://dx.doi.org/10.1016/0020-0190(91)90053-K},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/lics/BonetB91,
author = {Maria Luisa Bonet and
Samuel R. Buss},
title = {On the Deduction Rule and the Number of Proof Lines},
booktitle = {LICS},
year = {1991},
pages = {286-297},
ee = {http://dx.doi.org/10.1109/LICS.1991.151653},
crossref = {DBLP:conf/lics/1991},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/lics/1991,
title = {Proceedings of the Sixth Annual Symposium on Logic in Computer
Science (LICS '91), Amsterdam, The Netherlands, July 15-18,
1991},
booktitle = {LICS},
publisher = {IEEE Computer Society},
year = {1991},
isbn = {0-8186-2230-X},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/interspeech/LleidaMNO91,
author = {Eduardo Lleida and
Jos{\'e} B. Mari{\~n}o and
Climent Nadeu and
Albert Oliveras},
title = {Two level continuous speech recognition using demisyllable-based
HMM word spotting},
booktitle = {EUROSPEECH},
year = {1991},
ee = {http://www.isca-speech.org/archive/eurospeech_1991/
e91_1199.html},
crossref = {DBLP:conf/interspeech/1991},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/interspeech/1991,
title = {Second European Conference on Speech Communication and
Technology,
EUROSPEECH 1991, Genova, Italy, September 24-26, 1991},
booktitle = {EUROSPEECH},
publisher = {ISCA},
year = {1991},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/ctrs/NieuwenhuisO90,
author = {Robert Nieuwenhuis and
Fernando Orejas},
title = {Clausal Rewriting},
booktitle = {CTRS},
year = {1990},
pages = {246-258},
ee = {http://dx.doi.org/10.1007/3-540-54317-1_95},
crossref = {DBLP:conf/ctrs/1990},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/ctrs/1990,
editor = {St{\'e}phane Kaplan and
Mitsuhiro Okada},
title = {Conditional and Typed Rewriting Systems, 2nd International
CTRS Workshop, Montreal, Canada, June 11-14, 1990, Proceedings},
booktitle = {CTRS},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {516},
year = {1991},
isbn = {3-540-54317-1},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/cade/NieuwenhuisOR90,
author = {Robert Nieuwenhuis and
Fernando Orejas and
Albert Rubio},
title = {TRIP: An Implementation of Clausal Rewriting},
booktitle = {CADE},
year = {1990},
pages = {667-668},
ee = {http://dx.doi.org/10.1007/3-540-52885-7_133},
crossref = {DBLP:conf/cade/1990},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/cade/1990,
editor = {Mark E. Stickel},
title = {10th International Conference on Automated Deduction,
Kaiserslautern,
FRG, July 24-27, 1990, Proceedings},
booktitle = {CADE},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {449},
year = {1990},
isbn = {3-540-52885-7},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/adt/OrejasN90,
author = {Fernando Orejas and
Pilar Nivela},
title = {Constraints for Behavioural Specifications},
booktitle = {ADT},
year = {1990},
pages = {220-245},
ee = {http://dx.doi.org/10.1007/3-540-54496-8_12},
crossref = {DBLP:conf/adt/1990},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/adt/1990,
editor = {Hartmut Ehrig and
Klaus P. Jantke and
Fernando Orejas and
Horst Reichel},
title = {Recent Trends in Data Type Specification, Proceedings 7th
Workshop on Abstract Data Types, Wusterhausen, Dosse, Germany,
April 17-20, 1990},
booktitle = {ADT},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {534},
year = {1991},
isbn = {3-540-54496-8},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/adt/NieuwenhuisO90,
author = {Robert Nieuwenhuis and
Fernando Orejas},
title = {Clausal Rewriting: Applications and Implementation},
booktitle = {ADT},
year = {1990},
pages = {204-219},
ee = {http://dx.doi.org/10.1007/3-540-54496-8_11},
crossref = {DBLP:conf/adt/1990},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/category/OrejasNE88,
author = {Fernando Orejas and
Pilar Nivela and
Hartmut Ehrig},
title = {Semantical Constructions for Categories of Behavioural
Specifications},
booktitle = {Categorial Methods in Computer Science},
year = {1988},
pages = {220-243},
crossref = {DBLP:conf/category/1988},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/category/1988,
editor = {Hartmut Ehrig and
Horst Herrlich and
Hans-J{\"o}rg Kreowski and
Gerhard Preu{\ss}},
title = {Categorial Methods in Computer Science: With Aspects from
Topology [Workshop, September 1988, Berlin, Germany]},
booktitle = {Categorial Methods in Computer Science},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {393},
year = {1989},
isbn = {3-540-51722-7},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/adt/OrejasSNNP88,
author = {Fernando Orejas and
Ana S{\'a}nchez and
Marisa Navarro and
Pilar Nivela and
Ricardo Pena},
title = {Term Rewriting Methods for Partial Specifications},
booktitle = {ADT},
year = {1988},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/adt/NivelaO88,
author = {Pilar Nivela and
Fernando Orejas},
title = {A Module Concept within the Initial Behaviour Framework},
booktitle = {ADT},
year = {1988},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/adt/NivelaO87,
author = {Pilar Nivela and
Fernando Orejas},
title = {Initial Behaviour Semantics for Algebraic Specifications},
booktitle = {ADT},
year = {1987},
pages = {184-207},
ee = {http://dx.doi.org/10.1007/3-540-50325-0_10},
crossref = {DBLP:conf/adt/1987},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/adt/1987,
editor = {Donald Sannella and
Andrzej Tarlecki},
title = {Recent Trends in Data Type Specification, 5th Workshop on
Abstract Data Types, Gullane, Scotland, September 1-4, 1987,
Selected Papers},
booktitle = {ADT},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {332},
year = {1987},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/eccc/ECCC-TR03-044,
author = {Juan Luis Esteban and
Jacobo Tor{\'a}n},
title = {A Combinatorial Characterization of Treelike Resolution
Space},
journal = {Electronic Colloquium on Computational Complexity (ECCC)},
number = {044},
year = {2003},
ee = {http://eccc.hpi-web.de/eccc-reports/2003/TR03-044/index.html},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/eccc/ECCC-TR03-041,
author = {Albert Atserias and
Maria Luisa Bonet and
Jordi Levy},
title = {On Chvatal Rank and Cutting Planes Proofs},
journal = {Electronic Colloquium on Computational Complexity (ECCC)},
number = {041},
year = {2003},
ee = {http://eccc.hpi-web.de/eccc-reports/2003/TR03-041/index.html},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/aepia/LarrosaM03a,
author = {Javier Larrosa and
Pedro Meseguer},
title = {Restricciones Blanda: Modelos y Algoritmos},
journal = {Inteligencia Artificial, Revista Iberoamericana de Inteligencia
Artificial},
volume = {7},
number = {20},
year = {2003},
pages = {69-82},
ee = {http://polar.lsi.uned.es/revista/index.php/ia/article/view/376},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/eccc/ECCC-TR98-035,
author = {Maria Luisa Bonet and
Juan Luis Esteban and
Nicola Galesi and
Jan Johannsen},
title = {Exponential Separations between Restricted Resolution and
Cutting Planes Proof Systems},
journal = {Electronic Colloquium on Computational Complexity (ECCC)},
volume = {5},
number = {35},
year = {1998},
ee = {http://eccc.hpi-web.de/eccc-reports/1998/TR98-035/index.html},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
This file was generated by bibtex2html 1.96.