D A Wolfram.
January 1991.
We find that the semantics of lambda Prolog languages are based on equivalences of formal systems, and that the languages have no model-theoretic semantics. Satisfiability and validity of formulas, and soundness and completeness of interpreters are undefined. The approaches of providing a semantics by using Henkin-Andrews general models, uniform proofs, and generalizing resolution are discussed and found to be inappropriate. Two solutions are suggested: basing the semantics of the language on sets of V-complexes due to Andrews, or defining another language, called the Clausal Theory of Types, for which resolution can be generalized.