• Part 2: First-order logic

• Redundancy

• Simplification and deletion rules
• Redundancy of clauses
• Examples (tautologies, subsumption, ...)
• Saturation up to redundancy

• The structure of a resolution prover

• Hyperresolution

• Example: The Neuman-Stubblebine Security Protocoly

Imprint | Data Protection