Logic Resources: Unification

Enter a pair of atomic formulas into the text-boxes below, and click `Unify' to begin. Click each equation to apply the corresponding transformation. Any term (except predicate/function applications) starting with a capital is considered to be a variable, anything else is a constant.
I haven't thoroughly tested the parser, so it may well behave... erratically. Particularly if you start putting whitespace in odd places. I'll fix it up eventually. In the meantime, let me know if anything goes catastrophically awry.

Propositional Logic
  • Resolution

Predicate Logic