Fx7Explanation

Fx7 is an automated theorem prover implemented in the Nemerle programming language (MoskalL06) by Michal Moskal, a visiting MOBIUS PhD student in 2007. Fx7 supports the same set of theories as Simplify and Z3, as well as a similar set of concrete syntaxes as Z3.

As Nemerle is implemented in Microsoft's .NET platform, the Mono runtime must be installed on non-Microsoft Windows Mobius PVE host operating systems. Currently the Fx7 prover is a hand-installed extension to the Mobius PVE. It will be included in a future release of the Mobius PVE, complete with a pre-packaged runtime for user convenience.

Fx7 has been "bridged" into the MOBIUS Automated Prover API in a fashion akin to the other provers discussed in this section. Piped datastreams are used to communicate with the prover, and starting and stopping the prover and controlling its resources use is provided via the API.

In addition, because Fx7 is exclusively developed by MOBIUS-supported researchers, including contributors from UCD, various experiments in automated proving and verification are easy to carry out. In particular, Fx7 generates proofs of valid formulae and includes two proof checkers which run on embedded devices like PDAs (GrigoreM07). These capabilities represent the first concrete experiences with proof generation and checking the Mobius PVE, albeit for extended static checking with ESCJava2 rather than full functional verification.

Version: 1 Time: Fri Mar 28 13:26:27 2008 Author: dcochran (dcochran) IP: 193.1.132.32