Automated reasoning

Automatic reasoning, which is the attempt to prove statements with a computer, is discussed. Applications to mathematical theorem proving, diagnosis from first principles, logic circuit design and validation, and program verification and validation are described. >