@ARTICLE{BG94,
        AUTHOR             = {Bachmair, L. and Ganzinger, H.},
        TITLE              = {Rewrite-based Equational Theorem Proving with Selection and Simplification},
        NUMBER             = {4},
        PAGES              = {217--247},
        JOURNAL            = {Journal of Logic and Computation},
        VOLUME             = {3},
        YEAR               = {1994}
}

@incollection{DBLP:books/el/RV01/NieuwenhuisR01,
  author    = {Robert Nieuwenhuis and
               Albert Rubio},
  title     = {Paramodulation-Based Theorem Proving},
  booktitle = {Handbook of Automated Reasoning},
  year      = {2001},
  pages     = {371-443},
  crossref  = {DBLP:books/el/RobinsonV01},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@book{DBLP:books/el/RobinsonV01,
  editor    = {John Alan Robinson and
               Andrei Voronkov},
  title     = {Handbook of Automated Reasoning (in 2 volumes)},
  publisher = {Elsevier and MIT Press},
  year      = {2001}
}

@inproceedings{DBLP:conf/cade/BachmairGLS92,
  author    = {Leo Bachmair and
               Harald Ganzinger and
               Christopher Lynch and
               Wayne Snyder},
  title     = {Basic Paramodulation and Superposition},
  booktitle = {Automated Deduction - CADE-11, 11th International Conference on Automated
               Deduction, Saratoga Springs, NY, USA, June 15-18, 1992, Proceedings},
  pages     = {462--476},
  year      = {1992},
  crossref  = {DBLP:conf/cade/1992},
  url       = {https://doi.org/10.1007/3-540-55602-8_185},
  doi       = {10.1007/3-540-55602-8_185},
  timestamp = {Mon, 12 Oct 2009 13:08:35 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/cade/BachmairGLS92},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@proceedings{DBLP:conf/cade/1992,
  editor    = {Deepak Kapur},
  title     = {Automated Deduction - CADE-11, 11th International Conference on Automated
               Deduction, Saratoga Springs, NY, USA, June 15-18, 1992, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {607},
  publisher = {Springer},
  year      = {1992},
  isbn      = {3-540-55602-8},
  timestamp = {Wed, 03 Jul 2002 09:55:41 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/cade/1992},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@article{DBLP:journals/iandc/BachmairGLS95,
  author    = {Leo Bachmair and
               Harald Ganzinger and
               Christopher Lynch and
               Wayne Snyder},
  title     = {Basic Paramodulation},
  journal   = {Inf. Comput.},
  volume    = {121},
  number    = {2},
  pages     = {172--192},
  year      = {1995},
  url       = {https://doi.org/10.1006/inco.1995.1131},
  doi       = {10.1006/inco.1995.1131},
  timestamp = {Wed, 06 Jul 2011 21:24:02 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/iandc/BachmairGLS95},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
