Automation of First- and Higher-Order Logic
Introduction to the theory and practice of automatic theorem proving, covering automation of classical propositional logic, first and higher-order logic, with emphasis on proof calculi and their implementation using functional and agent-oriented programming languages.