intent to package pclu (clu compiler), lp (theorem prover)
pclu is a "portable ,clu compiler`". clu is an obscure,
experimental language that lp happens to be written in.
The unfortunately-named `lp' is the Larch Prover, an "interactive
proof assistant for multisorted first-order logic. It can be used to
axiomatize theories and to provide assistance in proving theorems."
(I say "unfortunately-named" because on some Unix systems, though not
Debian, lp is the print command (~= lpr). Any suggestions as to what
to call the package and/or binary? `lp' would be the default name in
each case, as this is what the upstream version is called.)
I dreamily hope that it (or some other theorem prover) may be useful
for Mercury programs. It shouldn't be too difficult to write a
Mercury-to-lp translator; the difficult bit seems to be telling lp how
to prove all the useful properties of predicates once you have the
predicates in lp notation, even if you could write proofs on paper.
pclu is under a BSD-like license.
The licensing terms for lp are unfortunately not stated anywhere in
the distribution. The licensing terms of lclint (which is another
program from the Larch project) are non-DFSG, though very close:
essentially, one must request permission before distributing modified
versions of lclint.
I have already packaged these things (except for some small but
important details like finding out the licensing terms), but am not
yet registered as a Debian developer. (I will wait until next linux
user group meeting and try to get a debian developer to sign my PGP
key. Any LUVers reading this?)
pjm.
Reply to: