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

Abstract

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.