• Part 2: First-order logic

  • 2.10 Refutational completeness of resolution

    • candidate models, properties
    • refutational completeness of propositional resolution
    • resolution for first-order clauses
      • unification
          the Martelli-Montanari algorithm for computing most general unifiers
      • the lifting lemma
      • refutational completeness of resolution

    Imprint | Data Protection