% This propositional logic problem that was the
% "most difficult" (!) theorem proved by the "new"
% Logic Theorist of 1972.
% 
% Selmer Bringsjord (born 1958)
% Intro to Logic Programming and AI, Spring 1998

% Interesting twist:  OTTER returns immediate verification
% that --p <-> p is indeed a theorem of the propositional
% calculus, and that verification isn't enlightening from
% the standpoint of a human desiring to produce a "natural"
% proof.  What happens if we convert the theorem in question
% to first-order logic, and attempt to prove it from some
% axiomatization of the propositional calculus?  The
% conversion to propositional form for the theorem here is
% shown below in a comment statement.

set(auto).
set(propositional).

formula_list(usable).

-(-(-p) <-> p).
% all x (Ti(n(n(x)),x)).

end_of_list.