BibSLEIGH
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
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 DBLP: Nieuwenhuis:Robert

Facilitated 2 volumes:

CADE 2005Ed
RTA 2003Ed

Contributed to:

IJCAR 20122012
SAT 20112011
SAT 20092009
CAV 20082008
SAT 20082008
RTA 20072007
CAV 20062006
SAT 20062006
CAV 20052005
RTA 20052005
CAV 20042004
IJCAR 20012001
LICS 20012001
LICS 20002000
CADE 19991999
LICS 19991999
RTA 19991999
LICS 19981998
CADE 19971997
LICS 19961996
LICS 19951995
RTA 19951995
CADE 19941994
RTA 19931993
CADE 19921992
ESOP 19921992
CADE 19901990

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.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.