• Part 2: First-order logic

  • 2.5 Normal forms, Skolemization

  • 2.6 Herbrand models
    • Herbrand interpretations as sets of ground atoms
    • Existence of Herbrand models

  • 2.7 Inference systems, Proofs
    • Inference systems, proof. provability relation
    • Soundness, completeness, refutational completeless of an inference system
    • Proofs as trees

  • 2.8 Propositional resolution
    • The resolution calculus (Res)
    • Resolution with implicit factorization (RIF)
    • Soundness of resolution


    Imprint | Data Protection