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
Robert Nieuwenhuis' main publications

Main publications

2005

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.
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.
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
Term Indexing Techniques for Automated Reasoning (invited talk)
Eighth Workshop on Automated Reasoning (ARW'2001)
University of York (UK), March 22-23, 2001
Abstract

Robert Nieuwenhuis
New Ideas for Term Indexing
Dagstuhl Seminar on Deduction
International Conference and Research Centre for Computer Science,
Schloss Dagstuhl, Wadern, Alemania, Febrero de 2001.
Abstracts Seminar Info

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.