The Mechanized Inference group at the University of North Carolina has
been developing theorem provers under the guidance of Dr. David Plaisted.
While the mainstream theorem proving community has been re-hashing
Robinson's resolution rule for the past thirty years, we have been
studying fundamentally different approaches, some of which are competitive
even when programmed in Prolog, which is comparatively slow.
Table of contents:
Present CADE by-laws
If you have a link to this page...