Journal of the ACM Bibliography
Jean Gallier, Paliath Narendran, Stan Raatz, and Wayne Snyder. Theorem proving
using equational matings and rigid E-unification.
Journal of the ACM, 39(2):377-429, April 1992.
[BibTeX entry]
Selected papers that cite this one
- Bernhard Beckert. Semantic tableaux with
equality. Journal of Logic and Computation, 7(1):39-58,
February 1997.
- Anatoli Degtyarev, Yuri Matiyasevich, and Andrei Voronkov. Simultaneous
E-unification and related algorithmic problems. In
Proceedings, 11th Annual IEEE Symposium on Logic in Computer
Science, pages 494-502, New Brunswick, New Jersey, 27-30 July
1996. IEEE Computer Society Press.
- Anatoli Degtyarev and Andrei Voronkov. The undecidability of
simultaneous rigid E-unification. Theoretical
Computer Science, 166(1-2):291-300, 20 October 1996. Note.
- Anatoli Degtyarev and Andrei Voronkov. Decidability problems
for the prenex fragment of intuitionistic logic. In
Proceedings, 11th Annual IEEE Symposium on Logic in Computer
Science, pages 503-512, New Brunswick, New Jersey, 27-30 July
1996. IEEE Computer Society Press.
- Jean Gallier, Paliath Narendran, David Plaisted, Stan Raatz, and Wayne
Snyder. An algorithm
for finding canonical sets of ground rewrite rules in polynomial
time. Journal of the ACM, 40(1):1-16, January 1993.
- Jean Goubault. Rigid
E-unifiability is DEXPTIME-complete. In
Proceedings, Ninth Annual IEEE Symposium on Logic in Computer
Science, pages 498-506, Paris, France, 4-7 July 1994. IEEE
Computer Society Press.
- David A. Plaisted and Andrea Sattler-Klein. Proof lengths for equational
completion. Information and Computation,
125(2):154-170, 15 March 1996.
Selected references
- Leo Bachmair, Nachum Dershowitz, and Jieh Hsiang. Orderings for equational
proofs. In Proceedings, Symposium on Logic in Computer
Science, pages 346-357, Cambridge, Massachusetts, 16-18 June
1986. IEEE Computer Society.
- Wolfgang Bibel. On matrices
with connections. Journal of the ACM, 28(4):633-645,
October 1981.
- Peter J. Downey, Ravi Sethi, and Robert Endre Tarjan. Variations on the common
subexpression problem. Journal of the ACM,
27(4):758-771, October 1980.
- Jean Gallier, Paliath Narendran, David Plaisted, Stan Raatz, and Wayne
Snyder. An algorithm
for finding canonical sets of ground rewrite rules in polynomial
time. Journal of the ACM, 40(1):1-16, January 1993.
- Jean Gallier, Paliath Narendran, David Plaisted, and Wayne Snyder. Rigid
E-unification: NP-completeness and applications to equational
matings. Information and Computation, 87(1/2):129-195,
July/August 1990.
- Jean H. Gallier, Stan Raatz, and Wayne Snyder. Theorem proving using
rigid E-unification equational matings. In
Proceedings, Symposium on Logic in Computer Science, pages
338-346, Ithaca, New York, 22-25 June 1987. The Computer Society of the
IEEE.
- J. Gallier, W. Snyder, P. Narendran, and D. Plaisted. Rigid
E-unification is NP-complete. In Proceedings, Third
Annual Symposium on Logic in Computer Science, pages 218-227,
Edinburgh, Scotland, 5-8 July 1988. IEEE Computer Society.
- Gérard Huet. Confluent reductions: Abstract
properties and application to term rewriting systems. Journal
of the ACM, 27(4):797-821, October 1980.
- Greg Nelson and Derek C. Oppen. Fast decision procedures based on
congruence closure. Journal of the ACM, 27(2):356-364,
April 1980.
Shortcuts: