A Collection of Theorem Provers for Temporal Logics.
The applications can also be used via online web apps without having to download or compile anyting. This git repository contains:
- unify [cgibin preview] A unified UI around various CTL* and BCTL* theorem provers, and an NL-BCTL* based rewrite system.
- mechecker [cgibin preview] A Model Checker for General Linear Time
- batl [js preview] A simple OCaml Tableau for BATL* (and NL-BATL*)
- bctl [js preview] A simple OCaml Tableau for BCTL* (and NL-BCTL*)
The unified UI uses (4) above, and can also use:
- CTLStarTab: Various Java based Tableaux for CTL*, BCTL* and NL-BCTL*. These are the tableaux we gave uppercase names: CTL, BCTLOLD, BCTLNEW, BCTLHUE, BPATHUE and BPATH
- mlsolver: Hybrid Tableau for CTL* that requires a pgsolver
To fetch all dependances and compile on Ubuntu just enter ./build.sh. This was last tested on Ubuntu 14.04.