% % Arend % Educational Proof Assistant % Andy Clifton %

Arend is a proof assistant designed for use in undergraduate computer science education. It is based on a fragment of first-order intuitionistic propositional logic (and hence is named after Arend Heyting) similar to that underlying Lambda Prolog, and has a web-based user interface for interactively constructing and exploring proofs.

Installation

If you only want to use the web-based version of Arend, there is no installation. Just copy the src, res and lib directories to somewhere under your www root and add some pages that use them. Arend includes all the dependencies it needs for web-based usage in the lib directory

If you want to run Arend via Node, or you want to develop Arend, you should install it via

npm install

This will download Arend's dependencies (mostly development tools).