# Pitt CS 1571 - Inference in first order logic (18 pages)

Previewing pages 1, 2, 3, 4, 5, 6 of 18 page document
View Full Document

# Inference in first order logic

Previewing pages 1, 2, 3, 4, 5, 6 of actual document.

View Full Document
View Full Document

## Inference in first order logic

25 views

Lecture Notes

Pages:
18
School:
University of Pittsburgh
Course:
Cs 1571 - Intro to Artificl Intelligence
##### Intro to Artificl Intelligence Documents
• 13 pages

• 16 pages

• 22 pages

• 21 pages

• 22 pages

• 20 pages

• 16 pages

• 12 pages

• 12 pages

• 19 pages

• 25 pages

Unformatted text preview:

CS 1571 Introduction to AI Lecture 19 Inference in first order logic Milos Hauskrecht milos cs pitt edu 5329 Sennott Square CS 1571 Intro to AI M Hauskrecht Logical inference in FOL Logical inference problem Given a knowledge base KB a set of sentences and a sentence does the KB semantically entail KB In other words In all interpretations in which sentences in the KB are true is also true Logical inference problem in the first order logic is undecidable No procedure that can decide the entailment for all possible input sentences in a finite number of steps CS 1571 Intro to AI M Hauskrecht 1 Logical inference problem in the Propositional logic Computational procedures that answer KB Three approaches Truth table approach Inference rules Conversion to the inverse SAT problem Resolution refutation CS 1571 Intro to AI M Hauskrecht Inference rules Inference rules from the propositional logic Modus ponens A B B Resolution A A B B C A C and others And introduction And elimination Orintroduction Negation elimination Additional inference rules are needed for sentences with quantifiers and variables Must involve variable substitutions CS 1571 Intro to AI M Hauskrecht 2 Variable substitutions Variables in the sentences can be substituted with terms terms constants variables functions Substitution Is represented by a mapping from variables to terms x1 t1 x 2 t 2 K Application of the substitution to sentences SUBST x Sam y Pam Likes x y Likes Sam Pam SUBST x z y fatherof John Likes x y Likes z fatherof John CS 1571 Intro to AI M Hauskrecht Inference rules for quantifiers Universal elimination x x a a is a constant symbol substitutes a variable with a constant symbol x Likes x IceCream Likes Ben IceCream Existential elimination x x a Substitutes a variable with a constant symbol that does not appear elsewhere in the KB x Kill x Victim Kill Murderer Victim CS 1571 Intro to AI M Hauskrecht 3 Inference rules for quantifiers Universal instantiation introduction x x is not free in

View Full Document

Unlocking...