The following case studies are available for download:

Folder Sorting contains the verification of the sorting algorithms

Insertion sort

Bubble sort

Minimum sort

Selection sort

Tree sort

Merge sort

Quick sort

Heapsort


Folder Number Theory contains

proofs of inequations and series (Textbook Exercises)

a proof of the irrationality of the square root of 2

a proof of the Binomial Theorem and some properties of Binomial Coefficients

a verification of Eratosthenes' method for computing all primes in a given interval

a proof of Fermat's Little Theorem using the Binomial
Theorem

a proof of Fermat's Little Theorem using reduced residue systems

a proof of Euler's Theorem

a proof of Wilson's Theorem (prime modulus)

a proof of Wilson's Theorem (composite
modulus)

a verification of the RSA encryption method

a proof of the infinitude of primes using Euclid's
method

a proof of the infinitude of primes using Fermat Numbers

a proof of soundness, completeness and uniqueness of prime
factorization

a proof of the boundedness of the smallest prime factor by the square root of a
composite


Folder Propositional Logic contains soundness and completeness proofs for

a sequent calculus

an implicational calculus

unit resolution for Horn clause sets

the BoyerMoore tautology checker

the DavisPutnam procedure


Folder Matching & Unification contains proofs of soundness, completeness and mostgenerality of

a firstorder matching algorithm

a firstorder unification algorithm


Folder BoyerMoore contains 3 case studies from the BoyerMoore corpus, viz.

the verification of the BoyerMoore Fast String Search algorithm

the verification of the BoyerMoore tautology checker

the proof of the unsolvability of the Halting Problem


Folder
VFR 1601 Proofs contains 3 case studies from the paper Fermat, Euler, Wilson  Three Case Studies in Number
Theory. The remaining case studies of the paper are collected in the folder Number Theory above.
_______________________________
Last update 20161026