The Resolution Calculus

Focusing on resolution theorem proving, the author presents a selective exploration of this specific area within the broader field of automated deduction. The course, delivered through five lectures, prioritizes depth over breadth, highlighting recent advancements and applications of resolution theory. Key topics include completeness, redundancy, termination, and complexity, demonstrating that while resolution is no longer the sole focus in computational logic, it remains relevant and rich with potential for new insights and developments.