Spring 2003
School of Computer Science
University of Waterloo
Instructors: | Relu Patrascu | DC2127, x3299 | rpatrasc@cs.uwaterloo.ca |
Dale Schuurmans | DC1310, x3005 | dale@cs.uwaterloo.ca |
Correct & exhaustive first order reasoning:
First order semantics:
interpretation I=(D,C,F,R).
D = domain, C maps constants, F maps function symbols,
R maps predicates.
Evaluating ground sentences without variables and quantifiers.
Variable assignment V maps variables.
Evaluating formulae with variables and quantifiers.
Interpretation satisfies, falsifies a sentence.
Sentence meaning: restriction on satisfying interpretations
(possible states of affairs).
Sentence satisfiable, falsifiable, unsatisfiable (inconsistent),
unfalsifiable (valid).
Sentence semantically entails another sentence.
Correctness (soundness) of resolution+factoring w.r.t.
interpretations.
Exhaustiveness (completeness) of resolution+factoring w.r.t.
interpretations.