@ARTICLE{ArRaRu2,
AUTHOR = {Alessandro Armando and Silvio Ranise and Micha\"el Rusinowitch},
TITLE = "A rewriting approach to satisfiability procedures",
JOURNAL = "Information and Computation",
YEAR = 2002,
VOLUME = "To appear"}

@ARTICLE{BacTiwVig,
AUTHOR = "Leo Bachmair and Ashish Tiwari and Laurent Vigneron",
TITLE = "Abstract {C}ongruence {C}losure",
JOURNAL = "Journal of Automated Reasoning",
YEAR = 2002,
VOLUME = "To appear"}

@INPROCEEDINGS{BarrettEtAl1,
AUTHOR = "Clark W. Barrett and David L. Dill and Aaron Stump",
TITLE = "A framework for cooperating decision procedures",
BOOKTITLE = "Proceedings of CADE-17",
EDITOR = "David McAllester",
YEAR = 2000,
SERIES = "LNAI",
VOLUME = 1831,
PAGES = "79--97",
PUBLISHER = "Springer"}

@INPROCEEDINGS{BarrettEtAl2,
AUTHOR = "Clark W. Barrett and David L. Dill and Aaron Stump",
TITLE = "A generalization of {S}hostak's method for combining decision procedures",
BOOKTITLE = "Proceedings of the 4th Workshop on Frontiers of Combining Systems",
YEAR = 2002,
EDITOR = "Alessandro Armando",
PUBLISHER = "Springer",
SERIES = "LNCS",
VOLUME = 2309}

@PHDTHESIS{bonacinaphdthesis,
AUTHOR = "Maria Paola Bonacina",
TITLE = "Distributed automated deduction",
SCHOOL = "Department of Computer Science, State University of New York at Stony Brook",
MONTH = "December",
YEAR = 1992}

@ARTICLE{bonacinaTCScompletion,
AUTHOR = "Maria Paola Bonacina and Jieh Hsiang",
TITLE = "Towards a foundation of completion procedures as semidecision procedures",
JOURNAL = "Theoretical Computer Science",
MONTH = "July",
YEAR = 1995,
VOLUME = 146,
PAGES = "199--242"}

@ARTICLE{CTRS90,
AUTHOR = "Maria Paola Bonacina and Jieh Hsiang",
TITLE = "Completion {P}rocedures as semidecision procedures",
JOURNAL = "In Stephan Haplon and Mitsihiro Okada (editors) Proceedings of the 2nd International Workshop on Conditional and Typed Term Rewriting Systems (CTRS)",
PUBLISHER = "Springer-Verlag",
MONTH = "July",
YEAR = 1991,
VOLUME = "LNCS 516",
PAGES = "206--232"}

@INCOLLECTION{Bonacinataxonomy,
AUTHOR = "Maria Paola Bonacina",
TITLE = "A taxonomy of theorem-proving strategies",
BOOKTITLE = "Artificial Intelligence Today -- Recent Trends and Developments",
EDITOR = "Michael J. Wooldridge and Manuela Veloso",
SERIES = "Lecture Notes in Artificial Intelligence",
VOLUME = 1600,
PAGES = "43--84",
PUBLISHER = "Springer",
MONTH = "August",
YEAR = 1999}

@BOOK{nqthm,
AUTHOR = "Robert S. Boyer and J. Strother Moore",
TITLE = "A {C}omputational {L}ogic {H}andbook",
PUBLISHER = "Academic Press",
YEAR = 1988}

@INPROCEEDINGS{CollinsSyme,
AUTHOR = "Graham Collins and Donald Syme",
TITLE = "A theory of finite maps",
BOOKTITLE = "Proceedings of the Conference on Higher Order Logic Theorem Proving and its Applications",
YEAR = 1995,
SERIES = "LNCS",
PUBLISHER = "Springer"}

@INPROCEEDINGS{CVC,
AUTHOR = "Aaron Stump and Clark W. Barrett and David L. Dill",
TITLE = "{CVC}: a {C}ooperating {V}alidity {C}hecker",
BOOKTITLE = "Proceedings of the 14th Conference on Computer Aided Verification",
EDITOR = "Kim G. Larsen and Ed Brinksma",
YEAR = 2002,
PUBLISHER = "Springer",
SERIES = "LNCS",
VOLUME = "To appear"}

@INPROCEEDINGS{CyrLinSha,
AUTHOR = "David Cyrluk and Patrick Lincoln and Natarajan Shankar",
TITLE = {On {S}hostak's decision procedure for combination of theories},
BOOKTITLE = "Proceedings of CADE-13",
EDITOR = "Michael A. McRobbie and John K. Slaney",
YEAR = 1996,
SERIES = "LNAI",
VOLUME = 1104,
PAGES = "463--477",
PUBLISHER = "Springer"}

@INCOLLECTION{Der82,
AUTHOR = "Nachum Dershowitz",
TITLE = "Orderings for term-rewriting systems",
BOOKTITLE = "Theoretical Computer Science",
YEAR = 1982,
VOLUME = "17",
PAGES = "279--301"}

@INCOLLECTION{DerJou90,
AUTHOR = "Nachum Dershowitz and Jean-Pierre Jouannaud",
TITLE = "Rewrite systems",
EDITOR = "Jan van Leeuwen",
BOOKTITLE = "Handbook of Theoretical Computer Science",
YEAR = 1990,
VOLUME = "B",
PUBLISHER = "Elsevier",
PAGES = "243--320"}

@BOOK{HOL,
AUTHOR = "Michael Gordon and Tom F. Melham",
TITLE = "Introduction to {HOL} - {A} {T}heorem {P}roving {E}nvironment for {H}igher {O}rder {L}ogic",
PUBLISHER = "Cambridge University Press",
YEAR = 1993}

@ARTICLE{GHuet,
AUTHOR = "G\'erard Huet",
TITLE = "A complete proof of correctness of the {K}nuth-{B}endix completion algorithm",
JOURNAL = "Journal of Computing System Science",
YEAR = 1981,
VOLUME = 23,
PAGES = "11--21"}

@INCOLLECTION{HuetOppen,
AUTHOR = {G\'erard Huet and Derek C. Oppen},
TITLE = "Equations and {R}ewrite {R}ules: {A} {S}urvey",
BOOKTITLE = "Formal Language Theory",
EDITOR = "Ronald V.Book",
YEAR = 1980,
PUBLISHER = "Academic Press"}

@INPROCEEDINGS{DKonSho,
AUTHOR = "Deepak Kapur",
TITLE = "Shostak's {C}ongruence {C}losure as {C}ompletion",
BOOKTITLE = "Proceedings of the 8th RTA",
EDITOR = "Hubert Comon",
YEAR = 1997,
PUBLISHER = "Springer",
PAGES = "23--37",
SERIES = "LNCS",
VOLUME = 1232}

@INCOLLECTION{KB70,
AUTHOR = {D. E. Knuth and P. B. Bendix},
TITLE = {Simple {W}ord {P}roblems in {U}niversal {A}lgebras},
YEAR = 1970,
BOOKTITLE = {In J. Leech, editor, Computational Problems in Abstract Algebra},
PUBLISHER = {Pergamon Press},
ADDRESS = {Oxford},
PAGES = {263--297},
KEYWORDS = {}}

@ARTICLE{GRASP,
AUTHOR = {Jo{\~{a}}o Marques Silva and Karem A. Sakallah},
TITLE = "{GRASP}: a search algorithm for propositional satisfiability",
JOURNAL = "IEEE Transactions on Computers",
YEAR = 1999,
VOLUME = 48,
NUMBER = 5,
PAGES = "506--521"}

@INPROCEEDINGS{Chaff,
AUTHOR = "Matthew W. Moskewicz and Conor F. Madigan and Ying Zhao and Lintao Zhang and Sharad Malik",
TITLE = "Chaff: {E}ngineering an {E}fficient {SAT} {S}olver",
BOOKTITLE = "Proceedings of the 39th Design Automation Conference",
YEAR = 2001}

@ARTICLE{NO79,
AUTHOR = "Greg Nelson and Derek C. Oppen",
TITLE = "Simplification by cooperating decision procedures",
JOURNAL = "ACM Transactions on Programming Languages and Systems",
YEAR = 1979,
VOLUME = 1,
NUMBER = 2,
PAGES = "245--257"}

@ARTICLE{NO80,
AUTHOR = "Greg Nelson and Derek C. Oppen",
TITLE = "Fast {D}ecision {P}rocedures {B}ased on {C}ongruence {C}losure",
JOURNAL = "Journal of the Associate for Computing Machinery",
YEAR = 1980,
VOLUME = 27,
NUMBER = 2,
PAGES = "356--364"}

@INCOLLECTION{NR01,
AUTHOR = "Robert Nieuwenhuis and Albert Rubio",
TITLE = "Paramodulation-{B}ased {T}heorem {P}roving",
BOOKTITLE = "Handbook of Automated Reasoning",  
EDITOR = "A. Robinson and A. Voronkov",
YEAR = 2001,
PAGES = "371--443"}

@ARTICLE{Oppen,
AUTHOR = "Derek C. Oppen",
TITLE = "Complexity, {C}onvexity and {C}ombinations of {T}heories",
JOURNAL = "Theoretical Computer Science",
YEAR = 1980,
VOLUME = 12,
PAGES = "291-302"}

@MISC{Otter,
AUTHOR = "William W. McCune",
TITLE = "Otter: {A}n {A}utomated {D}eduction {S}ystem",
NOTE = "(Online) Available: \url{http://www-unix.mcs.anl.gov/AR/otter/}",
YEAR = 2002,
MONTH = "November",
DAY = "01"}

@INPROCEEDINGS{PVS,
AUTHOR = "Sam Owre and J. M. Rushby and Natarajan Shankar",
TITLE = "{PVS}: a prototype verification system",
BOOKTITLE = "Proceedings of CADE-11",
EDITOR = "Deepak Kapur",
YEAR = 1992,
PUBLISHER = "Springer Verlag",
PAGES = "748--752",
SERIES = "LNAI",
VOLUME = 607}

@TECHREPORT{GNelson,
AUTHOR = "Greg Nelson",
TITLE = "Techniques for {P}rogram {V}erification",
INSTITUTION = "Xerox Palo Alto Research Center",
MONTH = "June",
YEAR = 1981}

@INPROCEEDINGS{SehgalAK,
AUTHOR = {Alessandro Armando and Maria Paola Bonacina and Silvio Ranise
and Micha\"el Rusinowitch and Aditya Kumar Sehgal},
TITLE = "High-performance deduction for verification:
a case study in the theory of arrays",
BOOKTITLE = "Notes of the Workshop on Verification,
Third Federated Logic Conference (FLoC02)",
EDITOR = {Serge Autexier and Heiko Mantel},
YEAR = 2002,
PAGES = "103--112"}

@TECHREPORT{simplify,
AUTHOR = "Dave L. Detlefs and Greg Nelson and Jim Saxe",
TITLE = "Simplify: the {ESC} {T}heorem {P}rover",
YEAR = 1996,
INSTITUTION = "{DEC}"}

@INPROCEEDINGS{ShaonSho,
AUTHOR = {Harald Rue{\ss} and Natarajan Shankar},
TITLE = "Deconstructing {S}hostak",
BOOKTITLE = "Proceedings of the 16th IEEE Symposium on Logic in Computer Science",
YEAR = 2001}

@INCOLLECTION{Rus91,
AUTHOR = {Micha\"el Rusinowitch},
TITLE = {Theorem-proving with resolution and superposition},
YEAR = 1991,
BOOKTITLE = {Journal of Symbolic Computing},
PAGES = {21--50},
VOLUME = 11,
KEYWORDS = {}}

@ARTICLE{JE,
AUTHOR = "Stephan Schulz",
TITLE = "E -- {A} brainiac theorem prover",
JOURNAL = "AI Communications",
YEAR = 2002,
VOLUME = "To appear"}

@ARTICLE{ShostakCC2,
AUTHOR = "Robert E. Shostak",
TITLE = "Deciding combinations of theories",
JOURNAL = "Journal of the ACM",
YEAR = 1984,
VOLUME = 31,
NUMBER = 1,
PAGES = "1--12"}

@ARTICLE{ShostakCC1,
AUTHOR = "Robert E. Shostak",
TITLE = "An {A}lgorithm for {R}easoning about {E}quality",
JOURNAL = "Communications of the ACM",
YEAR = 1978,
VOLUME = 21,
NUMBER = 7,
PAGES = "583--585"}

@MISC{SPASS,
KEY = "SPASS",
TITLE = "{SPASS} {H}ome {P}age",
NOTE = "(Online) Available: \url{http://spass.mpi-sb.mpg.de/}",
YEAR = 2002,
MONTH = "November",
DAY = "01"}

@INPROCEEDINGS{StuBaDiLe,
AUTHOR = "Aaron Stump and Clark W. Barrett and David L. Dill and Jeremy R. Levitt",
TITLE = "A decision procedure for an extensional theory of arrays",
BOOKTITLE = "Proceedings of the 16th IEEE Symposium on Logic in Computer Science",
YEAR = 2001}

@MISC{SVCex,
KEY = "SVC",
TITLE = "Index of /{SVC}/svc-1.1/examples",
NOTE = "(Online) Available: \url{http://sprout.stanford.edu/SVC/svc-1.1/examples/}",
YEAR = 2002,
MONTH = "November",
DAY = "01"}

@PHDTHESIS{ATthesis,
AUTHOR = "Ashish Tiwari",
TITLE = "Decision procedures in automated deduction",
YEAR = 2000,
SCHOOL = "Department of Computer Science, State University of New York at Stony Brook"}

@MISC{TPTP,
AUTHOR = "Christian B. Suttner and Geoff Sutcliffe",
TITLE = "The {TPTP} {P}roblem {L}ibrary for {A}utomated {T}heorem {P}roving",
NOTE = "(Online) Available: \url{http://www.cs.miami.edu/~tptp/}",
YEAR = 2002,
MONTH = "November",
DAY = "01"}