Computing, solving, proving: A report on the Theorema project

In an oversimplified and abstract view, given a logic (syntax, semantics, inference system) L and a knowledge base K of formulae in L.“computer” for K enables the user to provide an expression (term, formula, program) T with a free variable x and a value υ (from an appropriate domain) and “evaluates” T_x←υ (T with υ substituted for x) w.r.t. K in L.“solver” for K enables the user to provide an expression T with a free variable x and produces (all) values υ for which T_x←υ holds w.r.t. K in L, and“prover” for K enables the user to provide an expression T with a free variable x and generates a proof (or disproves) that, for all values υ, T_x←υ holds w.r.t. K in L.