Alfa Libraries

Proof development can be speed up dramatically bu using libraries of re-usable proofs, just like program development can be speed up by using libraries of program components. Alfa should of course be accompanied by a large set of standard libraries...

Libraries

Michael Hedberg is working on a New standard library for Alfa. It is included in Alfa distribution dated 2002-08-01 or later. Documentation is under preparation.

Examples

Some example files are available. They can be found by clicking on the Library button in the file selection window when opening a file in Alfa.

At present, the following modules are available:

Bool Defines the type Bool for booleans (truth values) and some functions.
BoolProp Defines the proposition that a boolean is true.
Either Defines a type for disjount sum and some associeated functions.
Functions Basic combinators and function composition.
Maybe A type for optional values and associated functions.
Nat A type for natural numbers, addition, multiplication and equality.
NatProp Properties of natural numbers, mainly that both addition and multiplication are associative and commutative.
Pair A type for cartesian products, the funcions curry and uncurry.
Predikatlogik Connectives and inferences rules for predicate calculus.
Prop Defines the type Prop (for propositions as types), the trivially true proposition and the false (absurd) proposition.
Satslogik Connectives and inference rules for propositional calculus.
evenodd Standalone, functional programming example. Defines the type Bool, the type Nat and the functions even and odd from Nat to Bool. (Used in Keyboard tutorial.)
localQuant The power of dependent types, compared with Haskell.
predikatlogikExempel Sample natural deduction style proofs of some propositions in predicate logic.
satslogikExempel Sample natural deduction style proofs of some propositions in propositional calculus.
Naming convensions in these examples were inspired by Haskell.