Computer Science | Introduction to Applied Logic
B510 | 24024 | Daniel Leivant


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.