 | 2009 |
|---|
| 73 |       | Robert Nieuwenhuis:
SAT Modulo Theories: Enhancing SAT with Special-Purpose Algorithms.
SAT 2009: 1 |
| 72 | | Roberto Asín,
Robert Nieuwenhuis,
Albert Oliveras,
Enric Rodríguez-Carbonell:
Cardinality Networks and Their Applications.
SAT 2009: 167-180 |
| 71 | | 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 |
|---|
| 70 | | Miquel Bofill,
Robert Nieuwenhuis,
Albert Oliveras,
Enric Rodríguez-Carbonell,
Albert Rubio:
The Barcelogic SMT Solver.
CAV 2008: 294-298 |
| 69 | | 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 |
| 68 | | Roberto Asín,
Robert Nieuwenhuis,
Albert Oliveras,
Enric Rodríguez-Carbonell:
Efficient Generation of Unsatisfiability Proofs and Cores in SAT.
LPAR 2008: 16-30 |
| 67 | | Marc Bezem,
Robert Nieuwenhuis,
Enric Rodríguez-Carbonell:
The Max-Atom Problem and Its Relevance.
LPAR 2008: 47-61 |
| 66 | | 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 |
| 65 | | 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) |
| 2007 |
|---|
| 64 |  | Franz Baader,
Byron Cook,
Jürgen Giesl,
Robert Nieuwenhuis:
Deduction and Decision Procedures, 30.09. - 05.10.2007
Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany 2007 |
| 63 | | Franz Baader,
Byron Cook,
Jürgen Giesl,
Robert Nieuwenhuis:
07401 Abstracts Collection -- Deduction and Decision Procedures.
Deduction and Decision Procedures 2007 |
| 62 | | Franz Baader,
Byron Cook,
Jürgen Giesl,
Robert Nieuwenhuis:
07401 Executive Summary -- Deduction and Decision Procedures.
Deduction and Decision Procedures 2007 |
| 61 | | Robert Nieuwenhuis,
Albert Oliveras,
Enric Rodríguez-Carbonell,
Albert Rubio:
Challenges in Satisfiability Modulo Theories.
RTA 2007: 2-18 |
| 60 | | Robert Nieuwenhuis,
Albert Oliveras:
Fast congruence closure and extensions.
Inf. Comput. 205(4): 557-580 (2007) |
| 2006 |
|---|
| 59 | | Franz Baader,
Peter Baumgartner,
Robert Nieuwenhuis,
Andrei Voronkov:
Deduction and Applications, 23.-28. October 2005
Internationales Begegnungs- und Forschungszentrum für Informatik (IBFI), Schloss Dagstuhl, Germany 2006 |
| 58 | | Shuvendu K. Lahiri,
Robert Nieuwenhuis,
Albert Oliveras:
SMT Techniques for Fast Predicate Abstraction.
CAV 2006: 424-437 |
| 57 | | Clark Barrett,
Robert Nieuwenhuis,
Albert Oliveras,
Cesare Tinelli:
Splitting on Demand in SAT Modulo Theories.
LPAR 2006: 512-526 |
| 56 | | Robert Nieuwenhuis,
Albert Oliveras:
On SAT Modulo Theories and Optimization Problems.
SAT 2006: 156-169 |
| 55 | | 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) |
| 2005 |
|---|
| 54 | | Robert Nieuwenhuis:
Automated Deduction - CADE-20, 20th International Conference on Automated Deduction, Tallinn, Estonia, July 22-27, 2005, Proceedings
Springer 2005 |
| 53 | | Robert Nieuwenhuis,
Albert Oliveras:
DPLL(T) with Exhaustive Theory Propagation and Its Application to Difference Logic.
CAV 2005: 321-334 |
| 52 | | Franz Baader,
Peter Baumgartner,
Robert Nieuwenhuis,
Andrei Voronkov:
05431 Abstracts Collection - Deduction and Applications.
Deduction and Applications 2005 |
| 51 | | Franz Baader,
Peter Baumgartner,
Robert Nieuwenhuis,
Andrei Voronkov:
05431 Executive Summary - Deduction and Applications.
Deduction and Applications 2005 |
| 50 | | Robert Nieuwenhuis,
Albert Oliveras:
Decision Procedures for SAT, SAT Modulo Theories and Beyond. The BarcelogicTools.
LPAR 2005: 23-46 |
| 49 | | Robert Nieuwenhuis,
Albert Oliveras:
Proof-Producing Congruence Closure.
RTA 2005: 453-468 |
| 2004 |
|---|
| 48 | | Harald Ganzinger,
George Hagen,
Robert Nieuwenhuis,
Albert Oliveras,
Cesare Tinelli:
DPLL( T): Fast Decision Procedures.
CAV 2004: 175-188 |
| 47 | | Robert Nieuwenhuis,
Albert Oliveras,
Cesare Tinelli:
Abstract DPLL and Abstract DPLL Modulo Theories.
LPAR 2004: 36-50 |
| 46 | | Guillem Godoy,
Robert Nieuwenhuis,
Ashish Tiwari:
Classes of term rewrite systems with polynomial confluence problems.
ACM Trans. Comput. Log. 5(2): 321-331 (2004) |
| 45 | | Guillem Godoy,
Robert Nieuwenhuis:
Constraint Solving for Term Orderings Compatible with Abelian Semigroups, Monoids and Groups.
Constraints 9(3): 167-192 (2004) |
| 44 | | Harald Ganzinger,
Robert Nieuwenhuis,
Pilar Nivela:
Fast Term Indexing with Coded Context Trees.
J. Autom. Reasoning 32(2): 103-120 (2004) |
| 43 | | Guillem Godoy,
Robert Nieuwenhuis:
Superposition with completely built-in Abelian groups.
J. Symb. Comput. 37(1): 1-33 (2004) |
| 2003 |
|---|
| 42 | | Robert Nieuwenhuis:
Rewriting Techniques and Applications, 14th International Conference, RTA 2003, Valencia, Spain, June 9-11, 2003, Proceedings
Springer 2003 |
| 41 | | Robert Nieuwenhuis,
Albert Oliveras:
Congruence Closure with Integer Offsets.
LPAR 2003: 78-90 |
| 40 | | 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) |
| 39 | | 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) |
| 38 | | Anatoli Degtyarev,
Robert Nieuwenhuis,
Andrei Voronkov:
Stratified resolution.
J. Symb. Comput. 36(1-2): 79-99 (2003) |
| 2002 |
|---|
| 37 | | Robert Nieuwenhuis:
The impact of CASC in the development of automated deduction systems.
AI Commun. 15(2-3): 77-78 (2002) |
| 36 | | Robert Nieuwenhuis,
José Miguel Rivero:
Practical Algorithms for Deciding Path Ordering Constraint Satisfaction.
Inf. Comput. 178(2): 422-440 (2002) |
| 2001 |
|---|
| 35 | | Robert Nieuwenhuis,
Andrei Voronkov:
Logic for Programming, Artificial Intelligence, and Reasoning, 8th International Conference, LPAR 2001, Havana, Cuba, December 3-7, 2001, Proceedings
Springer 2001 |
| 34 | | Hubert Comon,
Guillem Godoy,
Robert Nieuwenhuis:
The Confluence of Ground Term Rewrite Systems is Decidable in Polynomial Time.
FOCS 2001: 298-307 |
| 33 | | Harald Ganzinger,
Robert Nieuwenhuis,
Pilar Nivela:
Context Trees.
IJCAR 2001: 242-256 |
| 32 | | Robert Nieuwenhuis,
Thomas Hillenbrand,
Alexandre Riazanov,
Andrei Voronkov:
On the Evaluation of Indexing Techniques for Theorem Proving.
IJCAR 2001: 257-271 |
| 31 | | Guillem Godoy,
Robert Nieuwenhuis:
On Ordering Constraints for Deduction with Built-In Abelian Semigroups, Monoids and Groups.
LICS 2001: 38-50 |
| 30 | | Robert Nieuwenhuis,
Albert Rubio:
Paramodulation-Based Theorem Proving.
Handbook of Automated Reasoning 2001: 371-443 |
| 2000 |
|---|
| 29 | | Miquel Bofill,
Guillem Godoy,
Robert Nieuwenhuis,
Albert Rubio:
Modular Redundancy for Theorem Proving.
FroCos 2000: 186-199 |
| 28 | | Guillem Godoy,
Robert Nieuwenhuis:
Paramodulation with Built-in Abelian Groups.
LICS 2000: 413-424 |
| 27 | | Hubert Comon,
Robert Nieuwenhuis:
Induction=I-Axiomatization+First-Order Consistency.
Inf. Comput. 159(1-2): 151-186 (2000) |
| 1999 |
|---|
| 26 | | Robert Nieuwenhuis:
Invited Talk: Rewrite-based Deduction and Symbolic Constraints.
CADE 1999: 302-313 |
| 25 | | Harald Ganzinger,
Robert Nieuwenhuis:
Constraints and Theorem Proving.
CCL 1999: 159-201 |
| 24 | | Miquel Bofill,
Guillem Godoy,
Robert Nieuwenhuis,
Albert Rubio:
Paramodulation with Non-Monotonic Orderings.
LICS 1999: 225-233 |
| 23 | | Robert Nieuwenhuis,
José Miguel Rivero:
Solved Forms for Path Ordering Constraints.
RTA 1999: 1-15 |
| 1998 |
|---|
| 22 | | Hubert Comon,
Paliath Narendran,
Robert Nieuwenhuis,
Michaël Rusinowitch:
Decision Problems in Ordered Rewriting.
LICS 1998: 276-286 |
| 21 | | Robert Nieuwenhuis:
Decidability and Complexity Analysis by Basic Paramodulation.
Inf. Comput. 147(1): 1-21 (1998) |
| 1997 |
|---|
| 20 | | 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 |
| 19 | | Robert Nieuwenhuis,
José Miguel Rivero,
Miguel Ángel Vallejo:
Barcelona.
J. Autom. Reasoning 18(2): 171-176 (1997) |
| 18 | | Robert Nieuwenhuis,
Albert Rubio:
Paramodulation with Built-in AC-Theories and Symbolic Constraints.
J. Symb. Comput. 23(1): 1-21 (1997) |
| 1996 |
|---|
| 17 | | Robert Nieuwenhuis,
José Miguel Rivero,
Miguel Ángel Vallejo:
An Implementation Kernel for Theorem Proving with Equality Clauses.
APPIA-GULP-PRODE 1996: 89-104 |
| 16 | | Robert Nieuwenhuis:
Basic Paramodulation and Decidable Theories (Extended Abstract).
LICS 1996: 473-482 |
| 1995 |
|---|
| 15 | | Hubert Comon,
Robert Nieuwenhuis,
Albert Rubio:
Orderings, AC-Theories and Symbolic Constraint Solving (Extended Abstract)
LICS 1995: 375-385 |
| 14 | | Robert Nieuwenhuis:
On Narrowing, Refutation Proofs and Constraints.
RTA 1995: 56-70 |
| 13 | | Robert Nieuwenhuis,
Albert Rubio:
Theorem Proving with Ordering and Equality Constrained Clauses.
J. Symb. Comput. 19(4): 321-351 (1995) |
| 12 | | Albert Rubio,
Robert Nieuwenhuis:
A Total AC-Compatible Ordering Based on RPO.
Theor. Comput. Sci. 142(2): 209-227 (1995) |
| 1994 |
|---|
| 11 | | Robert Nieuwenhuis,
Albert Rubio:
AC-Superposition with Constraints: No AC-Unifiers Needed.
CADE 1994: 545-559 |
| 1993 |
|---|
| 10 | | Hubert Bertling,
Harald Ganzinger,
Renate Schäfers,
Robert Nieuwenhuis,
Fernando Orejas:
Program Development: Completion Subsystem.
PROSPECTRA Book 1993: 460-494 |
| 9 | | Albert Rubio,
Robert Nieuwenhuis:
A Precedence-Based Total AC-Compatible Ordering.
RTA 1993: 374-388 |
| 8 | | Pilar Nivela,
Robert Nieuwenhuis:
Saturation of First-Order (Constrained) Clauses with the Saturate System.
RTA 1993: 436-440 |
| 7 | | Robert Nieuwenhuis:
Simple LPO Constraint Solving Methods.
Inf. Process. Lett. 47(2): 65-69 (1993) |
| 1992 |
|---|
| 6 | | Robert Nieuwenhuis,
Albert Rubio:
Theorem Proving with Ordering Constrained Clauses.
CADE 1992: 477-491 |
| 5 | | Robert Nieuwenhuis,
Albert Rubio:
Basic Superposition is Complete.
ESOP 1992: 371-389 |
| 1991 |
|---|
| 4 | | Robert Nieuwenhuis,
Pilar Nivela:
Efficient Deduction in Equality Horn Logic by Horn-Completion.
Inf. Process. Lett. 39(1): 1-6 (1991) |
| 1990 |
|---|
| 3 | | Robert Nieuwenhuis,
Fernando Orejas:
Clausal Rewriting: Applications and Implementation.
ADT 1990: 204-219 |
| 2 | | Robert Nieuwenhuis,
Fernando Orejas,
Albert Rubio:
TRIP: An Implementation of Clausal Rewriting.
CADE 1990: 667-668 |
| 1 | | Robert Nieuwenhuis,
Fernando Orejas:
Clausal Rewriting.
CTRS 1990: 246-258 |
