The Instant Glue prover for Glue Semantics was written by Miltiadis Kokkonidis, with the support of SSHRC SRG #410-2006-1650 to Ash Asudeh. The prover requires Prolog to run; SWI Prolog is freely available here.
The prover supports two linear logic connectives: implication (represented as '->' in the code) and multiplicative conjunction (represented as '*' in the code). An example is provided in the code.
Please refer to the licence agreement and the disclaimer in the code.
Prover: Prolog code