A logic with higher-order syntax. That is, it allows arbitrary terms (including variables) in places where predicate logic only allows predicates, functions, or atomic formulas.
HiLog's semantics is first-order and admits a sound and complete proof procedure. Actually it's very simple to transform to standard Prolog.
Implemented in Flora-2, partially implemented in XSB.
There seem to be many people of the opinion that HiLog is not actually useful for anything given the existence of call in standard Prolog.