PropSat allows you to specify and reason about finite structures in first-order predicate logic. PropSat is a BDD-based model-builder. PropSat onLine allows you to run simple examples in your web browser.

PropSat online

This link allows you to run propsat over the web. You can edit the examples given or cut and paste your own FDDL definitions. PropSat onLine uses JavaScript with HTTPrequest and will only run on browsers that support this.


PropSat is written in StandardML, is compiled with PolyML under Linux, and uses the PolyML C interface to call David Long's C-library, BDDLIB, to do most of its work. The online web interface uses LiveConnect to link Perl, Javascript and Java.