Fall 2004
Department of Computing Science
University of Alberta
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.