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

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

Inference in first order logic



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

View the full content.
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

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

Access the best Study Guides, Lecture Notes and Practice Exams

Loading Unlocking...
Login

Join to view Inference in first order logic and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Inference in first order logic and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?