Arend Theorem Prover

Not logged in

Arend is a theorem prover designed for use in undergraduate computer science education. It is intended to offer a gentle introduction to computer-assisted proofs, while still supporting the kind of mathematical reasoning typically required in elementary computer science.

Specification language

Arend's specification language is based on first-order hereditary Harrop formulae, an extension to Horn clauses which support rightward implication and explicit universal quantification. (Note, however, that in the initial version, only predicates that do not rely on these features can be reasoned about. Rightward implication introduces contexts at the reasoning level, which complicate proofs.)

Arend's specification language is intended to be primarily used by instructors, in building specifications.

Reasoning

Arend's reasoning interface takes a different approach from most proof assistants, as it tries to be more interactive and less programming-oriented. It emphasizes non-linear proof construction rather than "writing" a proof. It is web-based, and allows free movement between cases in a proof, lemmas, proofs, etc. The current proof state, and all previous proof states (as well as witnesses to transitions between them) are always readily available, along with contextual hints about the axioms of the system. (The full specification is, of course, always available.)

Implementation

Arend currently consists of two hopefully-converging implementations: a purely browser-based version written in Javascript, and a client-server (but still web-based) version written largely in Prolog. Note, however, that both implementations support offline use.

Status

External libraries and tools

Arend makes use of the following libraries and tools: