Formal Algorithmic Knowledge in the FDL
We have formally developed a variety of algorithms from formal specifications. These algorithms will be presented together with their formal specifications and a formal proof of their correctness. They will also be made available online for interactive browsing in the online version of the prototype FDL.
July 2003


 
  The following well-known algorithms are part of the FDL content. We provide links to the HTML version of the actual library content. The object will either be an explicit algorithm or a theorem, from whose proof the algorithm is extracted. The objects provide links to other objects that use the algorithm, especially to theorems that verify its properties.
  • Greatest Common Divisor (origin Nuprl, Cornell)
    A standard algorithm for computing the greatest common divisor (gcd) of two natural numbers.
    See also the PVS library about properties of gcd
  • Quotient Remainder (origin Nuprl, Cornell)
    For a given pair of numbers a,b, find integers q and r such that a = q*b +r.
    An integer division algorithm and a remainder algorithm can be extracted from the proof that q and r exist.
  • Bezout Identity (origin Nuprl, Cornell)
    For a given pair of coprimes a,b, find integers i and j such that i*a+j*b=1.
  • Ramsey's Theorem (origin PVS)
    For a given graph G find a k-clique in G or an independent set with at least k nodes. that a graph, if there is one
  • Propositional Decidability (origin Nuprl, Wyoming)
    An algorithm for deciding whether a propositional formula is true or not
  • The Pigeonhole Principle (origin Nuprl, Cornell)
    A mapping f from a set of size k into a smaller set must map two different elements onto the same element. The algorithm determines these two elements.
  • A collection of basic list algorithms (origin Nuprl, Cornell & Wyoming)
    append: concatenating two list,    
    length: number of elements of a list,    
    map: applying a function to all list elements,    
    reverse: inverting the order of elements in a list,    
    segment: selecting a segment from a list,    
    select: determining the i-th element of a list,    
    reject: removing the i-th element from a list,    
    reduce: iterate an operation over all list elements,    
    is_member: test if x occurs in a list l,    
    remove: removing the first occurrence of x from a list l,    
    filter: select all elements of a list that satisfy a given condition,    
    permute_list: rearrange a list according to an index function,    
    swap: swap two elements in a list
Below is a selection of the more than 100 verified algorithms that are currently being documented and migrated into the FDL from Nuprl, MetaPRL, and PVS.   Further algorithms will be migrated in the future.
We invite contributions of other algorithms that are verified with Nuprl, MetaPRL, PVS, or other formal systems.
  • Depth-first search
    Mark Bickford
  • Dijkstra's Algorithm
    Jim Caldwell
  • Two proofs of Ramsey's Theorem
    David Basin
  • A linear algorithm for computing maximal segment sums
    Joseph Bates, Robert Constable, Matthew Fluet
  • A majority vote algorithm
    Doug Howe, Chet Murthy
  • The pigeonhole principle
    Ralph Benzinger
  • Minimization of Automata
    Robert Constable, Paul Jackson
  • Factorials
    Doug Howe, Paul Jackson
  • Matching and Unification
    Doug Howe
  • Deciding propositional formulas
    Robert Constable, Doug Howe, James Caldwell
  • Tests for Primality
    Robert Constable