One of my earliest results was to show that any flowchart schema with a counter can be translated into an equivalent flowchart schema without any counters. This had been a major open problem attempted by many people.
I also had a number of results concerning NP complete problems. I found NP complete and NP hard problems involving number theory and integer and polynomial divisibility, where people had not expected them to be found.
I did some work in algorithms, too. With a couple of colleagues, I developed heuristic algorithms for the traveling salesman problem on the unit square. I also developed a heuristic algorithm for the maximal matching problem on graphs. Later, I developed a heuristic triangulation algorithm which I believe is still the best known. Unfortunately, this work seems largely to have been ignored by the computational geometry community. I also found a heuristic algorithm for small separators on graphs. I did some work with a colleague on graph thickness, but he eventually published a paper without listing me as a co-author.
On a sabbatical at SRI, I worked on Joe Goguen's error algebras. I showed that they are much more complex than he had thought, which influenced him to abandon them and concentrate on order-sorted algebras, instead.
In logic programming, I did some work on the occur check problem, showing how Prolog can simulate true unification efficiently. Typical Prolog implementations use a fast but unsound version of unification.
I worked with Mago's FFP group for a while, obtaining some significant results which were much appreciated by local people. Unfortunately, this project was suspended later. I also published a few papers on achitectures for functional programming and term-rewriting.
In term rewriting systems, I found the first of the recursive path orderings. This led to Dershowitz' recursive path ordering, which spawned a tremendous amount of research. With Leo Bachmair, I also developed the first associative path ordering, and this work was followed by a number of other papers by other researchers. I co-authored a paper on unfailing completion with Leo Bachmair and Nachum Dershowitz, and my main part of the work was to show that Knuth-Bendix completion relative to a given ordering would find a canonical system relative to that ordering if one existed. This is a really fundamental result in the field of completion. I also wrote a survey of term-rewriting systems, which was widely distributed and is one of the easiest for beginners to understand. However, it is not referenced as much as it might be. I also found some decidability results about termination of ground term-rewriting systems and a polynomial time constraint satisfaction system. A joint paper with Andrea Sattler-Klein about the complexity of Knuth-Bendix completion is I believe fundamental and seminal in the field.
I had the key ideas in the original proof that rigid E-unification is NP complete. This result has spurred many others since then. The simultaneous problem was later shown to be undecidable, and I also contributed some results in that area. I also found a polynomial time algorithm for completion of ground term-rewriting systems.
I had the first proof that ground reducibility is decidable; this is a key operation in inductive theorem proving using term-rewriting. There have been many papers since then improving the algorithm and the time bound.
My original paper on theorem proving with abstraction was seminal and has been followed by many other papers by other people. By now the later papers do not always acknowledge my original work, or appreciate its significance.
Our group has developed a number of instance-based theorem provers, which on some kinds of problems are much more efficient than resolution and similar methods. The work with Shie-Jue Lee on the clause linking method led Billon to develop the disconnection calculus. This in turn led to the disconnection calculus theorem prover (DCTP) which has done well in recent CADE competitions. Also, RRTP (written by M. Paramasivam) obtained the best score on non-Horn non-equality problems in a past CADE theorem prover competition. RRTP also scored third in the non-equality category, and a related prover of ours scored second in the satisfiability category. Later, Yunshan Zhu implemented OSHL, a system combining propositional efficiency, natural semantics, equality reasoning, and goal-sensitivity. This prover has been made available on the web at http://www.cs.unc.edu/~zhu/prover.html and announced in a couple of newsgroups on Sept. 24, 1997.
A joint paper with J. Avenhaus on general algorithms for permutations in equational inference has led to a number of follow-up papers by others.
It was at my prompting that the RTA conference (rewriting techniques and applications) was made democratic. I also instigated an effort to make the CADE conference democratic which, aided by a later amendment to the bylaws, was largely successful. I suggested to Deepak Kapur that the theorem proving community should respond to NSF's proposed reduction of funding. Subsequently he organized a workshop on this topic, but I don't know if my suggestion influenced him. I also initiated the organization of a workshop on first-order theorem proving. This FTP workshop has become a regular event since then.
I have done a number of investigations of the complexity of theorem proving strategies, culminating in a book with Yunshan Zhu which I believe is seminal in the field.
In addition, there have been a variety of other results.