Please note: This is a beta version of the new dblp website.
You can find the classic dblp view of this page here.
You can find the classic dblp view of this page here.
Robert Nieuwenhuis
2010 – today
- 2013
[c54]Deepak Kapur, Robert Nieuwenhuis, Andrei Voronkov, Christoph Weidenbach, Reinhard Wilhelm: Harald Ganzinger's Legacy: Contributions to Logics and Programming. Programming Logics 2013: 1-18- [c53]Ignasi Abío, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell: A Parametric Approach for Smaller and Better Encodings of Cardinality Constraints. CP 2013: 80-96
- [c52]Ignasi Abío, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, Peter J. Stuckey: To Encode or to Propagate? The Best Choice for Each Constraint in SAT. CP 2013: 97-106
- 2012
- [j25]Ignasi Abío, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, Valentin Mayer-Eichberger: A New Look at BDDs for Pseudo-Boolean Constraints. J. Artif. Intell. Res. (JAIR) 45: 443-480 (2012)
- [c51]
- 2011
- [j24]Roberto Asín, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell: Cardinality Networks: a theoretical and empirical study. Constraints 16(2): 195-221 (2011)
- [j23]Javier Larrosa, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell: A Framework for Certified Boolean Branch-and-Bound Optimization. J. Autom. Reasoning 46(1): 81-102 (2011)
- [c50]Ignasi Abío, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell: BDDs for Pseudo-Boolean Constraints - Revisited. SAT 2011: 61-75
- [c49]Ignasi Abío, Morgan Deters, Robert Nieuwenhuis, Peter J. Stuckey: Reducing Chaos in SAT-Like Search: Finding Solutions Close to a Given One. SAT 2011: 273-286
- [i1]Nikolaj Bjørner, Robert Nieuwenhuis, Helmut Veith, Andrei Voronkov: Decision Procedures in Soft, Hard and Bio-ware - Follow Up (Dagstuhl Seminar 11272). Dagstuhl Reports 1(7): 23-35 (2011)
- 2010
- [j22]Roberto Javier Asín Achá, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell: Practical algorithms for unsatisfiability proof and core generation in SAT solvers. AI Commun. 23(2-3): 145-157 (2010)
- [j21]Marc Bezem, Robert Nieuwenhuis, Enric Rodríguez-Carbonell: Hard problems in max-algebra, control theory, hypergraphs and other areas. Inf. Process. Lett. 110(4): 133-138 (2010)
- [c48]Robert Nieuwenhuis: SAT Modulo Theories: Getting the Best of SAT and Global Constraint Filtering. CP 2010: 1-2
2000 – 2009
- 2009
- [c47]
- [c46]Roberto Asín, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell: Cardinality Networks and Their Applications. SAT 2009: 167-180
- [c45]Javier Larrosa, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell: Branch and Bound for Boolean Optimization and the Generation of Optimality Certificates. SAT 2009: 453-466
- 2008
- [j20]Marc Bezem, Robert Nieuwenhuis, Enric Rodríguez-Carbonell: Exponential behaviour of the Butkovic-Zimmermann algorithm for solving two-sided linear systems in max-algebra. Discrete Applied Mathematics 156(18): 3506-3509 (2008)
- [c44]Miquel Bofill, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio: The Barcelogic SMT Solver. CAV 2008: 294-298
- [c43]Miquel Bofill, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio: A Write-Based Solver for SAT Modulo the Theory of Arrays. FMCAD 2008: 1-8
- [c42]Roberto Asín, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell: Efficient Generation of Unsatisfiability Proofs and Cores in SAT. LPAR 2008: 16-30
- [c41]Marc Bezem, Robert Nieuwenhuis, Enric Rodríguez-Carbonell: The Max-Atom Problem and Its Relevance. LPAR 2008: 47-61
- [c40]Germain Faure, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell: SAT Modulo the Theory of Linear Arithmetic: Exact, Inexact and Commercial Solvers. SAT 2008: 77-90
- 2007
- [j19]Robert Nieuwenhuis, Albert Oliveras: Fast congruence closure and extensions. Inf. Comput. 205(4): 557-580 (2007)
- [c39]Franz Baader, Byron Cook, Jürgen Giesl, Robert Nieuwenhuis: 07401 Executive Summary -- Deduction and Decision Procedures. Deduction and Decision Procedures 2007
- [c38]Franz Baader, Byron Cook, Jürgen Giesl, Robert Nieuwenhuis: 07401 Abstracts Collection -- Deduction and Decision Procedures. Deduction and Decision Procedures 2007
- [c37]Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio: Challenges in Satisfiability Modulo Theories. RTA 2007: 2-18
- [e5]Franz Baader, Byron Cook, Jürgen Giesl, Robert Nieuwenhuis (Eds.): Deduction and Decision Procedures, 30.09. - 05.10.2007. Dagstuhl Seminar Proceedings 07401, Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany 2007
- 2006
- [j18]Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli: Solving SAT and SAT Modulo Theories: From an abstract Davis--Putnam--Logemann--Loveland procedure to DPLL(T). J. ACM 53(6): 937-977 (2006)
- [c36]Shuvendu K. Lahiri, Robert Nieuwenhuis, Albert Oliveras: SMT Techniques for Fast Predicate Abstraction. CAV 2006: 424-437
- [c35]Clark Barrett, Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli: Splitting on Demand in SAT Modulo Theories. LPAR 2006: 512-526
- [c34]Robert Nieuwenhuis, Albert Oliveras: On SAT Modulo Theories and Optimization Problems. SAT 2006: 156-169
- [e4]Franz Baader, Peter Baumgartner, Robert Nieuwenhuis, Andrei Voronkov (Eds.): Deduction and Applications, 23.-28. October 2005. Dagstuhl Seminar Proceedings 05431, Internationales Begegnungs- und Forschungszentrum für Informatik (IBFI), Schloss Dagstuhl, Germany 2006
- 2005
- [c33]Robert Nieuwenhuis, Albert Oliveras: DPLL(T) with Exhaustive Theory Propagation and Its Application to Difference Logic. CAV 2005: 321-334
- [c32]Franz Baader, Peter Baumgartner, Robert Nieuwenhuis, Andrei Voronkov: 05431 Executive Summary - Deduction and Applications. Deduction and Applications 2005
- [c31]Franz Baader, Peter Baumgartner, Robert Nieuwenhuis, Andrei Voronkov: 05431 Abstracts Collection - Deduction and Applications. Deduction and Applications 2005
- [c30]Robert Nieuwenhuis, Albert Oliveras: Decision Procedures for SAT, SAT Modulo Theories and Beyond. The BarcelogicTools. LPAR 2005: 23-46
- [c29]
- [e3]Robert Nieuwenhuis (Ed.): Automated Deduction - CADE-20, 20th International Conference on Automated Deduction, Tallinn, Estonia, July 22-27, 2005, Proceedings. Lecture Notes in Computer Science 3632, Springer 2005, ISBN 3-540-28005-7
- 2004
- [j17]Guillem Godoy, Robert Nieuwenhuis: Constraint Solving for Term Orderings Compatible with Abelian Semigroups, Monoids and Groups. Constraints 9(3): 167-192 (2004)
- [j16]Harald Ganzinger, Robert Nieuwenhuis, Pilar Nivela: Fast Term Indexing with Coded Context Trees. J. Autom. Reasoning 32(2): 103-120 (2004)
- [j15]Guillem Godoy, Robert Nieuwenhuis: Superposition with completely built-in Abelian groups. J. Symb. Comput. 37(1): 1-33 (2004)
- [j14]Guillem Godoy, Robert Nieuwenhuis, Ashish Tiwari: Classes of term rewrite systems with polynomial confluence problems. ACM Trans. Comput. Log. 5(2): 321-331 (2004)
- [c28]Harald Ganzinger, George Hagen, Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli: DPLL( T): Fast Decision Procedures. CAV 2004: 175-188
- [c27]Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli: Abstract DPLL and Abstract DPLL Modulo Theories. LPAR 2004: 36-50
- 2003
- [j13]Miquel Bofill, Guillem Godoy, Robert Nieuwenhuis, Albert Rubio: Paramodulation and Knuth-Bendix Completion with Nontotal and Nonmonotonic Orderings. J. Autom. Reasoning 30(1): 99-120 (2003)
- [j12]Anatoli Degtyarev, Robert Nieuwenhuis, Andrei Voronkov: Stratified resolution. J. Symb. Comput. 36(1-2): 79-99 (2003)
- [j11]Hubert Comon, Paliath Narendran, Robert Nieuwenhuis, Michaël Rusinowitch: Deciding the confluence of ordered term rewrite systems. ACM Trans. Comput. Log. 4(1): 33-55 (2003)
- [c26]
- [e2]Robert Nieuwenhuis (Ed.): Rewriting Techniques and Applications, 14th International Conference, RTA 2003, Valencia, Spain, June 9-11, 2003, Proceedings. Lecture Notes in Computer Science 2706, Springer 2003, ISBN 3-540-40254-3
- 2002
- [j10]Robert Nieuwenhuis: The impact of CASC in the development of automated deduction systems. AI Commun. 15(2-3): 77-78 (2002)
- [j9]Robert Nieuwenhuis, José Miguel Rivero: Practical Algorithms for Deciding Path Ordering Constraint Satisfaction. Inf. Comput. 178(2): 422-440 (2002)
- 2001
- [c25]
- [c24]Robert Nieuwenhuis, Thomas Hillenbrand, Alexandre Riazanov, Andrei Voronkov: On the Evaluation of Indexing Techniques for Theorem Proving. IJCAR 2001: 257-271
- [c23]Hubert Comon, Guillem Godoy, Robert Nieuwenhuis: The Confluence of Ground Term Rewrite Systems is Decidable in Polynomial Time. FOCS 2001: 298-307
- [c22]Guillem Godoy, Robert Nieuwenhuis: On Ordering Constraints for Deduction with Built-In Abelian Semigroups, Monoids and Groups. LICS 2001: 38-47
- [p1]Robert Nieuwenhuis, Albert Rubio: Paramodulation-Based Theorem Proving. Handbook of Automated Reasoning 2001: 371-443
- [e1]Robert Nieuwenhuis, Andrei Voronkov (Eds.): Logic for Programming, Artificial Intelligence, and Reasoning, 8th International Conference, LPAR 2001, Havana, Cuba, December 3-7, 2001, Proceedings. Lecture Notes in Computer Science 2250, Springer 2001, ISBN 3-540-42957-3
- 2000
- [j8]Hubert Comon, Robert Nieuwenhuis: Induction=I-Axiomatization+First-Order Consistency. Inf. Comput. 159(1-2): 151-186 (2000)
- [c21]Miquel Bofill, Guillem Godoy, Robert Nieuwenhuis, Albert Rubio: Modular Redundancy for Theorem Proving. FroCoS 2000: 186-199
- [c20]
1990 – 1999
- 1999
- [c19]Robert Nieuwenhuis: Invited Talk: Rewrite-based Deduction and Symbolic Constraints. CADE 1999: 302-313
- [c18]
- [c17]Miquel Bofill, Guillem Godoy, Robert Nieuwenhuis, Albert Rubio: Paramodulation with Non-Monotonic Orderings. LICS 1999: 225-233
- [c16]
- 1998
- [j7]Robert Nieuwenhuis: Decidability and Complexity Analysis by Basic Paramodulation. Inf. Comput. 147(1): 1-21 (1998)
- [c15]Hubert Comon, Paliath Narendran, Robert Nieuwenhuis, Michaël Rusinowitch: Decision Problems in Ordered Rewriting. LICS 1998: 276-286
- 1997
- [j6]Robert Nieuwenhuis, José Miguel Rivero, Miguel Ángel Vallejo: Barcelona. J. Autom. Reasoning 18(2): 171-176 (1997)
- [j5]Robert Nieuwenhuis, Albert Rubio: Paramodulation with Built-in AC-Theories and Symbolic Constraints. J. Symb. Comput. 23(1): 1-21 (1997)
- [c14]Robert Nieuwenhuis, José Miguel Rivero, Miguel Ángel Vallejo: Dedan: A Kernel of Data Structures and Algorithms for Automated Deduction with Equality Clauses. CADE 1997: 49-52
- 1996
- [c13]Robert Nieuwenhuis, José Miguel Rivero, Miguel Ángel Vallejo: An Implementation Kernel for Theorem Proving with Equality Clauses. APPIA-GULP-PRODE 1996: 89-104
- [c12]Robert Nieuwenhuis: Basic Paramodulation and Decidable Theories (Extended Abstract). LICS 1996: 473-482
- 1995
- [j4]Robert Nieuwenhuis, Albert Rubio: Theorem Proving with Ordering and Equality Constrained Clauses. J. Symb. Comput. 19(4): 321-351 (1995)
- [j3]Albert Rubio, Robert Nieuwenhuis: A Total AC-Compatible Ordering Based on RPO. Theor. Comput. Sci. 142(2): 209-227 (1995)
- [c11]Hubert Comon, Robert Nieuwenhuis, Albert Rubio: Orderings, AC-Theories and Symbolic Constraint Solving (Extended Abstract). LICS 1995: 375-385
- [c10]
- 1994
- [c9]Robert Nieuwenhuis, Albert Rubio: AC-Superposition with Constraints: No AC-Unifiers Needed. CADE 1994: 545-559
- 1993
- [j2]
- [c8]Hubert Bertling, Harald Ganzinger, Renate Schäfers, Robert Nieuwenhuis, Fernando Orejas: Program Development: Completion Subsystem. PROSPECTRA Book 1993: 460-494
- [c7]Albert Rubio, Robert Nieuwenhuis: A Precedence-Based Total AC-Compatible Ordering. RTA 1993: 374-388
- [c6]Pilar Nivela, Robert Nieuwenhuis: Saturation of First-Order (Constrained) Clauses with the Saturate System. RTA 1993: 436-440
- 1992
- [c5]Robert Nieuwenhuis, Albert Rubio: Theorem Proving with Ordering Constrained Clauses. CADE 1992: 477-491
- [c4]
- 1991
- [j1]Robert Nieuwenhuis, Pilar Nivela: Efficient Deduction in Equality Horn Logic by Horn-Completion. Inf. Process. Lett. 39(1): 1-6 (1991)
- 1990
- [c3]Robert Nieuwenhuis, Fernando Orejas: Clausal Rewriting: Applications and Implementation. ADT 1990: 204-219
- [c2]Robert Nieuwenhuis, Fernando Orejas, Albert Rubio: TRIP: An Implementation of Clausal Rewriting. CADE 1990: 667-668
- [c1]
Coauthor Index
data released under the ODC-BY 1.0 license. See also our legal information page
last updated on 2013-10-02 11:08 CEST by the dblp team