Files of check-in [9e954b6b56] in the top-level directory
% % 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.
If you only want to use the web-based version of Arend, there is no installation.
Just copy the
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
If you want to run Arend via Node, or you want to develop Arend, you should install it via
This will download Arend's dependencies (mostly development tools).