Robert Nieuwenhuis - researchr alias

researchr

You are not signed in
Sign in
Sign up

2011

2010

Practical algorithms for unsatisfiability proof and core generation in SAT solversRoberto Javier Asín Achá, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell. aicom, 23(2-3):145-157, 2010. [doi]

Hard problems in max-algebra, control theory, hypergraphs and other areasMarc Bezem, Robert Nieuwenhuis, Enric Rodríguez-Carbonell. ipl, 110(4):133-138, 2010. [doi]

SAT Modulo Theories: Getting the Best of SAT and Global Constraint FilteringRobert Nieuwenhuis. cp 2010: 1-2 [doi]

2009

Cardinality Networks and Their ApplicationsRoberto Asín, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell. sat 2009: 167-180 [doi]

Branch and Bound for Boolean Optimization and the Generation of Optimality CertificatesJavier Larrosa, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell. sat 2009: 453-466 [doi]

SAT Modulo Theories: Enhancing SAT with Special-Purpose AlgorithmsRobert Nieuwenhuis. sat 2009: 1 [doi]

2008

Efficient Generation of Unsatisfiability Proofs and Cores in SATRoberto Asín, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell. lpar 2008: 16-30 [doi]

The Max-Atom Problem and Its RelevanceMarc Bezem, Robert Nieuwenhuis, Enric Rodríguez-Carbonell. lpar 2008: 47-61 [doi]

Exponential behaviour of the Butkovic-Zimmermann algorithm for solving two-sided linear systems in max-algebraMarc Bezem, Robert Nieuwenhuis, Enric Rodríguez-Carbonell. DAM, 156(18):3506-3509, 2008. [doi]

The Barcelogic SMT SolverMiquel Bofill, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio. cav 2008: 294-298 [doi]

A Write-Based Solver for SAT Modulo the Theory of ArraysMiquel Bofill, Robert Nieuwenhuis, Albert Oliveras, Enric RodrÃguez-Carbonell, Albert Rubio. FMCAD 2008: 1-8 [doi]

SAT Modulo the Theory of Linear Arithmetic: Exact, Inexact and Commercial SolversGermain Faure, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell. sat 2008: 77-90 [doi]

2007

Deduction and Decision Procedures, 30.09. - 05.10.2007Franz Baader, Byron Cook, Jürgen Giesl, Robert Nieuwenhuis, editors, Volume 07401 of Dagstuhl Seminar Proceedings, Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany, 2007.

07401 Executive Summary -- Deduction and Decision ProceduresFranz Baader, Byron Cook, Jürgen Giesl, Robert Nieuwenhuis. dagstuhl 2007: [doi]

07401 Abstracts Collection -- Deduction and Decision ProceduresFranz Baader, Byron Cook, Jürgen Giesl, Robert Nieuwenhuis. dagstuhl 2007: [doi]

Challenges in Satisfiability Modulo TheoriesRobert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio. RTA 2007: 2-18 [doi]

Fast congruence closure and extensionsRobert Nieuwenhuis, Albert Oliveras. iandc, 205(4):557-580, 2007. [doi]

2006

Deduction and Applications, 23.-28. October 2005Franz Baader, Peter Baumgartner, Robert Nieuwenhuis, Andrei Voronkov, editors, Volume 05431 of Dagstuhl Seminar Proceedings, Internationales Begegnungs- und Forschungszentrum für Informatik (IBFI), Schloss Dagstuhl, Germany, 2006.

Splitting on Demand in SAT Modulo TheoriesClark Barrett, Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli. lpar 2006: 512-526 [doi]

SMT Techniques for Fast Predicate AbstractionShuvendu K. Lahiri, Robert Nieuwenhuis, Albert Oliveras. cav 2006: 424-437 [doi]

Solving SAT and SAT Modulo Theories: From an abstract Davis--Putnam--Logemann--Loveland procedure to DPLL(::::T::::)Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli. JACM, 53(6):937-977, 2006. [doi]

On SAT Modulo Theories and Optimization ProblemsRobert Nieuwenhuis, Albert Oliveras. sat 2006: 156-169 [doi]

2005

05431 Abstracts Collection - Deduction and ApplicationsFranz Baader, Peter Baumgartner, Robert Nieuwenhuis, Andrei Voronkov. dagstuhl 2006: [doi]

05431 Executive Summary - Deduction and ApplicationsFranz Baader, Peter Baumgartner, Robert Nieuwenhuis, Andrei Voronkov. dagstuhl 2006: [doi]

Automated Deduction - CADE-20, 20th International Conference on Automated Deduction, Tallinn, Estonia, July 22-27, 2005, ProceedingsRobert Nieuwenhuis, editor, Volume 3632 of Lecture Notes in Computer Science, Springer, 2005.

Decision Procedures for SAT, SAT Modulo Theories and Beyond. The BarcelogicToolsRobert Nieuwenhuis, Albert Oliveras. lpar 2005: 23-46 [doi]

Proof-Producing Congruence ClosureRobert Nieuwenhuis, Albert Oliveras. RTA 2005: 453-468 [doi]

DPLL(T) with Exhaustive Theory Propagation and Its Application to Difference LogicRobert Nieuwenhuis, Albert Oliveras. cav 2005: 321-334 [doi]

2004

2003

Paramodulation and Knuth-Bendix Completion with Nontotal and Nonmonotonic OrderingsMiquel Bofill, Guillem Godoy, Robert Nieuwenhuis, Albert Rubio. JAR, 30(1):99-120, 2003.

Deciding the confluence of ordered term rewrite systemsHubert Comon, Paliath Narendran, Robert Nieuwenhuis, Michaël Rusinowitch. tocl, 4(1):33-55, 2003. [doi]

Stratified resolutionAnatoli Degtyarev, Robert Nieuwenhuis, Andrei Voronkov. JSC, 36(1-2):79-99, 2003. [doi]

Congruence Closure with Integer OffsetsRobert Nieuwenhuis, Albert Oliveras. lpar 2003: 78-90 [doi]

Rewriting Techniques and Applications, 14th International Conference, RTA 2003, Valencia, Spain, June 9-11, 2003, ProceedingsRobert Nieuwenhuis, editor, Volume 2706 of Lecture Notes in Computer Science, Springer, 2003.

2002

The impact of CASC in the development of automated deduction systemsRobert Nieuwenhuis. aicom, 15(2-3):77-78, 2002. [doi]

Practical Algorithms for Deciding Path Ordering Constraint SatisfactionRobert Nieuwenhuis, José Miguel Rivero. iandc, 178(2):422-440, 2002. [doi]

2001

The Confluence of Ground Term Rewrite Systems is Decidable in Polynomial TimeHubert Comon, Guillem Godoy, Robert Nieuwenhuis. focs 2001: 298-307

Context TreesHarald Ganzinger, Robert Nieuwenhuis, Pilar Nivela. cade 2001: 242-256 [doi]

On Ordering Constraints for Deduction with Built-In Abelian Semigroups, Monoids and GroupsGuillem Godoy, Robert Nieuwenhuis. lics 2001: 38-50

On the Evaluation of Indexing Techniques for Theorem ProvingRobert Nieuwenhuis, Thomas Hillenbrand, Alexandre Riazanov, Andrei Voronkov. cade 2001: 257-271 [doi]

Logic for Programming, Artificial Intelligence, and Reasoning, 8th International Conference, LPAR 2001, Havana, Cuba, December 3-7, 2001, ProceedingsRobert Nieuwenhuis, Andrei Voronkov, editors, Volume 2250 of Lecture Notes in Computer Science, Springer, 2001.

Paramodulation-Based Theorem ProvingRobert Nieuwenhuis, Albert Rubio. In John Alan Robinson, Andrei Voronkov, editors, Handbook of Automated Reasoning (in 2 volumes). pages 371-443, Elsevier and MIT Press, 2001.

2000

Modular Redundancy for Theorem ProvingMiquel Bofill, Guillem Godoy, Robert Nieuwenhuis, Albert Rubio. frocos 2000: 186-199

Induction=I-Axiomatization+First-Order ConsistencyHubert Comon, Robert Nieuwenhuis. iandc, 159(1-2):151-186, 2000.

Paramodulation with Built-in Abelian GroupsGuillem Godoy, Robert Nieuwenhuis. lics 2000: 413-424 [doi]

1999

1998

Decision Problems in Ordered RewritingHubert Comon, Paliath Narendran, Robert Nieuwenhuis, Michaël Rusinowitch. lics 1998: 276-286

Decidability and Complexity Analysis by Basic ParamodulationRobert Nieuwenhuis. iandc, 147(1):1-21, 1998.

1997

BarcelonaRobert Nieuwenhuis, José Miguel Rivero, Miguel Ángel Vallejo. JAR, 18(2):171-176, 1997.

Paramodulation with Built-in AC-Theories and Symbolic ConstraintsRobert Nieuwenhuis, Albert Rubio. JSC, 23(1):1-21, 1997.

Dedan: A Kernel of Data Structures and Algorithms for Automated Deduction with Equality ClausesRobert Nieuwenhuis, José Miguel Rivero, Miguel Ángel Vallejo. cade 1997: 49-52

1996

Basic Paramodulation and Decidable Theories (Extended Abstract)Robert Nieuwenhuis. lics 1996: 473-482

An Implementation Kernel for Theorem Proving with Equality ClausesRobert Nieuwenhuis, José Miguel Rivero, Miguel Ángel Vallejo. agp 1996: 89-104

1995

Orderings, AC-Theories and Symbolic Constraint Solving (Extended Abstract)Hubert Comon, Robert Nieuwenhuis, Albert Rubio. lics 1995: 375-385

Theorem Proving with Ordering and Equality Constrained ClausesRobert Nieuwenhuis, Albert Rubio. JSC, 19(4):321-351, 1995.

On Narrowing, Refutation Proofs and ConstraintsRobert Nieuwenhuis. RTA 1995: 56-70

A Total AC-Compatible Ordering Based on RPOAlbert Rubio, Robert Nieuwenhuis. TCS, 142(2):209-227, 1995. [doi]

1994

AC-Superposition with Constraints: No AC-Unifiers NeededRobert Nieuwenhuis, Albert Rubio. cade 1994: 545-559

1993

Program Development: Completion SubsystemHubert Bertling, Harald Ganzinger, Renate Schäfers, Robert Nieuwenhuis, Fernando Orejas. prospectra 1993: 460-494

Simple LPO Constraint Solving MethodsRobert Nieuwenhuis. ipl, 47(2):65-69, 1993.

Saturation of First-Order (Constrained) Clauses with the ::::Saturate:::: SystemPilar Nivela, Robert Nieuwenhuis. RTA 1993: 436-440

A Precedence-Based Total AC-Compatible OrderingAlbert Rubio, Robert Nieuwenhuis. RTA 1993: 374-388

1992

Theorem Proving with Ordering Constrained ClausesRobert Nieuwenhuis, Albert Rubio. cade 1992: 477-491

Basic Superposition is CompleteRobert Nieuwenhuis, Albert Rubio. ESOP 1992: 371-389

1991

Efficient Deduction in Equality Horn Logic by Horn-CompletionRobert Nieuwenhuis, Pilar Nivela. ipl, 39(1):1-6, 1991.

1990

Clausal Rewriting: Applications and ImplementationRobert Nieuwenhuis, Fernando Orejas. adt 1991: 204-219

TRIP: An Implementation of Clausal RewritingRobert Nieuwenhuis, Fernando Orejas, Albert Rubio. cade 1990: 667-668

Clausal RewritingRobert Nieuwenhuis, Fernando Orejas. ctrs 1991: 246-258