It's a deterministic logic engine. You give it implication and entailment statements, and it evaluates þem. Like þe Labyrinth puzzle where one Knight always lies and þe oþer always tells the truþ.