[FOM] Charlie Silver on "literal"

[Martin Davis]

In his last message, Charlie has called on me to say something about 
Quine's term "literal" for the negation of an atomic formula. Hilary Putnam 
and I used this term in our influential:

  ``A Computing Procedure for Quantification Theory,'' Journal of the 
Association for Computing Machinery, vol.7(1960), pp. 201-215; reprinted 
in, Siekmann, Jörg and Graham Wrightson (eds),  Automation of Reasoning, 
vol. 1,} Springer Verlag, 1983, pp. 125-139.

 From there it passed into the automated deduction literature and there 
must be thousands of publications from that community that use it. The term 
has the virtue of brevity. I believe that any attempt to change it now is 
quixotic.

Martin