Alfa är en efterföljare till beviseditorn ALF, dvs en editor för direktmanipulering av bevisobjekt i ett logiskt ramverk baserat på Per Martin-Löfs typteori. Med Alfa kan man, interaktivt och inkrementellt, definiera teorier (axiom och härledningsregler), formulera satser och konstruera bevis av satser. Alla steg i beviskonstruktionen kontrolleras direkt av systemet, så det är omöjligt att konstruera felaktiga bevis.

Man kan också se Alfa som ett syntaxorienterad redigeringsprogram för ett litet, rent funktionellt programmeringsspråk med ett typsystem som har beroende typer. Det funktionella språket är i själva verket mycket likt språket Cayenne av Lennart Augustsson.

Alfa utvecklas av några av medlemmarna i Programmeringslogikgruppen vid Chalmers. Alfa utnyttjar ett beviskontrollprogram som ursprungligen skrevs av Thierry Coquand (V3) och sedan vidareutvecklades av Catarina Coquand (Agda). De senaste förbättringarna av Agda har gjorts av Makoto Takeyama. Han har lagt till idata-konstruktionen, för att få tillbaka en del av den uttryckskraft som fanns i de induktiva datadefintionerna i det gamla ALF-systemet.

Alfa har också visst stöd för att arbeta med översättningar av bevis till naturligt språk, genom att koppla ihop Alfa med Aarne Rantas Grammatiska Ramverk, GF.

Det grafiska användargränssnittet och infrastrukturen som kopplar samman alltihop implementeras av Thomas Hallgren. Alla programdelar skrivs i språket Haskell.

Vill du ladda ner Alfa, se nedan.

Alfa-dokumentation

• Features of Alfa. Kort beskrivning av Alfa och dess implementering. Planer på framtida förbättringar. Begränsningar i den nuvarande versionen.
• Alfa User's Guide. Användarmanual.
• Quick reference pages:
  • Command line syntax and options.
  • Top 10 ways to fill in a place holder.
  • Overview of the menus.
  • Overview of the keyboard.
  • Printing Alfa documents.
  • Using Alfa plug-in modules.
• Tutorials:
  • Editing by using the keyboard only.
  • Constructing proofs in Natural Deduction style.
  • Using the GF plug-in to produce natural language translations of proofs.
• Alfa Library/Example Modules.

• History of changes. Nyheter i Alfa (uppdaterad 2023-04-23).
• Known Bugs. Kända fel och brister (uppdaterad 2023-04-23).

Länkar

• Agda. Bevismotorn som används i Alfa.
• GF - det Grammatiska Ramverket, som används i Alfa för att översätta bevis till och från naturligt språk.
• Andra Bevisassistenter i webbkatalogen dmoz open directory.

Ladda ner Alfa

Alfa har testats och fungerar på bland annat följande system (oktober 2000):

• NetBSD 1.4/i386, FreeBSD 3.2/i386, Redhat Linux/i386 (version 5.2, 6.2 och 7.0)
• SunOS-5.x/sparc (=Solaris 2.x)

Uppdatering 2020-10-26: uppdaterade källkodpaket för Fudgets och Alfa är nu tillgängliga, för att göra det lättare att kompilera Alfa med de senaste versionerna av GHC. Det binära installationspaketet för macOS som nämns ovan finns också kvar.