4.15 First-order logic, and inference in it

Work through these

• Write objects, relations, functions and quantifiers in first-order syntax

  The vocabulary that lets one sentence say something about every object rather than one sentence per object. Getting the two quantifiers the right way round is the usual source of wrong statements.

• Translate English sentences into first-order logic, and check them against a small world

  Writing the sentence, then testing it on a world you invented where it should be true and one where it should be false. Nearly every mistranslation shows up in that second test.

• Unify two expressions, and find the most general unifier

  Finding the substitution that makes two expressions identical, using the least commitment that works. It is the single mechanism underneath every inference rule that follows.

• Run forward chaining from facts towards conclusions

  Starting with what is known and applying rules until nothing new appears. It suits situations where facts arrive first and you want everything they imply, which is what a monitoring system needs.

• Run backward chaining from a goal towards the facts it needs

  Starting from the question and working back to the facts that would answer it. It suits diagnosis, where you have a hypothesis in mind and want to know what would confirm it.

• Apply resolution with unification, and say why it is refutation-based

  Adding the negation of what you want to prove and deriving a contradiction. Working by refutation is what lets one rule handle a whole logic rather than a rule for each connective.