fsp (pronounced fellowship) is a super-prover that enables the centralized development of proof libraries for other proof assistants, such as Coq and PVS. It implements first-order sequent calculus annotated by λμμ'-proof terms, a monadic proof language, and a flurry of other innovative concepts. Albeit still under developement, in its current form it is arguably quite usable.
 |
DownloadGet the latest official release of the fsp theorem prover:
You can also download the older release: fellowship-0.1.0.tar.gz. |
Unwrap
To compile and run fsp, all you need is a modern version (> 3.08) of the OCaml compiler, and the standard-issue automake tools. For increased command-line flexibility, ledit will be used if available on your system.
If you want to check the proofs with external proof assistants, you'll need to have them installed. At the moment, fsp supports:
- version 8.0 of the Coq proof assistant or higher,
- version 3.0 of the PVS Specification and Verification System or higher.
Documentation
fsp has significant support integrated in its toplevel —just typing "help." is usually a good starting point.
A frugal manual is also part of the software package under the "documentation/" directory. Comprehensive documentation and design choices discussion can be found in Florent Kirchner's Ph.D dissertation.
You can also download and view the various piece of documentation separately using the following links: