First Order Logic
May 11, 2021 § Leave a comment
First Order Logic (FOL) is a flexible, well-understood, and computationally tractable approach to the representation of knowledge that satisfies many of the desiderata for a meaning representation language.
In addition, an attractive feature of FOL is that it makes very few specific commitments as to how things ought to be represented.
Basic elements of First Order Logic
We will explore FOL in a bottom-up fashion by first examining its various atomic elements and then showing how they can be composed to create larger meaning representation.
Constants in FOL refer to specific objects in the world being described. Like programming language constants, FOL constants refer exactly one object. Objects can, how ever, have multiple constants that refer to them.
Functions in FOL corresponds to concepts that are often expressed in English as genitives.
Function provide a convenient way to refer to specific objects without having to associate a named constant with them. This is particularly convenient in cases in which many named objects, like restaurants, have a unique concept such as a location associated with them.
The notion of a variable is our final FOL mechanism for referring to objects. Variables, which are normally depicted as sigle lower case letters, let us make assertions and draw inferences about objects without having to make reference to any particular named object.
Predicates are symbols that refer to, or name, the relations tha hold among some fixed number of objects in a given domain.
A one-place predicate that is used, not to relate multiple objects, but rather to assert a property of a single object. In this case, it encodes the category membership Maharani.
Larger composite representations can also be put together through the use of logical connectives.
Variables and Quantifiers
Variable are used in two ways in FOL: to refer to a particular anonymous objects and to refer generically to al objects in a collection. These two uses are made possible through the use of operators known as quantifiers.
To review, variables in logical formulas must be either existentially or universally quantified. To satisfy an existentially quantified variable, at least one substitution must result in a true sentence. Sentences with universally quantified variables must be true under all possible substitutions.
The final element we need to complete our discussion of FOL is called lambda notation. This notation provides a way to abstract from fully specified FOL formula in a way that will be particularly useful for semantic analysis.
Such expressions consist of the greek letter lambda, followed by one or more variables, followed by a FOL formula that makes use of those variables.
This process is known as lambda-reduction and consist of a simple textual replacement of the lambda variables with the specified FOL items, accompanied by the subsequent removal of the lambda.
This general technique, called currying, is a way of converting a predicate with multiple arguments into a sequence of single argument predicates. The lambda notation provides a way to incrementally gather arguments to a predicate when they do not all appear together as daughters of the predicate in a parse tree.
The Semantics of First Order Logic
The model theoretic approach: this approach employs simple set-theoretic notions to provide a truth conditional mapping from the expressions in a meaning representation to the state of affairs being modeled.
We can start by asserting that the objects in our world, FOL terms, denote elements in a domain, and asserting that atomic formulas are captured either as sets of domain elements for properties, or as sets of tuples of elements for relations.
There are no variables in our set based models, only elements of the domain and relations that hold among them. We can provide model based account for formulas with variables by employing the notion of a substitution introduced earlier in this page. Formulas involving the existential quantifier are true if a substitution of terms for variables results in a formula that is true in the model. Formulas involving the universal quantifier must be true under all possible substitutions.
One of the most important desiderata given for meaning representation language is that it should support inference, or deduction. That is, the ability to add valid new proposition to a knowledge base or to determine the truth of propositions not explicitly contained within a knowledge base. This section briefly discusses modus-ponens, the most widely implemented inference method provided by FOL.
Modus-ponens is a familiar form of inference that corresponds to what is informally known as if-then reasoning. We can abstractly define modus ponens as follows, where alpha and beta should be taken as FOL formulas.
Modus-ponens simply states that if the left-hand side of an implication rule is true, then the right-hand side of the rule can be inferred. In the following discussions, we will refer to the left-hand side of an implication as the antecedent and the right-hand side as the consequent.
Modus-ponens can be put to practical use in one of two ways: forward chaining and backward chaining. In forward chaining systems, as individual facts are added to the knowledge base, modus ponens is used to fire all the applicable implications rules.
The forward chaining approach has the advantage that facts will be present in the knowledge base when needed, because, in a sense all inference is performed in advance. This can substantially reduce the time needed to answer subsequent queries since they should all amount to simple lookups. The disadvantage of this approach is that facts that will never be needed may be inferred and stored.
Production systems which are used extensively in cognitive modeling research are forward chaining inference systems augmented with additional control knowledge taht governs which rules are to be fired.
In backward chaining modus ponens is run in reverse to prove specific propositions called queries. The first step is to see if the query formula is true by determining if ot os present in the knowledge base. If it is not, then the next step is to search for applicable implication rules present in the knowledge base. An applicable rule is one whereby the consequent of the rule matches the query formula. The Prolog programming language is a backward chaining system that implements this strategy.
Note that it is critical to distinguish between reasoning by backward chaining from queries to known facts and reasoning backwards from known consequents to unknown antecedents. To be specific, by reasoning backwards we mean that if the consequent of a rule is known to be true, we assume that the antecedent will be as well.
While backward chaining is a sound method of reasoning, reasoning backwards is an invalid, though frequently useful, form of plausible reasoning. Plausible reasoning from consequents to antecedents is known as abduction, and is often useful in accounting for many of the inferences people make while analyzing extended discourses.
While forward and backward reasoning are sound, neither is complete. This means that there are valid inferences that cannot be found by systems using these methods alone. Fortunately, there is an alternative inference technique called resolution that is sound and complete.