The SCEAS System
Navigation Menu
Introduction
Collection Based
Clustering
Ranking
Paper Based
Journals
Conferences
DB Status
Statistics
Search

Search the dblp DataBase

Title:
Author:
Robert Nieuwenhuis: [Publications] [Author Rank by year] [Co-authors] [Prefers] [Cites] [Cited by]

Publications of Author

  1. Robert Nieuwenhuis, Albert Rubio
    Theorem Proving with Ordering and Equality Constrained Clauses. [Citation Graph (1, 0)][DBLP]
    J. Symb. Comput., 1995, v:19, n:4, pp:321-351 [Journal]
  2. Robert Nieuwenhuis, Fernando Orejas
    Clausal Rewriting: Applications and Implementation. [Citation Graph (0, 0)][DBLP]
    ADT, 1990, pp:204-219 [Conf]
  3. Robert Nieuwenhuis, José Miguel Rivero, Miguel Ángel Vallejo
    An Implementation Kernel for Theorem Proving with Equality Clauses. [Citation Graph (0, 0)][DBLP]
    APPIA-GULP-PRODE, 1996, pp:89-104 [Conf]
  4. Harald Ganzinger, Robert Nieuwenhuis, Pilar Nivela
    Context Trees. [Citation Graph (0, 0)][DBLP]
    IJCAR, 2001, pp:242-256 [Conf]
  5. Robert Nieuwenhuis
    Invited Talk: Rewrite-based Deduction and Symbolic Constraints. [Citation Graph (0, 0)][DBLP]
    CADE, 1999, pp:302-313 [Conf]
  6. Robert Nieuwenhuis, Thomas Hillenbrand, Alexandre Riazanov, Andrei Voronkov
    On the Evaluation of Indexing Techniques for Theorem Proving. [Citation Graph (0, 0)][DBLP]
    IJCAR, 2001, pp:257-271 [Conf]
  7. Robert Nieuwenhuis, Fernando Orejas, Albert Rubio
    TRIP: An Implementation of Clausal Rewriting. [Citation Graph (0, 0)][DBLP]
    CADE, 1990, pp:667-668 [Conf]
  8. Robert Nieuwenhuis, Albert Rubio
    Theorem Proving with Ordering Constrained Clauses. [Citation Graph (0, 0)][DBLP]
    CADE, 1992, pp:477-491 [Conf]
  9. Robert Nieuwenhuis, Albert Rubio
    AC-Superposition with Constraints: No AC-Unifiers Needed. [Citation Graph (0, 0)][DBLP]
    CADE, 1994, pp:545-559 [Conf]
  10. Robert Nieuwenhuis, José Miguel Rivero, Miguel Ángel Vallejo
    Dedan: A Kernel of Data Structures and Algorithms for Automated Deduction with Equality Clauses. [Citation Graph (0, 0)][DBLP]
    CADE, 1997, pp:49-52 [Conf]
  11. Harald Ganzinger, George Hagen, Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli
    DPLL( T): Fast Decision Procedures. [Citation Graph (0, 0)][DBLP]
    CAV, 2004, pp:175-188 [Conf]
  12. Shuvendu K. Lahiri, Robert Nieuwenhuis, Albert Oliveras
    SMT Techniques for Fast Predicate Abstraction. [Citation Graph (0, 0)][DBLP]
    CAV, 2006, pp:424-437 [Conf]
  13. Robert Nieuwenhuis, Albert Oliveras
    DPLL(T) with Exhaustive Theory Propagation and Its Application to Difference Logic. [Citation Graph (0, 0)][DBLP]
    CAV, 2005, pp:321-334 [Conf]
  14. Harald Ganzinger, Robert Nieuwenhuis
    Constraints and Theorem Proving. [Citation Graph (0, 0)][DBLP]
    CCL, 1999, pp:159-201 [Conf]
  15. Robert Nieuwenhuis, Fernando Orejas
    Clausal Rewriting. [Citation Graph (0, 0)][DBLP]
    CTRS, 1990, pp:246-258 [Conf]
  16. Franz Baader, Peter Baumgartner, Robert Nieuwenhuis, Andrei Voronkov
    05431 Executive Summary - Deduction and Applications. [Citation Graph (0, 0)][DBLP]
    Deduction and Applications, 2005, pp:- [Conf]
  17. Franz Baader, Peter Baumgartner, Robert Nieuwenhuis, Andrei Voronkov
    05431 Abstracts Collection - Deduction and Applications. [Citation Graph (0, 0)][DBLP]
    Deduction and Applications, 2005, pp:- [Conf]
  18. Robert Nieuwenhuis, Albert Rubio
    Basic Superposition is Complete. [Citation Graph (0, 0)][DBLP]
    ESOP, 1992, pp:371-389 [Conf]
  19. Hubert Comon, Guillem Godoy, Robert Nieuwenhuis
    The Confluence of Ground Term Rewrite Systems is Decidable in Polynomial Time. [Citation Graph (0, 0)][DBLP]
    FOCS, 2001, pp:298-307 [Conf]
  20. Miquel Bofill, Guillem Godoy, Robert Nieuwenhuis, Albert Rubio
    Modular Redundancy for Theorem Proving. [Citation Graph (0, 0)][DBLP]
    FroCos, 2000, pp:186-199 [Conf]
  21. Miquel Bofill, Guillem Godoy, Robert Nieuwenhuis, Albert Rubio
    Paramodulation with Non-Monotonic Orderings. [Citation Graph (0, 0)][DBLP]
    LICS, 1999, pp:225-233 [Conf]
  22. Hubert Comon, Paliath Narendran, Robert Nieuwenhuis, Michaël Rusinowitch
    Decision Problems in Ordered Rewriting. [Citation Graph (0, 0)][DBLP]
    LICS, 1998, pp:276-286 [Conf]
  23. Hubert Comon, Robert Nieuwenhuis, Albert Rubio
    Orderings, AC-Theories and Symbolic Constraint Solving (Extended Abstract) [Citation Graph (0, 0)][DBLP]
    LICS, 1995, pp:375-385 [Conf]
  24. Guillem Godoy, Robert Nieuwenhuis
    Paramodulation with Built-in Abelian Groups. [Citation Graph (0, 0)][DBLP]
    LICS, 2000, pp:413-424 [Conf]
  25. Guillem Godoy, Robert Nieuwenhuis
    On Ordering Constraints for Deduction with Built-In Abelian Semigroups, Monoids and Groups. [Citation Graph (0, 0)][DBLP]
    LICS, 2001, pp:38-50 [Conf]
  26. Robert Nieuwenhuis
    Basic Paramodulation and Decidable Theories (Extended Abstract). [Citation Graph (0, 0)][DBLP]
    LICS, 1996, pp:473-482 [Conf]
  27. Clark Barrett, Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli
    Splitting on Demand in SAT Modulo Theories. [Citation Graph (0, 0)][DBLP]
    LPAR, 2006, pp:512-526 [Conf]
  28. Robert Nieuwenhuis, Albert Oliveras
    Congruence Closure with Integer Offsets. [Citation Graph (0, 0)][DBLP]
    LPAR, 2003, pp:78-90 [Conf]
  29. Robert Nieuwenhuis, Albert Oliveras
    Decision Procedures for SAT, SAT Modulo Theories and Beyond. The BarcelogicTools. [Citation Graph (0, 0)][DBLP]
    LPAR, 2005, pp:23-46 [Conf]
  30. Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli
    Abstract DPLL and Abstract DPLL Modulo Theories. [Citation Graph (0, 0)][DBLP]
    LPAR, 2004, pp:36-50 [Conf]
  31. Hubert Bertling, Harald Ganzinger, Renate Schäfers, Robert Nieuwenhuis, Fernando Orejas
    Program Development: Completion Subsystem. [Citation Graph (0, 0)][DBLP]
    PROSPECTRA Book, 1993, pp:460-494 [Conf]
  32. Robert Nieuwenhuis
    On Narrowing, Refutation Proofs and Constraints. [Citation Graph (0, 0)][DBLP]
    RTA, 1995, pp:56-70 [Conf]
  33. Robert Nieuwenhuis, Albert Oliveras
    Proof-Producing Congruence Closure. [Citation Graph (0, 0)][DBLP]
    RTA, 2005, pp:453-468 [Conf]
  34. Robert Nieuwenhuis, José Miguel Rivero
    Solved Forms for Path Ordering Constraints. [Citation Graph (0, 0)][DBLP]
    RTA, 1999, pp:1-15 [Conf]
  35. Pilar Nivela, Robert Nieuwenhuis
    Saturation of First-Order (Constrained) Clauses with the Saturate System. [Citation Graph (0, 0)][DBLP]
    RTA, 1993, pp:436-440 [Conf]
  36. Albert Rubio, Robert Nieuwenhuis
    A Precedence-Based Total AC-Compatible Ordering. [Citation Graph (0, 0)][DBLP]
    RTA, 1993, pp:374-388 [Conf]
  37. Robert Nieuwenhuis, Albert Oliveras
    On SAT Modulo Theories and Optimization Problems. [Citation Graph (0, 0)][DBLP]
    SAT, 2006, pp:156-169 [Conf]
  38. Robert Nieuwenhuis
    The impact of CASC in the development of automated deduction systems. [Citation Graph (0, 0)][DBLP]
    AI Commun., 2002, v:15, n:2-3, pp:77-78 [Journal]
  39. Guillem Godoy, Robert Nieuwenhuis
    Constraint Solving for Term Orderings Compatible with Abelian Semigroups, Monoids and Groups. [Citation Graph (0, 0)][DBLP]
    Constraints, 2004, v:9, n:3, pp:167-192 [Journal]
  40. Hubert Comon, Robert Nieuwenhuis
    Induction=I-Axiomatization+First-Order Consistency. [Citation Graph (0, 0)][DBLP]
    Inf. Comput., 2000, v:159, n:1-2, pp:151-186 [Journal]
  41. Robert Nieuwenhuis
    Decidability and Complexity Analysis by Basic Paramodulation. [Citation Graph (0, 0)][DBLP]
    Inf. Comput., 1998, v:147, n:1, pp:1-21 [Journal]
  42. Robert Nieuwenhuis, José Miguel Rivero
    Practical Algorithms for Deciding Path Ordering Constraint Satisfaction. [Citation Graph (0, 0)][DBLP]
    Inf. Comput., 2002, v:178, n:2, pp:422-440 [Journal]
  43. Robert Nieuwenhuis
    Simple LPO Constraint Solving Methods. [Citation Graph (0, 0)][DBLP]
    Inf. Process. Lett., 1993, v:47, n:2, pp:65-69 [Journal]
  44. Robert Nieuwenhuis, Pilar Nivela
    Efficient Deduction in Equality Horn Logic by Horn-Completion. [Citation Graph (0, 0)][DBLP]
    Inf. Process. Lett., 1991, v:39, n:1, pp:1-6 [Journal]
  45. Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli
    Solving SAT and SAT Modulo Theories: From an abstract Davis--Putnam--Logemann--Loveland procedure to DPLL(T). [Citation Graph (0, 0)][DBLP]
    J. ACM, 2006, v:53, n:6, pp:937-977 [Journal]
  46. Miquel Bofill, Guillem Godoy, Robert Nieuwenhuis, Albert Rubio
    Paramodulation and Knuth-Bendix Completion with Nontotal and Nonmonotonic Orderings. [Citation Graph (0, 0)][DBLP]
    J. Autom. Reasoning, 2003, v:30, n:1, pp:99-120 [Journal]
  47. Harald Ganzinger, Robert Nieuwenhuis, Pilar Nivela
    Fast Term Indexing with Coded Context Trees. [Citation Graph (0, 0)][DBLP]
    J. Autom. Reasoning, 2004, v:32, n:2, pp:103-120 [Journal]
  48. Robert Nieuwenhuis, José Miguel Rivero, Miguel Ángel Vallejo
    Barcelona. [Citation Graph (0, 0)][DBLP]
    J. Autom. Reasoning, 1997, v:18, n:2, pp:171-176 [Journal]
  49. Anatoli Degtyarev, Robert Nieuwenhuis, Andrei Voronkov
    Stratified resolution. [Citation Graph (0, 0)][DBLP]
    J. Symb. Comput., 2003, v:36, n:1-2, pp:79-99 [Journal]
  50. Guillem Godoy, Robert Nieuwenhuis
    Superposition with completely built-in Abelian groups. [Citation Graph (0, 0)][DBLP]
    J. Symb. Comput., 2004, v:37, n:1, pp:1-33 [Journal]
  51. Robert Nieuwenhuis, Albert Rubio
    Paramodulation with Built-in AC-Theories and Symbolic Constraints. [Citation Graph (0, 0)][DBLP]
    J. Symb. Comput., 1997, v:23, n:1, pp:1-21 [Journal]
  52. Albert Rubio, Robert Nieuwenhuis
    A Total AC-Compatible Ordering Based on RPO. [Citation Graph (0, 0)][DBLP]
    Theor. Comput. Sci., 1995, v:142, n:2, pp:209-227 [Journal]
  53. Guillem Godoy, Robert Nieuwenhuis, Ashish Tiwari
    Classes of term rewrite systems with polynomial confluence problems. [Citation Graph (0, 0)][DBLP]
    ACM Trans. Comput. Log., 2004, v:5, n:2, pp:321-331 [Journal]
  54. Hubert Comon, Paliath Narendran, Robert Nieuwenhuis, Michaël Rusinowitch
    Deciding the confluence of ordered term rewrite systems. [Citation Graph (0, 0)][DBLP]
    ACM Trans. Comput. Log., 2003, v:4, n:1, pp:33-55 [Journal]
  55. Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio
    Challenges in Satisfiability Modulo Theories. [Citation Graph (0, 0)][DBLP]
    RTA, 2007, pp:2-18 [Conf]
  56. Robert Nieuwenhuis, Albert Oliveras
    Fast congruence closure and extensions. [Citation Graph (0, 0)][DBLP]
    Inf. Comput., 2007, v:205, n:4, pp:557-580 [Journal]

  57. The Barcelogic SMT Solver. [Citation Graph (, )][DBLP]


  58. 07401 Abstracts Collection -- Deduction and Decision Procedures. [Citation Graph (, )][DBLP]


  59. 07401 Executive Summary -- Deduction and Decision Procedures. [Citation Graph (, )][DBLP]


  60. A Write-Based Solver for SAT Modulo the Theory of Arrays. [Citation Graph (, )][DBLP]


  61. The Max-Atom Problem and Its Relevance. [Citation Graph (, )][DBLP]


  62. Efficient Generation of Unsatisfiability Proofs and Cores in SAT. [Citation Graph (, )][DBLP]


  63. Branch and Bound for Boolean Optimization and the Generation of Optimality Certificates. [Citation Graph (, )][DBLP]


  64. SAT Modulo the Theory of Linear Arithmetic: Exact, Inexact and Commercial Solvers. [Citation Graph (, )][DBLP]


  65. Cardinality Networks and Their Applications. [Citation Graph (, )][DBLP]


  66. SAT Modulo Theories: Enhancing SAT with Special-Purpose Algorithms. [Citation Graph (, )][DBLP]


  67. Practical algorithms for unsatisfiability proof and core generation in SAT solvers. [Citation Graph (, )][DBLP]


  68. Exponential behaviour of the Butkovic-Zimmermann algorithm for solving two-sided linear systems in max-algebra. [Citation Graph (, )][DBLP]


Search in 0.004secs, Finished in 0.451secs
NOTICE1
System may not be available sometimes or not working properly, since it is still in development with continuous upgrades
NOTICE2
The rankings that are presented on this page should NOT be considered as formal since the citation info is incomplete in DBLP
 
Introduction Collection Based Clustering Ranking Paper Based Journals Conferences DB Status Statistics Search
System created by asidirop@csd.auth.gr [http://users.auth.gr/~asidirop/] © 2002
for Data Engineering Laboratory, Department of Informatics, Aristotle University © 2002