Issue No.04 - April (1976 vol.25)
E. Sandewall , Linkoeping University
The problem of converting axioms in predicate calculus to deterministic programs, which are to be used as "rules" by a general problem solver (GPS)-type supervisor is considered. It is shown that this can be done, but that the "objects" must then contain procedure closures or "FUNARG-expressions" which are later applied.
Closure, deduction, FUNARG-expression, nondeterministic, retrieval, theorem proving.
E. Sandewall, "Conversion of Predicate-Calculus Axioms to Corresponding Deterministic Programs", IEEE Transactions on Computers, vol.25, no. 4, pp. 342-346, April 1976, doi:10.1109/TC.1976.1674615