ALF was designed to be genuine integration of both programming paradigms, and thus any functional expression can be used in a goal literal and arbitrary predicates can occur in conditions of equations.
ALF's operational semantics is based on the resolution rule to solve literals and narrowing to evaluate functional expressions.
[citation needed] Terms are simplified by rewriting before a narrowing step is applied and equations are rejected if the two sides have different constructors at the top.
Rewriting and rejection are supposed to result in a large reduction of the search tree and produce an operational semantics that is more efficient than Prolog's resolution strategy.
The ALF System[4] runs on Unix and is available under a custom proprietary software license that grants the right to use for "evaluation, research and teaching purposes" but not commercial or military use.