Pocklington's Criterion

Some links and files related to the Pocklington's Criterion case study I did together with Olga Caprotti. The case study consists of a development of some theory needed to prove the criterion in the theorem prover Coq, and a Java program that generates primality Coq proofs based on communication with a Computer Algebra System. The generated proofs make use of Pocklington's Criterion. The Computer Algebra system we used is GAP.

Online Demo

PockApplet

An Applet that produces Coq tactic scripts for primality proofs. Of course you need to download the Coq files below in order to interpret the generated tactics.

Download

	coqpock.tar.gz	Coq input files. Development of Pocklington's Criterion in Coq. Includes a Makefile. Compatible with Coq V7.1 (check the Coq contributions archive for a version compatible with more recent Coq versions).
	pock.jar	Java class files. This contains the Pocklington Client Application and Applet, the GAP Command Line Server Wrapper, Netscape Privilege Manager stuff.
	pock-src.tar.gz	Java sources. The source files of the above Java classes.
	API Docs	JavaDoc API Documentation of the above Java classes.
	pock.gap	Extended Euclid's algorithm for GAP.

Links

	Olga's page	Check out Olga Caprotti's page on Pocklington's Criterion. Contains publications and related work.
	Coq Home	The Coq Home Page.
	Up	Up to Martijn's home page.