Contains the logical abilities of the kernel. If two formulas are logically equivalent could be checked here.