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


B510 Introduction to Applied Logic (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.