Case Studies

The following case studies are available for download:

  1. Folder Sorting contains the verification of the sorting algorithms

    • Insertion sort
    • Bubble sort
    • Minimum sort
    • Selection sort
    • Tree sort
    • Merge sort
    • Quick sort
    • Heapsort
      •   
  2. 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
      •   
  3. Folder Propositional Logic contains soundness and completeness proofs for

    • a sequent calculus

    • an implicational calculus

    • unit resolution for Horn clause sets

    • the Boyer-Moore tautology checker

    • the Davis-Putnam procedure

      •  
  4. Folder Matching & Unification contains proofs of soundness, completeness and most-generality of
    • a first-order matching algorithm
    • a first-order unification algorithm
      •  
  5. Folder Boyer-Moore contains 3 case studies from the Boyer-Moore corpus, viz.
    • the verification of the Boyer-Moore Fast String Search algorithm
    • the verification of the Boyer-Moore tautology checker
    • the proof of the unsolvability of the Halting Problem
      •   
  6. Folder VFR 16-01 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 2016-10-26