dblp.uni-trier.dewww.uni-trier.de

Robert Nieuwenhuis Vis

List of publications from the DBLP Bibliography Server - FAQ
Coauthor Index - Ask others: ACM DL/Guide - CiteSeerX - CSB - MetaPress - Google - Bing - Yahoo
Home Page

*2009
73EERobert Nieuwenhuis: SAT Modulo Theories: Enhancing SAT with Special-Purpose Algorithms. SAT 2009: 1
72EERoberto Asín, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell: Cardinality Networks and Their Applications. SAT 2009: 167-180
71EEJavier 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
70EEMiquel Bofill, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio: The Barcelogic SMT Solver. CAV 2008: 294-298
69EEMiquel 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
68EERoberto Asín, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell: Efficient Generation of Unsatisfiability Proofs and Cores in SAT. LPAR 2008: 16-30
67EEMarc Bezem, Robert Nieuwenhuis, Enric Rodríguez-Carbonell: The Max-Atom Problem and Its Relevance. LPAR 2008: 47-61
66EEGermain 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
65EEMarc 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
63EEFranz Baader, Byron Cook, Jürgen Giesl, Robert Nieuwenhuis: 07401 Abstracts Collection -- Deduction and Decision Procedures. Deduction and Decision Procedures 2007
62EEFranz Baader, Byron Cook, Jürgen Giesl, Robert Nieuwenhuis: 07401 Executive Summary -- Deduction and Decision Procedures. Deduction and Decision Procedures 2007
61EERobert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio: Challenges in Satisfiability Modulo Theories. RTA 2007: 2-18
60EERobert 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
58EEShuvendu K. Lahiri, Robert Nieuwenhuis, Albert Oliveras: SMT Techniques for Fast Predicate Abstraction. CAV 2006: 424-437
57EEClark Barrett, Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli: Splitting on Demand in SAT Modulo Theories. LPAR 2006: 512-526
56EERobert Nieuwenhuis, Albert Oliveras: On SAT Modulo Theories and Optimization Problems. SAT 2006: 156-169
55EERobert 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
53EERobert Nieuwenhuis, Albert Oliveras: DPLL(T) with Exhaustive Theory Propagation and Its Application to Difference Logic. CAV 2005: 321-334
52EEFranz Baader, Peter Baumgartner, Robert Nieuwenhuis, Andrei Voronkov: 05431 Abstracts Collection - Deduction and Applications. Deduction and Applications 2005
51EEFranz Baader, Peter Baumgartner, Robert Nieuwenhuis, Andrei Voronkov: 05431 Executive Summary - Deduction and Applications. Deduction and Applications 2005
50EERobert Nieuwenhuis, Albert Oliveras: Decision Procedures for SAT, SAT Modulo Theories and Beyond. The BarcelogicTools. LPAR 2005: 23-46
49EERobert Nieuwenhuis, Albert Oliveras: Proof-Producing Congruence Closure. RTA 2005: 453-468
2004
48EEHarald Ganzinger, George Hagen, Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli: DPLL( T): Fast Decision Procedures. CAV 2004: 175-188
47EERobert Nieuwenhuis, Albert Oliveras, Cesare Tinelli: Abstract DPLL and Abstract DPLL Modulo Theories. LPAR 2004: 36-50
46EEGuillem Godoy, Robert Nieuwenhuis, Ashish Tiwari: Classes of term rewrite systems with polynomial confluence problems. ACM Trans. Comput. Log. 5(2): 321-331 (2004)
45EEGuillem Godoy, Robert Nieuwenhuis: Constraint Solving for Term Orderings Compatible with Abelian Semigroups, Monoids and Groups. Constraints 9(3): 167-192 (2004)
44EEHarald Ganzinger, Robert Nieuwenhuis, Pilar Nivela: Fast Term Indexing with Coded Context Trees. J. Autom. Reasoning 32(2): 103-120 (2004)
43EEGuillem 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
41EERobert Nieuwenhuis, Albert Oliveras: Congruence Closure with Integer Offsets. LPAR 2003: 78-90
40EEHubert 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)
38EEAnatoli Degtyarev, Robert Nieuwenhuis, Andrei Voronkov: Stratified resolution. J. Symb. Comput. 36(1-2): 79-99 (2003)
2002
37EERobert Nieuwenhuis: The impact of CASC in the development of automated deduction systems. AI Commun. 15(2-3): 77-78 (2002)
36EERobert 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
33EEHarald Ganzinger, Robert Nieuwenhuis, Pilar Nivela: Context Trees. IJCAR 2001: 242-256
32EERobert 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
28EEGuillem 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
26EERobert Nieuwenhuis: Invited Talk: Rewrite-based Deduction and Symbolic Constraints. CADE 1999: 302-313
25EEHarald Ganzinger, Robert Nieuwenhuis: Constraints and Theorem Proving. CCL 1999: 159-201
24EEMiquel Bofill, Guillem Godoy, Robert Nieuwenhuis, Albert Rubio: Paramodulation with Non-Monotonic Orderings. LICS 1999: 225-233
23EERobert 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
20EERobert 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
14EERobert 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)
12EEAlbert Rubio, Robert Nieuwenhuis: A Total AC-Compatible Ordering Based on RPO. Theor. Comput. Sci. 142(2): 209-227 (1995)
1994
11EERobert 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
9EEAlbert Rubio, Robert Nieuwenhuis: A Precedence-Based Total AC-Compatible Ordering. RTA 1993: 374-388
8EEPilar 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
6EERobert Nieuwenhuis, Albert Rubio: Theorem Proving with Ordering Constrained Clauses. CADE 1992: 477-491
5EERobert 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
2EERobert 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

Coauthor Index

1Roberto Asín [68] [72]
2Franz Baader [51] [52] [59] [62] [63] [64]
3Clark W. Barrett (Clark Barrett) [57]
4Peter Baumgartner [51] [52] [59]
5Hubert Bertling [10]
6Marc Bezem [65] [67]
7Miquel Bofill [24] [29] [39] [69] [70]
8Hubert Comon-Lundh (Hubert Comon) [15] [22] [27] [34] [40]
9Byron Cook [62] [63] [64]
10Anatoli Degtyarev [38]
11Germain Faure [66]
12Harald Ganzinger [10] [25] [33] [44] [48]
13Jürgen Giesl [62] [63] [64]
14Guillem Godoy [24] [28] [29] [31] [34] [39] [43] [45] [46]
15George Hagen [48]
16Thomas Hillenbrand [32]
17Shuvendu K. Lahiri [58]
18Javier Larrosa [71]
19Paliath Narendran [22] [40]
20Pilar Nivela [4] [8] [33] [44]
21Albert Oliveras [41] [47] [48] [49] [50] [53] [55] [56] [57] [58] [60] [61] [66] [68] [69] [70] [71] [72]
22Fernando Orejas [1] [2] [3] [10]
23Alexandre Riazanov [32]
24José Miguel Rivero [17] [19] [20] [23] [36]
25Enric Rodríguez-Carbonell [61] [65] [66] [67] [68] [69] [70] [71] [72]
26Albert Rubio [2] [5] [6] [9] [11] [12] [13] [15] [18] [24] [29] [30] [39] [61] [69] [70]
27Michaël Rusinowitch [22] [40]
28Renate Schäfers [10]
29Cesare Tinelli [47] [48] [55] [57]
30Ashish Tiwari [46]
31Miguel Ángel Vallejo [17] [19] [20]
32Andrei Voronkov [32] [35] [38] [51] [52] [59]

Colors in the list of coauthors

Copyright © Tue Nov 3 08:52:44 2009 by Michael Ley (ley@uni-trier.de)