UNC-CH/ CS/ Mechanized Inference

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:

o People
o Periphery
o Provers

Book Ad

o Publications
o Present CADE by-laws

plaisted@cs.unc.edu, 17-Apr-01
If you have a link to this page...