Automated Theorem Proving

This text and software package introduces readers to automated theorem proving, while providing two approaches implemented as easy-to-use programs. These are semantic-tree theorem proving and resolution-refutation theorem proving.