Robert Nieuwenhuis' main publications

Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456

Main publications

2007

Robert Nieuwenhuis and Albert Oliveras
Fast Congruence Closure and Extensions .
Information and Computation, 205(4):557-580, April 2007.
paper (.pdf) © Elsevier Science

2006

Robert Nieuwenhuis, Albert Oliveras and Cesare Tinelli
Solving SAT and SAT Modulo Theories: From an Abstract Davis-Putnam-Logemann-Loveland Procedure to DPLL(T).
Journal of the ACM, 53(6), 937-977, November 2006.
paper (.pdf) © ACM Press

Robert Nieuwenhuis and Albert Oliveras
On SAT Modulo Theories and Optimization Problems..
9th Int. Conf. on Theory and Applications of Satisfiability Testing (SAT), August 2006, Seattle.
paper (.pdf) © Springer-Verlag

Shuvendu Lahiri, Robert Nieuwenhuis and Albert Oliveras
SMT Techniques for Predicate Abstraction.
18th International Conference on Computer Aided Verification (CAV), August 2006, Seattle.
paper (.pdf) © Springer-Verlag

Clark Barrett, Robert Nieuwenhuis, Albert Oliveras and Cesare Tinelli
Splitting on Demand in Satisfiability Modulo Theories.
13th Int. Conf. Logic for Programming, Artif. Intell. and Reasoning (LPAR), November 2006, Phnom Penh.
paper (.pdf) © Springer-Verlag

2005

Robert Nieuwenhuis and Albert Oliveras
Decision procedures for SAT, SAT Modulo Theories and Beyond. The BarcelogicTools. (Invited Paper).
12th Int. Conf. Logic for Programming, Artif. Intell. and Reasoning (LPAR), December 2005, Jamaica.
paper (.ps.gz) © Springer-Verlag

Robert Nieuwenhuis (Ed.)
Automated Deduction- CADE-20
Proceedings of the 20th International Conference (CADE 2005).
Volume 3632 of Lecture Notes in Computer Science. © Springer-Verlag.

Robert Nieuwenhuis and Albert Oliveras
DPLL(T) with Exhaustive Theory Propagation and its Application to Difference Logic.
17th International Conference on Computer Aided Verification (CAV), July 2005, Edinburgh.
paper (.pdf) © Springer-Verlag

Robert Nieuwenhuis, Albert Oliveras and Cesare Tinelli
Abstract DPLL and Abstract DPLL Modulo Theories.
11th Int. Conf. on Logics for Programming, AI and Reasoning (LPAR)
Montevideo, March 2005. Springer LNAI 3452, pp 36-50.
paper (.pdf) © Springer-Verlag

Robert Nieuwenhuis and Albert Oliveras.
Proof-Producing Congruence closure.
16th International Conference on Rewriting Techniques and Applications (RTA)
April 19 - 21, 2005 Nara, Japan. Springer LNCS 3467, pp 453-468.
paper (.pdf) © Springer-Verlag

2004

Harald Ganzinger, Robert Nieuwenhuis and Pilar Nivela
Fast Term Indexing with Coded Context Trees
Journal of Automated Reasoning, 32 (2): 103-120, February 2004.
Paper © Kluwer

Guillem Godoy and Robert Nieuwenhuis
Constraint Solving for Orderings Compatible with Abelian Semigroups, Monoids and Groups
Constraints 9(3), 167-192, July 2004.
Paper © Kluwer

Guillem Godoy and Robert Nieuwenhuis
Superposition with Completely Built-in Abelian Groups
Journal of Symbolic Computation. 37(1), January 2004, 1-33.
Paper © Elsevier Science

Guillem Godoy, Robert Nieuwenhuis and Ashish Tiwari
Classes of Term Rewrite Systems with Polynomial Confluence Problems
ACM Transactions on Computational Logic (TOCL). 5(2), April 2004
Paper © ACM

Harald Ganzinger, George Hagen, Robert Nieuwenhuis, Albert Oliveras, and Cesare Tinelli
DPLL(T): Fast Decision Procedures
16th International Conference on Computer Aided Verification (CAV), July 2004, Boston (USA).
[ Paper © Springer-Verlag | Detailed experimental results ]

2003

Anatoli Degtyarev, Robert Nieuwenhuis and Andrei Voronkov
Stratified Resolution
Journal of Symbolic Computation (JSC) 36(1-2):77-99, July-August 2003.
Paper © Elsevier Science

Robert Nieuwenhuis and Albert Oliveras.
Congruence closure with integer offsets.
10th Int. Conf. on Logics for Programming, AI and Reasoning (LPAR), Sept. 2003
paper (.ps) © Springer-Verlag

Hubert Comon, Paliath Narendran, Robert Nieuwenhuis and Michael Rusinowitch.
Deciding the Confluence of Ordered Rewriting.
ACM Transactions on Computational Logic (TOCL) 4(1), January 2003.
Paper © ACM

Miquel Bofill, Guillem Godoy, Robert Nieuwenhuis and Albert Rubio
Paramodulation and Knuth-Bendix Completion with Nontotal and Nonmonotonic Orderings.
Journal of Automated Reasoning 30(1), 99-120, Jan 2003.
Paper © Kluwer.

Robert Nieuwenhuis (Ed.)
Rewriting Techniques and Applications
Proceedings of the 14th International Conference (RTA 2003).
Volume 2706 of Lecture Notes in Computer Science, ISBN 3-540-40254-3. © Springer-Verlag.

2002

Robert Nieuwenhuis and Jose Miguel Rivero
Practical Algorithms for Deciding Path Ordering Constraint Satisfaction.
Information and Computation. 178(2):422-440,2002.
Paper © Academic Press

Robert Nieuwenhuis
The impact of CASC in the development of automated deduction systems .
(Guest editoral) AI Communications 15(2-3), 2002.
Paper at IOS Press © IOS Press

Robert Nieuwenhuis (Ed.)
Procs. 2002 Workshop on the Implementation of Logics.
October 2002, Tbilisi, Georgia.
Electronic version of the proceedings.

2001

Guillem Godoy and Robert Nieuwenhuis
On Ordering Constraints for Deduction with Built-In Abelian Semigroups, Monoids and Groups
Procs. 16th Annual IEEE Symposium on Logic in Computer Science (LICS)
Boston, USA, 2001.
Long paper © IEEE and Slides

Harald Ganzinger, Robert Nieuwenhuis and Pilar Nivela
Context Trees
Int. Joint Conf. On Automated Reasoning (IJCAR), Siena, Italy, 2001.
Paper © Springer-Verlag

Robert Nieuwenhuis, Thomas Hillenbrand, Alexander Riazanov and Andrei Voronkov
On the Evaluation of Indexing Techniques for Theorem Proving
Int. Joint Conf. On Automated Reasoning (IJCAR), Siena, Italy, 2001.
Paper © Springer-Verlag

Hubert Comon, Guillem Godoy and Robert Nieuwenhuis
The Confluence of Ground Term Rewrite Systems is Decidable in Polynomial Time
42nd Annual IEEE Symposium on Foundations of Computer Science (FOCS)
Las Vegas, Nevada, USA, 2001.
Paper © IEEE and Slides

Harald Ganzinger and Robert Nieuwenhuis
Constraints and Theorem Proving
Chapter of: Comon, Marche and Treinen, (Eds)
Constraints in Computational Logics: Theory and Applications
Chapter (gzipped postscript, 128KB)
Springer LNCS Vol. 2002, pages 159-201, 2001. © Springer-Verlag

Robert Nieuwenhuis
Recent trends in rewrite-based and paramodulation-based deduction (invited paper)
International Workshop on Rewriting in Proof and Computation (RPC'01)
Sendai, Japan, October 25-27, 2001.
Paper

Robert Nieuwenhuis and Andrei Voronkov (Eds.)
Logics for Programming, AI and Reasoning
Proceedings of the 8th International Conference (LPAR 2001).
Volume 2250 of Lecture Notes in AI, ISBN 3-540-42957-3. © Springer-Verlag.

Robert Nieuwenhuis and Albert Rubio
Paramodulation-Based Theorem Proving.
Chapter of Handbook of Automated Reasoning
Edited by Alan Robinson and Andrei Voronkov.
ISBN 0-444-82949-0. © Elsevier Science and MIT Press, 2001.
Chapter (gzipped postscript, 169KB)

2000

Guillem Godoy and Robert Nieuwenhuis
Paramodulation with Built-In Abelian Groups
Procs. 15th Annual IEEE Symposium on Logic in Computer Science (LICS), pages 413-424,
Santa Barbara, USA, 2000.
Paper © IEEE and Long paper

Hubert Comon and Robert Nieuwenhuis
Induction = I-Axiomatization + First-Order Consistency .
Information and Computation 159(1/2):151-186, May 2000. © Academic Press
Paper

Miquel Bofill, Guillem Godoy, Robert Nieuwenhuis and Albert Rubio
Modular Redundancy for Theorem Proving .
In Procs. FroCoS 2000 © Springer-Verlag
LNCS 1794, pages 186-199, Nancy, France, April, 2000. Springer-Verlag.
Paper

1999

Robert Nieuwenhuis
Rewrite-based Deduction and Symbolic Constraints (Invited Paper) .
In Procs. 16th International Conference on Automated Deduction (CADE) © Springer-Verlag
LNCS/LNAI 1632, pages 302-313, Trento, Italy, July, 1999. Springer-Verlag.
Paper

Robert Nieuwenhuis and Jose Miguel Rivero
Solved Forms for Path Ordering Constraints .
In Procs. 10th International Conference on Rewriting Techniques and Applications (RTA) © Springer-Verlag
LNCS 1631, pages 1-15, Trento, Italy, July, 1999. Springer-Verlag.
Paper. Test software.

Miquel Bofill, Guillem Godoy, Robert Nieuwenhuis and Albert Rubio
Paramodulation with Non-Monotonic Orderings .
In Procs. 14th Annual IEEE Symposium on Logic in Computer Science (LICS)
IEEE Comp. Sc. Press, pages 225-234, Trento, Italy, July, 1999.
Paper

1998

Hubert Comon, Paliath Narendran, Robert Nieuwenhuis and Michael Rusinowitch.
Decision Problems in Ordered Rewriting.
13th Annual IEEE Symposium on Logic in Computer Science (LICS), Indianapolis, USA, 1998.
Paper

Robert Nieuwenhuis.
Decidability and Complexity Analysis by Basic Paramodulation .
Information and Computation, 147:1-21, 1998.
Paper

1997

Robert Nieuwenhuis, Jose Miguel Rivero and Miguel Angel Vallejo.
Dedam: a kernel of data structures and algorithms for automated deduction with equality clauses (System description) .
Springer-Verlag Lecture Notes in Artificial Intelligence 1249. 14th International Conference on Automated Deduction (CADE) © Springer-Verlag Townsville, Australia, July 1997.
Paper

Robert Nieuwenhuis, Jose Miguel Rivero and Miguel Angel Vallejo.
The Barcelona Prover .
Journal of Automated Reasoning , 18:171-176, February 1997.
Paper

Robert Nieuwenhuis and Albert Rubio.
Paramodulation with Built-in AC-Theories and Symblic Constraints .
Journal of Symbolic Computation , 23:1-21, May 1997.
Paper

1996

Robert Nieuwenhuis.
Basic Paramodulation and Decidable Theories .
In 11th Annual IEEE Symposium on Logic in Computer Science (LICS), New Brunswick, NJ, USA, July, 1996.
Paper

1995

Hubert Comon, Robert Nieuwenhuis, and Albert Rubio.
Orderings, AC-Theories and Symbolic Constraint Solving .
In Tenth Annual IEEE Symposium on Logic in Computer Science (LICS) , San Diego, California, USA, June, 1995.
Paper

Albert Rubio and Robert Nieuwenhuis.
A total AC-compatible ordering based on RPO .
Theoretical Computer Science , 142(2):209-227, May 15, 1995.
Paper

Robert Nieuwenhuis.
On Narrowing, Refutation Proofs and Constraints .
In J. Hsiang, editor, 6th International Conference on Rewriting Techniques and Applications (RTA) © Springer-Verlag
LNCS 914, pages 56-70, Kaiserslautern, Germany, April 4-7, 1995. Springer-Verlag.
Paper

Robert Nieuwenhuis and Albert Rubio.
Theorem Proving with Ordering and Equality Constrained Clauses.
Journal of Symbolic Computation , 19(4):321-351, April 1995.
Paper

1994

Robert Nieuwenhuis and Albert Rubio.
AC-Superposition with constraints: No AC-unifiers needed .
In Allan Bundy, editor, 12th International Conference on Automated Deduction © Springer-Verlag , LNAI, Nancy, France, June 1994. Springer-Verlag.
Paper

1993

Robert Nieuwenhuis.
Simple LPO constraint solving methods .
Information Processing Letters , 47:65-69, August 1993.
Paper

Pilar Nivela and Robert Nieuwenhuis.
Practical results on the saturation of full first-order clauses: Experiments with the Saturate system. (System description) .
In C. Kirchner, editor, 5th International Conference on Rewriting Techniques and Applications (RTA) © Springer-Verlag , LNCS 690, Montreal, Canada, June 16-18, 1993. Springer-Verlag.
Paper

Albert Rubio and Robert Nieuwenhuis.
A precedence-based total AC-compatible ordering .
In C. Kirchner, editor, 5th International Conference on Rewriting Techniques and Applications (RTA) © Springer-Verlag , LNCS 690, pages 374-388, Montreal, Canada, June 16-18, 1993.
Paper (longer version)

1992 and before

Robert Nieuwenhuis and Albert Rubio.
Theorem Proving with Ordering Constrained Clauses .
In Deepak Kapur, editor, 11th CADE , LNAI 607, pages 477-491, Saratoga Springs, New York, 1992.

Robert Nieuwenhuis and Albert Rubio.
Basic superposition is complete .
In B. Krieg-Brückner, editor, European Symposium on Programming , LNCS 582, pages 371-390, Rennes, France, February 26-28, 1992. Springer-Verlag.

Robert Nieuwenhuis and Pilar Nivela.
Efficient deduction in equality Horn logic by Horn-completion .
Information Processing Letters , 39(1):1-6, July 1991.

Robert Nieuwenhuis, Fernando Orejas, and Albert Rubio.
TRIP: An Implementation of Clausal Rewriting .
In Mark E. Stickel, editor, 10th International Conference on Automated Deduction , LNAI 449, pages 667-668, Kaiserslautern, FRG, July 24-27, 1990. Springer-Verlag.

Robert Nieuwenhuis and Fernando Orejas.
Clausal Rewriting .
In Stéphane Kaplan and Mitsuhiro Okada, editors, Conditional and Typed Rewriting Systems, 2nd International Workshop , LNCS 516, pages 246-258, Montreal, Canada, June 11-14, 1990. Springer-Verlag.

Robert Nieuwenhuis and Fernando Orejas.
Clausal Rewriting, Applications and Implementation .
In 7th Workshop on Specification of Abstract Data Types , LNCS 534, pages 204-219. Springer-Verlag, 1990.

Robert Nieuwenhuis.
Theorem Proving in first-order logic with equality by clausal rewriting and completion .
PhD thesis, Technical University of Catalonia, Spain, 1990.