The previous posts on propositional calculus (or zeroth-order logic) and predicate calculus (first-order logic), build on the final and practical application of these logical systems in artificial intelligence automated reasoning systems. Through logical inference and unification we will take a real world example for a financial advisor decision making system.
We come to the full possession of our power of drawing inferences, the last of our facilities; for it is not so much a natural fight as a long and difficult art.
C. S. Pierce
Logical Inference
Logical inference is a formal theory that infers new correct expressions from a set of true assertions. These new assertions will be consistent with all previous statements and interpretations. Inference rules provide the computational mechanism which we can use the concept that a conclusion “logically follows” from a premise.
A basic example is modus ponens. The inference rule for modus ponens is
If P and P → Q are true, then modus ponens infers Q is also true.More inference rules like modus tollens, examples can be found at the Wikipedia page here.
Unification
In order to apply these rules of inference we will need to be able to determine when two expressions match. This is trivial in propositional calculus, but the presence of variables in predicate calculus makes it more complicated. Unification is the algorithm that determines what substitutions we can make to predicate calculus expressions in order to make them match.
First we check the initial predicate symbol, then the number of arguments the predicate has, and then the actual arguments for a match. These arguments are either variables or constants, for example,
love(X, Y) and love(eleanor, chidi)
We can list substitutions and unify as {X/eleanor, Y/chidi}.When unifying we have three rules:
- a variable can by unified with an atom, variable or term
- two atoms can by unified if they are identical
- a term can be unified if the identifiers are the same
Here are some more examples:
p(X,Y) and p(a,Z)
'X' is a variable, and 'a' is an atom.
'X' and 'Z' are variables.
Therefore it unifies with {X/a, Z/Y}.p(X,X) and p(a,b)
'X' is a variable, but it cannot be substituted by both 'a' and 'b' atoms, therefore it does not unify.ancestor(X,Y) and ancestor(bill,father(bill))
'ancestor' and 'ancestor' unify and return the empty set {}
'X' and 'bill' unify as {bill/X}
'Y' and father(bill) unifies as {father(bill)/Y}
Therefore it unifies to {bill/X,father(bill)/Y}ancestor(X,father(X)) and ancestor(david,george)
Assuming that george is the father of david:
'ancestor' and 'ancestor' unify and return the empty set {}
'X' and 'david' unify as {david/X}
father(X) and 'george' unify as {george/father(X)}
Therefore it unifies to {david/X,george/father(X)}A logic-based financial advisor
This example is part of the exercises found in Lugers text[efn_note](Luger, George F.; Stubblefield, William A, Artificial intelligence: structures and strategies for complex problem solving 1998)[/efn_note].
We are going to build a financial advisor that decides how someone should split their money between investments and savings. Specifically, the advisor should recommend the amount according the the following criteria.
- Inadequate savings accounts should always make increasing their savings the top priority regardless of their income.
- Adequate savings and adequate income should consider riskier investments in the stock market.
- Lower income with an adequate savings may consider splitting their surplus in investments and savings.
From this we can create the first three predicates for our logical system:
1. savings_account(inadequate) → investment(savings)
2. savings_account(adequate)⋀income(adequate) → investment(stocks)
3. savings_account(adequate)⋀income(inadequate) → investment(combination)We now need to determine when savings and income are considered adequate. To do this we create the function minsavings which takes one argument, the number of dependents, and returns 5000 times that argument. minsavings(X) ≡ 5000 * X. Now we have two more predicates for our logical system.
4. ∀ X amount_saved(X) ⋀ ∃ Y (dependents(Y) ⋀ greater(X, minsavings(Y))) → savings_account(adequate)
5. ∀ X amount_saved(X) ⋀ ∃ Y (dependents(Y) ⋀ ¬ greater(X, minsavings(Y))) → savings_account(inadequate)Similiarily we need a minincome function. We will define this function as minincome(X) ≡ 15000 + (4000 * X). To define an investors income as adequate it must be above this minimum income and also steady. This adds three more predicates to our logical system.
6. ∀ X earnings(X, steady) ⋀ ∃ Y (dependents(Y) ⋀ greater(X, minincome(Y))) → income(adequate)
7. ∀ X earnings(X, steady) ⋀ ∃ Y (dependents(Y) ⋀ ¬ greater(X, minincome(Y))) → income(inadequate)
8. ∀ X earnings(X, unsteady) → income(inadequate)For our example, Jane Doe has four dependents, a steady income of $30,000 and $15,000 in her savings account. This adds our final three predicate calculus sentences.
9. amount_savings(15000)
10. earnings(30000,steady)
11. dependents(4)Now for the fun part! Let’s unify! First we can unify conjunction of 10 and 11 with the first two components of 7.
earnings(30000, steady) ⋀ dependents(4) unifies with:
earnings(X, steady) ⋀ dependents(Y) under substitution {30000/X, 4/Y} yielding:
earnings(30000, steady) ⋀ dependents(4) ¬ greater(30000, minincome(4)) → income(inadequate)
earnings(30000, steady) ⋀ dependents(4) ¬ greater(30000, 31000) → income(inadequate)All 3 components of the premise are true, therefore by 10, 3, and the mathematical definition of greater their conjunction is true and the entire premise is true. Thus, we can add another premise
12. income(inadequate)amount_saved(15000) ⋀ dependents(4) unifies with the first two elements of assertion 5 under the substitution {15000/X, 4/Y} yielding:
amount_saved(15000) ⋀ dependents(4) ⋀ ¬ greater(15000, minsavings(4)) → savings_account(inadequate)
amount_saved(15000) ⋀ dependents(4) ⋀ ¬ greater(15000, 20000) → savings_account(inadequate)Given that all 3 components of the premise are true, we have another premise
13. savings(inadequate)As a consequence of expressions 13 and 1 and modus pollens,
savings(inadequate) → investment(savings)Our automated logical reasoning system suggests that Jane Doe’s surplus income goes into her savings account. This example shows how we can automatically reason and draw conclusions by applying these inference rules in a programmatic fashion.