Work through this worksheet to help you prepare for our work on first-order logic inference via forward chaining, backward chaining, and unification.
A lot of this stuff with logic may seem hopelessly tedious. All these tiny logical steps that are so small they seem worthless, or needlessly confusing and abstract.
The goal for mathematical logic (that’s really what this topic is) is to take the everyday common-sense mathematical reasoning that you do all the time (in calc, using epsilon-delta definitions, or algorithms showing that some f is O(g), abstract algebra showing that something is an equivalence relation) and make it rigorous.
Why do this?
In the 19th century and into the earlier 20th, mathematicians started running into logical paradoxes. But since mathematics is built on logic, this could be a problem: how do we know that the logic we’re using is sound? Are our conclusions actually correct?
As a computer science student, you can think of logical paradoxes as analogous to a program that doesn’t halt, or crashes, or computes a result that may be wrong.
Consider things like the set of all sets that don’t contain themselves. If that set contains itself, it’s not in the set…and then it doesn’t contain itself, so it’s in the set…!
The mathematicians who developed this field worked out careful, precise ways to avoid paradoxes and be certain about the soundness of their conclusions. We need to do that too: when trying to prove something or work with these sentences: be very, very careful and take small steps. Be sure you can identify each equivalence or inference rule you use.
In more computer science-y terms: we want to use careful, well-defined, well-justified baby steps so that we can convert them into algorithms, and be certain that the algorithm will work.
In the spirit of upgrading our reasoning from everyday, loosey-goosey common sense logic to high-powered, proper mathematical logic, I’ve been trying to use the proper terminology, and not be too cavalier about things like “expression”, “term”, “statement”, and so on. I try to be careful about the distinction between symbols and syntax – and the actual objects to which they refer. (That’s the ontology stuff the text gets into.)
I encourage you to do the same. Using the proper terms will sharpen and guide your thinking as you learn these ideas.
In class you worked out the negation of the defining FOL sentence for “f is O(g)”. It’s not true that sqrt(n) is O(sin(n)). Use your negation and prove it. For any ‘∃’, find an actual thing (number, etc) that exists and makes it true; for any ‘∀’, show that the universally quantified sentence does hold for every instantiation of the quantified variable.
For a bit more practice, go back to Calc 1: write the ε-δ definition of continuity of f at x0. Negate it. Take a step function and see how it satisfies that negation at the discontinuity.
If you have a finite number of objects in your FOL model, a universally quantified FOL sentence is equivalent to the corresponding set of PL sentences via universal instantiation. But it seems to me that for an existential quantification, the corresponding PL sentence with a Skolem constant via existential instantiation doesn’t quite say the same thing. Why? Work with this statement: there exists an integer between 20 and 30 that is prime.
Introduce a new constant and write a PL sentence expressing the above sentence. (It’ll be a conjunct of three things.) To what object in your model does your constant refer? (In more prosaic terms: what does N equal?)
The kicker of course is that there are two primes between 20 and 30. Write a PL sentence that is consistent with the existentially quantified FOL sentence, but which is independent of your first PL sentence.
Get some practice with the ideas behind these inference algorithms.
Here’s a KB:
You would like to know if Q is true or false.
Start from those axioms. Go through them and use modus ponens to add some theorems to your KB.
Now go through your KB again. Look at the antecedents of your implications. For those that are true, use modus ponens to infer some new theorems.
Keep going! A culinary metaphor for the above modus ponens strategy: think of the LHS of an implication as a recipe, and the pieces the ingredients. When you have all the ingredients, you can prepare the RHS and put it on the table.
Can you infer Q?1
Okay, now let’s do the same thing but in a different way.
You want to infer Q. Look through your initial KB. You’ll be building a “need-to-prove” tree. Start with Q as its root. Where does Q appear as the consequent of an implication? For each of those, add the antecedents as children of Q.
Go through those children. For each conjunction or disjunction, add the terms as children of the node.
Keep going: every time you consider a node, look for that node as the consequent of an implication, or break it up into terms. If you get to a single symbol with no children, is it true, false, or not in the KB?
When your tree is built: what do you think this says about Q?
To finish: let’s roll (with our rolling pin?) with this culinary metaphor: think of ingredients, dishes to prepare, and so on. The first procedure is like starting with…and getting to…? The second procedure is like starting with…and getting to…?
We’ll be working through the unification algorithm next
time. It will help to remember how
ASTs work. You can just think
of the following as, say, Python expressions. For example: the AST for
Poof(w, Green(a, Foo(A)), v) is
Write the AST for each of the following.
(P ∧ Q) ∨ R ⇒ S:Knows(John, x)Knows(y, Mother(y))P(F(y), z, G(F(A)))T(G(y), F(H(A)))S(x, x, F(A))Now, label nodes in those trees:
“constant symbol”: capitalized things like A, John and so on. These symbols refer to objects in the model. For the big-O example, N would refer to, say, the integer 104. John in the kings example would refer to the actual human John who was king of England.
“predicate or function”: predicates map their arguments to true or false, according to whether the associated relation holds for those arguments: Knows, Evil, Owns. A function maps one or more objects to an object in the model. LeftLeg; Mother.
“variable”: lowercase letters are variables that are part of some quantification.
Review sections 8.2-3, roughly what we did today.
The NatNum bit isn’t just abstract math-y stuff – in
languages like Haskell, that’s literally how you do things! Check out Learn You a Haskell for Great
Good! (up-to-date).
Work through 9.1 to 9.3 and understand it as best you can. Next time we’ll be working through forward and backward chaining and unification.
Look up these topics on the web. There are tons of pages and PDFs of lecture slides out there on these topics – look some up. They may explain things a bit differently, in a way that makes more sense to you. This also gives you a little bit of a big-picture viewpoint on how what we’re studying fits into the broader AI landscape.
Be prepared to show how you did any of the above exercises. As in: be prepared to be cold-called. If you struggle with anything here: you’re in good company! It’s normal. Get help from a classmate. Get help from me. Do not just give up and presume you’ll just fly under the radar next week.
A sort of corollary to that: when you’re done here, email me and let me know how it went. Too hard? Seems irrelevant or not useful? Is there some other format or structure you would prefer? Something else that would motivate you better? I mean it: just click here and start typing what you think.
My goal with these is to help you learn and make our class meetings more productive. If there’s something better, I really want to know.
Less seriously, I’m still working on what to call this. How do you want to describe these kinds of exercises, preparation, instructions, guidance? I am offering magic internet points, actual treats, and actual credit for the engagement component of your grade.
spoiler: yes.↩︎