software system consisting of a programming language, an extensible theory in a first-order logic, and an automated theorem prover
