L. Bachmair and H. Ganzinger, On restrictions of ordered paramodulation with simplification, Lecture Notes in Computer Science, vol.449, pp.427-441, 1990.
DOI : 10.1007/3-540-52885-7_105

L. Bachmair and H. Ganzinger, Completion of first-order clauses with equality by strict superposition, CTRS, pp.162-180, 1991.
DOI : 10.1007/3-540-54317-1_89

L. Bachmair, H. Ganzinger, C. Lynch, and W. Snyder, Basic Paramodulation, Information and Computation, vol.121, issue.2, pp.172-192, 1995.
DOI : 10.1006/inco.1995.1131
URL : http://doi.org/10.1006/inco.1995.1131

D. Basin and H. Ganzinger, Automated complexity analysis based on ordered resolution, Journal of the ACM, vol.48, issue.1, pp.70-109, 2001.
DOI : 10.1145/363647.363681

F. Bronsard and U. S. Reddy, Conditional rewriting in focus, Proceedings of the Second International Workshop on Conditional and Typed Rewriting Systems, 1991.
DOI : 10.1007/3-540-54317-1_77

N. Dershowitz and R. Treinen, Rta list of open problems, problem 37, 1998.

J. Hsiang and M. Rusinowitch, Proving refutational completeness of theorem-proving strategies: the transfinite semantic tree method, Journal of the ACM, vol.38, issue.3, pp.559-587, 1991.
DOI : 10.1145/116825.116833

G. Huet, Constrained Resolution: A Complete Method for Higher Order Logic, 1972.

C. Lynch, Schematic Saturation for Decision and Unification Problems, Lecture Notes in Computer Science, vol.2741, pp.427-441, 2003.
DOI : 10.1007/978-3-540-45085-6_37

A. David and . Mcallester, Automatic recognition of tractability in inference relations, J. ACM, vol.40, issue.2, pp.284-303, 1993.

R. Nieuwenhuis and F. Orejas, Clausal rewriting, CTRS, pp.246-258, 1990.
DOI : 10.1007/3-540-54317-1_95

R. Nieuwenhuis and A. Rubio, AC-superposition with constraints: No AC-unifiers needed, CADE, pp.545-559, 1994.
DOI : 10.1007/3-540-58156-1_40

L. Vigneron, Associative-commutative deduction with constraints, Lecture Notes in Computer Science, vol.814, pp.530-544, 1994.
DOI : 10.1007/3-540-58156-1_39