後件部に選言を含む論理式を Non Horn 論理式という。 Non Horn 論理式は、一階述語論理を表現できるので、 Full First Order ともいわれる。 Horn 論理式は、逆に後件部に選言を含まない論理式であり、 ルール形式
において、m は高々 1 である。 上のルールを連言標準形で書くと、
となるので、Horn 論理式では、各節における正リテラルの出現は 高々 1 である。 これは当然ながら知識表現上の制約を受けるが、 Prolog では、トップダウンにおける処理効率を考慮し、 節を Horn 節に限定している。 実際、トップダウン処理系において、 節を Horn 節に限定した場合には、推論手続きの計算量を多項式オーダー 抑えることができる。