A mechanical proof of Segall's PIF algorithm
In August, 1996, I concluded the construction of a mechanical proof
of Segall's PIF algorithm. It mainly serves as an example of the
techniques developed for the
mechanical proof
of the algorithm of Gallager, Humblet and Spira .
Both proofs use the theorem prover NQTHM-1992 of Boyer and
Moore, which can be obtained from
nqthm-request@cli.com, Computational Logic, Inc.,
1717 West Sixth Street, Suite 290,
Austin, Texas 78703, USA.
The PIF algorithm and its proof are described in
The event file that can be read and submitted to NQTHM-1992 for
verification is
Comments are welcome, June 26, 1998.