Accompanying the paper A Proof-Theoretic Approach to the Static Analysis of Logic Programs by Dale Miller is a simple λProlog implementation of the underlying static analysis algorithm (deduction in linear logic). This implementation is mean to be simplistic so that the structure of procedures remains clear. This code will compile and execute directly on the Teyjus implementation of λProlog. Below are the main source files for this implementation.
Linear logic connectives. Some predicates for basic manipulations of linear logic formulas.
Constants that are used to represent Horn clause program.
Printing routines for formulas and programs.
The multiplicative prover is now working on some tests. In order to stop the prover from cycling with symmetric assumptions (as in the case for equivalences o-o), I simply deleted a rewrite rule each time it was selected. This is a probable loss of completeness that I should check more carefully.
The harness for the two programs above. This is the main module.
A Makefile can be used to call the Teyjus compiler tjcc
The Teyjus bytecode intepreter tjsim can be called interactively of via a couple different executable scripts: mprove will apply the mcheck predicate to the argument given at the unix command line. For example,
% mprove listswill apply the multiplicative prover on the clauses and invariances in the file lists.hc. This executable also makes sure that the top-level predicates are compiled. Similarly, the aprove calls the additive prover instead.
Example Horn clause programs put into files using the .hc extension. Since I have not written a parser, we need to enter abstract syntax directly (using lambda Prolog's concrete syntax in a direct fashion). The .txt files are the result of running the mprove command on the associated .hc file.