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.
Home

Propositional Logic
  • Resolution

Predicate Logic