We describe a novel logic, called HiLog, and show that it provides a more suitable basis for logic
programming than does traditional predicate logic. HiLog has a higher-order syntax and allows
arbitrary terms to appear in places where predicates, functions and atomic formulas occur in predicate
calculus. But its semantics is first-order and admits a sound and complete proof procedure.
Applications of HiLog are discussed, including DCG grammars, higher-order and modular logic programming,
and deductive databases.