Alfa (particle traces)

[In English]

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.

Alfa finns installerad på Unix-datorerna vid vår institution och startas med kommandot alfa. Externa användare kan ladda ner Alfa, se nedan.


Alfa-dokumentation

Resten av dokumentationen är på engelska.

Länkar


Ladda ner Alfa

(Inga binärdistributioner finns att ladda ner längre, pga omorganisation. Tack för det, Chalmers.)

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


5 Jul 2012 19:45 Thomas Hallgren
Länkar