Computer Science | Introduction to Applied Logic
B510 | 16752 | Leivant

(3 cr.) P: B501. Structures: relations between structures, term
structures. Description: notation and meaning, substitution
operations, first order formulas, database languages, program
verification conditions, semantics valuation, normal forms,
quantifier reduction, axiomatic theories. Proof: resolution,
sequential calculi, natural deduction, automated theorem proving,
semantic completeness. Limits of formalization: compactness,
undecidability of truth, undecidability of canonical theories, non-
formalizability of database theory. B510 corresponds to old C615.