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.