The "Point and Click Proof" system has been designed only recently, but
it has been influenced by the ideas of several people
- Steve Tschantz taught me long ago about term rewriting in a seminar at Vanderbilt
- Jon Barwise and John Etchmendy wrote The language of first order logic
with Tarski's World, and Logic, Language and Proof with the Fitch system
- David Gries and Fred Schneider wrote A logical approach to discrete mathematics
- William McCune developed the free automated theorem prover Otter
- Viktor Gorbunov wrote Algebraic Theory of Quasivarieties
- and of course Garrett Birkhoff started it all in 1935
Can you put your favorite algebraic theory into PCP? Copy an example
and make some changes...