Bibliography

Bachmair, L. & Ganzinger, H. (1994 a),

Ordered chaining for total orderings, in `Proc. 12$th$ International Conference on Automated Deduction', Vol. 814 of Lecture Notes in Artificial Intelligence, Springer-Verlag, Berlin, pp. 435-450.

Bachmair, L. & Ganzinger, H. (1994 b),

`Rewrite-based equational theorem proving with selection and simplification', J. Logic and Computation 4(3), 217-247.
Revised version of Technical Report MPI-I-91-208, 1991.

Bachmair, L. & Ganzinger, H. (1994 c),

Rewrite techniques for transitive relations, in `Proc. 9th IEEE Symposium on Logic in Computer Science', IEEE Computer Society Press, pp. 384-393.
URL: //people.mpi-inf.mpg.de/alumni/ag2/2011/hg/pca.html#LICS94

Bachmair, L. & Ganzinger, H. (1995 a),

Associative-commutative superposition, in N. Dershowitz & N. Lindenstrauss, eds, `Proc. 4th Int'l Workshop on Conditional and Typed Rewrite Systems, Jerusalem', Vol. 968 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, pp. 1-14.
Revised version of MPI-I-93-267, 1993.

Bachmair, L. & Ganzinger, H. (1995 b),

Ordered chaining calculi for first-order theories of binary relations, Research Report MPI-I-95-2-009, Max-Planck-Institut für Informatik, Saarbrücken, Saarbrücken.
Revised version to appear in JACM.
URL: //people.mpi-inf.mpg.de/alumni/ag2/2011/hg/pra.html#MPI-I-95-2-009

Basin, D. & Ganzinger, H. (1995),

Automated complexity analysis based on ordered resolution, Research Report MPI-I-95-2-006, Max-Planck-Institut für Informatik, Saarbrücken, Saarbrücken.
Full version of LICS'96 paper.
URL: //people.mpi-inf.mpg.de/alumni/ag2/2011/hg/pra.html#MPI-I-95-2-006

Basin, D. & Ganzinger, H. (1996),

Complexity analysis based on ordered resolution, in `Proc. 11th IEEE Symposium on Logic in Computer Science', IEEE Computer Society Press, pp. 456-465.
URL: //people.mpi-inf.mpg.de/alumni/ag2/2011/hg/pca.html#LICS96

Nieuwenhuis, R. & Rubio, A. (1992 a),

Basic superposition is complete, in `ESOP'92', Vol. 582 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, pp. 371-389.

Nieuwenhuis, R. & Rubio, A. (1992 b),

Theorem proving with ordering constrained clauses, in `Automated Deduction -- CADE'11', Vol. 607 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, pp. 477-491.

Imprint | Data Protection