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 Proposed by-laws considered at CADE 13 [PostScript] [DVI] [LaTex]
Long speech about the bylaws issue [PostScript] [DVI] [HTML]
Speech delivered at the business meeting [PostScript] [DVI] [HTML]
Outcome of the vote [PostScript] [DVI] [HTML]
A discussion of the new bylaws
o Present CADE by-laws

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