unicode_fol_kit.is_horn

unicode_fol_kit.is_horn(node)[source]

Return True iff node’s clausal form consists of Horn clauses.

Syntactic/clausal definition: skolemise, drop the universal prefix, put the matrix into CNF, split into clauses, and check that every clause has at most one positive literal.

Parameters:

node (Node)

Return type:

bool