ALF is based on Horn clause logic with equality which

consists of predicates and Horn clauses for logicprogramming, and functions and equations for functionalprogramming. Any functional expression can be used in a

goal literal and arbitrary predicates can occur in

conditions of equations. ALF uses narrowing and

rewriting.