BibSLEIGH — Robert

Travelled to:

1 × Australia
1 × Canada
1 × China
1 × Germany
1 × Japan
11 × USA
3 × France
3 × United Kingdom
4 × Italy

Collaborated with:

A.Oliveras A.Rubio ∅ E.Rodríguez-Carbonell G.Godoy P.Nivela J.M.Rivero H.Comon H.Ganzinger I.Abío M.Bofill S.K.Lahiri M.Á.Vallejo F.Orejas M.Deters P.J.Stuckey R.Asín J.Larrosa G.Faure T.Hillenbrand A.Riazanov A.Voronkov P.Narendran M.Rusinowitch G.Hagen C.Tinelli

Talks about:

order (8) constraint (7) theori (7) sat (6) modulo (4) paramodul (3) rewrit (3) deduct (3) optim (3) claus (3)

Person: Robert Nieuwenhuis

DBLP: Nieuwenhuis:Robert

Facilitated 2 volumes:

Contributed to:

2012

2011

2009

2008

2007

2006

2005

2004

2001

2000

1999

1998

1997

1996

1995

1994

1993

1992

1990

Wrote 32 papers:

IJCAR-2012-Nieuwenhuis #challenge #satisfiability #smt: SAT and SMT Are Still Resolution: Questions and Challenges (RN), pp. 10–13.
SAT-2011-AbioDNS: Reducing Chaos in SAT-Like Search: Finding Solutions Close to a Given One (IA, MD, RN, PJS), pp. 273–286.
SAT-2011-AbioNOR #constraints #pseudo #revisited: BDDs for Pseudo-Boolean Constraints — Revisited (IA, RN, AO, ERC), pp. 61–75.
SAT-2009-AsinNOR #network: Cardinality Networks and Their Applications (RA, RN, AO, ERC), pp. 167–180.
SAT-2009-LarrosaNOR #bound #branch #generative #optimisation: Branch and Bound for Boolean Optimization and the Generation of Optimality Certificates (JL, RN, AO, ERC), pp. 453–466.
SAT-2009-Nieuwenhuis #algorithm #modulo theories #satisfiability: SAT Modulo Theories: Enhancing SAT with Special-Purpose Algorithms (RN), p. 1.
CAV-2008-BofillNORR #smt: The Barcelogic SMT Solver (MB, RN, AO, ERC, AR), pp. 294–298.
SAT-2008-FaureNOR #formal method #linear #satisfiability: SAT Modulo the Theory of Linear Arithmetic: Exact, Inexact and Commercial Solvers (GF, RN, AO, ERC), pp. 77–90.
RTA-2007-NieuwenhuisORR #challenge #modulo theories #satisfiability: Challenges in Satisfiability Modulo Theories (RN, AO, ERC, AR), pp. 2–18.
CAV-2006-LahiriNO #abstraction #performance #smt: SMT Techniques for Fast Predicate Abstraction (SKL, RN, AO), pp. 424–437.
SAT-2006-NieuwenhuisO #modulo theories #on the #optimisation #problem #satisfiability: On SAT Modulo Theories and Optimization Problems (RN, AO), pp. 156–169.
CAV-2005-NieuwenhuisO #difference #logic: DPLL(T) with Exhaustive Theory Propagation and Its Application to Difference Logic (RN, AO), pp. 321–334.
RTA-2005-NieuwenhuisO #congruence: Proof-Producing Congruence Closure (RN, AO), pp. 453–468.
CAV-2004-GanzingerHNOT #performance: DPLL( T): Fast Decision Procedures (HG, GH, RN, AO, CT), pp. 175–188.
IJCAR-2001-GanzingerNN: Context Trees (HG, RN, PN), pp. 242–256.
IJCAR-2001-NieuwenhuisHRV #evaluation #on the #proving #theorem proving: On the Evaluation of Indexing Techniques for Theorem Proving (RN, TH, AR, AV), pp. 257–271.
LICS-2001-GodoyN #constraints #deduction #monad #on the: On Ordering Constraints for Deduction with Built-In Abelian Semigroups, Monoids and Groups (GG, RN), pp. 38–47.
LICS-2000-GodoyN: Paramodulation with Built-in Abelian Groups (GG, RN), pp. 413–424.
CADE-1999-Nieuwenhuis #constraints #deduction: Invited Talk: Rewrite-based Deduction and Symbolic Constraints (RN), pp. 302–313.
LICS-1999-BofillGNR #order: Paramodulation with Non-Monotonic Orderings (MB, GG, RN, AR), pp. 225–233.
RTA-1999-NieuwenhuisR #constraints #order: Solved Forms for Path Ordering Constraints (RN, JMR), pp. 1–15.
LICS-1998-ComonNNR #order #problem: Decision Problems in Ordered Rewriting (HC, PN, RN, MR), pp. 276–286.
CADE-1997-NieuwenhuisRV #algorithm #automation #data type #deduction #kernel #named #similarity: Dedan: A Kernel of Data Structures and Algorithms for Automated Deduction with Equality Clauses (RN, JMR, MÁV), pp. 49–52.
LICS-1996-Nieuwenhuis #decidability: Basic Paramodulation and Decidable Theories (RN), pp. 473–482.
LICS-1995-ComonNR #constraints #order #theorem proving: Orderings, AC-Theories and Symbolic Constraint Solving (HC, RN, AR), pp. 375–385.
RTA-1995-Nieuwenhuis #constraints #on the #proving: On Narrowing, Refutation Proofs and Constraints (RN), pp. 56–70.
CADE-1994-NieuwenhuisR #constraints: AC-Superposition with Constraints: No AC-Unifiers Needed (RN, AR), pp. 545–559.
RTA-1993-NivelaN #first-order: Saturation of First-Order (Constrained) Clauses with the Saturate System (PN, RN), pp. 436–440.
RTA-1993-RubioN #order: A Precedence-Based Total AC-Compatible Ordering (AR, RN), pp. 374–388.
CADE-1992-NieuwenhuisR #proving #theorem proving: Theorem Proving with Ordering Constrained Clauses (RN, AR), pp. 477–491.
ESOP-1992-NieuwenhuisR: Basic Superposition is Complete (RN, AR), pp. 371–389.
CADE-1990-NieuwenhuisOR #implementation #named: TRIP: An Implementation of Clausal Rewriting (RN, FO, AR), pp. 667–668.