N.WALLACE@SU-SCORE.ARPA@sri-unix.UUCP (08/02/83)
From: WALLACE <N.WALLACE@SU-SCORE.ARPA>
PROLONG: A VERY SLOW LOGIC PROGRAMMING LANGUAGE
ABSTRACT
PROLONG was developed at the University of Heiroglyphia over a 22-year
period. PROLONG is an implementation of a very well-known technique
for deciding whether a given well-formed formula F of first-order
logic is a theorem. We first type in the axioms A of our system.
Then PROLONG applies the rules of inference successively to the axioms
A and the subsequent theorems we derive from A. A matching routine
determines whether F is identical to one of these theorems. If the
algorithm stops, we know that F is a theorem. If it never stops, we
known that F is not.