Logisk programmering - Logic programming

"Regelbaserade" omdirigeringar här. För metoden för maskinöversättning, se Regelbaserad maskinöversättning . För metoder för maskininlärning, se Regelbaserat maskininlärning .
Programmeringsparadigm

Logisk programmering är ett programmeringsparadigm som till stor del bygger på formell logik . Varje program som är skrivet på ett logiskt programmeringsspråk är en uppsättning meningar i logisk form som uttrycker fakta och regler om någon problemdomän. Stora logiska programmeringsspråkfamiljer inkluderar Prolog , svarsuppsättningsprogrammering (ASP) och Datalog . På alla dessa språk skrivs regler i form av klausuler :

H :- B1, …, Bn.

och läses deklarativt som logiska konsekvenser:

H if B1 and … and Bn.

Hkallas regelns huvud och , ..., kallas kroppen . Fakta är regler som inte har någon kropp, och är skrivna i den förenklade formen: B1Bn

H.

I det enklaste fallet där H, ..., alla är atomformler , kallas dessa klausuler bestämda klausuler eller hornklausuler . Det finns dock många förlängningar av detta enkla fall, det viktigaste är fallet där förhållanden i en klausul också kan vara negationer av atomformler. Logiska programmeringsspråk som inkluderar denna förlängning har kunskapsrepresentationsförmågan hos en icke-monoton logik . B1Bn

I ASP och Datalog har logikprogram endast en deklarativ avläsning, och deras utförande utförs med hjälp av ett provningsförfarande eller modellgenerator vars beteende inte är avsett att styras av programmeraren. I Prolog-familjen Prolog har emellertid logikprogram också en procedurell tolkning som målreducerande förfaranden:

att lösa H, lösa och ... och lösa .B1Bn

Tänk på följande klausul som ett exempel:

fallible(X) :- human(X).

baserat på ett exempel som Terry Winograd använde för att illustrera programmeringsspråket Planner . Som en klausul i ett logikprogram kan det användas både som ett förfarande för att testa om det Xär falliblegenom att testa om det Xär human, och som ett förfarande för att hitta Xvilket som är falliblegenom att hitta ett Xvilket är human. Även fakta har en procedurell tolkning. Till exempel klausulen:

human(socrates).

kan användas både som ett förfarande för att visa att socratesär human, och som ett förfarande för att hitta en Xsom är humanav "tilldela" socratestill X.

Den deklarativa läsningen av logiska program kan användas av en programmerare för att verifiera att de är korrekta. Dessutom kan logikbaserade tekniker för programtransformation också användas för att omvandla logiska program till logiskt ekvivalenta program som är mer effektiva. I Prolog-familjen av logiska programmeringsspråk kan programmeraren också använda det kända problemlösningsbeteendet hos körningsmekanismen för att förbättra programmens effektivitet.

Historia

Användningen av matematisk logik för att representera och köra datorprogram är också ett inslag i lambda -kalkylen , utvecklad av Alonzo Church på 1930 -talet. Det första förslaget att använda den klausulära logikformen för att representera datorprogram gjordes dock av Cordell Green . Detta använde en axiomatisering av en delmängd av LISP , tillsammans med en representation av en input-output-relation, för att beräkna relationen genom att simulera genomförandet av programmet i LISP. Foster och Elcocks Absys , å andra sidan, använde en kombination av ekvationer och lambda -beräkning i ett påstått programmeringsspråk som inte sätter några begränsningar för ordningen i vilken operationer utförs.

Logisk programmering i dess nuvarande form kan spåras tillbaka till debatter i slutet av 1960 -talet och början av 1970 -talet om deklarativa kontra procedurella representationer av kunskap inom artificiell intelligens . Förespråkare för deklarativa representationer arbetade särskilt på Stanford , associerade med John McCarthy , Bertram Raphael och Cordell Green, och i Edinburgh , med John Alan Robinson (en akademisk besökare från Syracuse University ), Pat Hayes och Robert Kowalski . Förespråkare för procedurföreställningar var främst centrerade vid MIT , under ledning av Marvin Minsky och Seymour Papert .

Även om det var baserat på logikens bevismetoder, var Planner , utvecklat vid MIT, det första språket som växte fram inom detta proceduralistiska paradigm. Planeraren innehöll mönsterriktad påkallande av procedurplaner från mål (dvs. målreduktion eller bakåtgående kedja ) och från påståenden (dvs. framåtkedjning ). Den mest inflytelserika implementeringen av Planner var delmängden av Planner, kallad Micro-Planner, implementerad av Gerry Sussman , Eugene Charniak och Terry Winograd . Det användes för att genomföra Winograds naturliga språkförståelseprogram SHRDLU , som var ett landmärke vid den tiden. För att klara de mycket begränsade minnessystemen vid den tiden använde Planner en backtracking -kontrollstruktur så att endast en möjlig beräkningsväg behövde lagras åt gången. Planner gav upphov till programmeringsspråken QA-4, Popler, Conniver, QLISP och det samtidiga språket Ether.

Hayes och Kowalski i Edinburgh försökte förena det logikbaserade deklarativa tillvägagångssättet för kunskapsrepresentation med Planners processuella tillvägagångssätt. Hayes (1973) utvecklade ett ekvationsspråk, Golux, där olika förfaranden kunde erhållas genom att förändra beteendet hos teoremprover. Kowalski, å andra sidan, utvecklade SLD-upplösning , en variant av SL-upplösning, och visade hur den behandlar implikationer som målreducerande förfaranden. Kowalski samarbetade med Colmerauer i Marseille, som utvecklade dessa idéer i utformningen och genomförandet av programmeringsspråket Prolog .

Den Föreningen för Logikprogrammering grundades för att främja Logikprogrammering 1986.

Prolog gav upphov till programmeringsspråken ALF , Fril , Gödel , Mercury , Oz , Ciao , Visual Prolog , XSB och λProlog , samt en mängd samtidiga logiska programmeringsspråk , begränsande logiska programmeringsspråk och Datalog .

Begrepp

Logik och kontroll

Huvudartikel: Deklarativ programmering

Logisk programmering kan ses som kontrollerat avdrag. Ett viktigt begrepp i logisk programmering är separering av program i deras logikkomponent och deras kontrollkomponent. Med rena logiska programmeringsspråk bestämmer logikkomponenten ensam de lösningar som produceras. Kontrollkomponenten kan varieras för att tillhandahålla alternativa sätt att köra ett logiskt program. Denna uppfattning fångas av parollen

Algoritm = Logik + kontroll

där "Logik" representerar ett logikprogram och "Kontroll" representerar olika teorembevisande strategier.

Problemlösning

I det förenklade, propositionella fallet där ett logikprogram och ett atommål på högsta nivå inte innehåller några variabler, bestämmer baklängesresonemang ett och-eller-träd , som utgör sökutrymmet för att lösa målet. Det översta målet är trädets rot. Med tanke på vilken nod som helst i trädet och en klausul vars huvud matchar noden, finns det en uppsättning barnsnoder som motsvarar delmålen i klausulens kropp. Dessa barns noder grupperas tillsammans med ett "och". De alternativa uppsättningarna barn som motsvarar alternativa sätt att lösa noden grupperas tillsammans med ett "eller".

Vilken sökstrategi som helst kan användas för att söka i det här utrymmet. Prolog använder en sekventiell, sist-in-först-ut, backtracking-strategi, där endast ett alternativ och ett delmål övervägs åt gången. Andra sökstrategier, som parallell sökning, intelligent backtracking eller bäst-först-sökning för att hitta en optimal lösning, är också möjliga.

I det mer allmänna fallet, där delmål delar variabler, kan andra strategier användas, till exempel att välja den delmål som är högst instanserad eller som är tillräckligt instanserad så att endast ett förfarande gäller. Sådana strategier används till exempel vid samtidig logisk programmering .

Negation som misslyckande

Huvudartikel: Negation som misslyckande

För de flesta praktiska tillämpningar, liksom för applikationer som kräver icke-monoton resonemang inom artificiell intelligens, måste Horn-klausulprogrammen utökas till normala logikprogram, med negativa förhållanden. En klausul i ett normalt logikprogram har formen:

H :- A1, …, An, not B1, …, not Bn.

och läses deklarativt som en logisk implikation:

H if A1 and … and An and not B1 and … and not Bn.

var Hoch alla och är atomformler. Negationen i de negativa bokstavarna kallas vanligtvis " negation som misslyckande ", eftersom i de flesta implementeringar visas ett negativt tillstånd att hålla genom att visa att det positiva tillståndet inte håller. Till exempel: AiBi not Bi not Bi Bi

canfly(X) :- bird(X), not abnormal(X).
abnormal(X) :- wounded(X).
bird(john).
bird(mary).
wounded(john).

Med tanke på målet att hitta något som kan flyga: 

:- canfly(X).

det finns två kandidatlösningar, som löser det första delmålet bird(X), nämligen X = johnoch X = mary. Den andra delmålet not abnormal(john)i den första kandidatlösningen misslyckas, eftersom den wounded(john)lyckas och därför abnormal(john)lyckas. Den andra delmålet not abnormal(mary)i den andra kandidatlösningen lyckas emellertid, eftersom den wounded(mary)misslyckas och därför abnormal(mary)misslyckas. Därför X = maryär den enda lösningen på målet.

Micro-Planner hade en konstruktion, kallad "thnot", som när den appliceras på ett uttryck returnerar värdet sant om (och endast om) utvärderingen av uttrycket misslyckas. En motsvarande operatör finns vanligtvis i moderna Prolog -implementeringar. Det är vanligtvis skrivet som eller , var är något mål (förslag) som ska bevisas av programmet. Denna operator skiljer sig från negation i första ordningens logik: en negation som misslyckas när variabeln har bundits till atomen , men den lyckas i alla andra fall, inklusive när den är obunden. Detta gör Prologs resonemang icke-monotont : misslyckas alltid, medan det kan lyckas, bindande till , beroende på om det ursprungligen var bundet (notera att standard Prolog utför mål i vänster till höger ordning). not(Goal)\+ GoalGoal\+ X == 1X1XX = 1, \+ X == 1\+ X == 1, X = 1X1X

Negationens logiska status som misslyckande var olöst tills Keith Clark [1978] visade att det under vissa naturliga förhållanden är ett korrekt (och ibland komplett) genomförande av klassisk negation med avseende på programmets slutförande. Slutförandet uppgår ungefär till uppsättningen av alla programklausuler med samma predikat på vänster sida, säg

H :- Body1.
…
H :- Bodyk.

som en definition av predikatet

H iff (Body1 or … or Bodyk)

där "iff" betyder "om och bara om". För att skriva färdigställandet krävs också uttrycklig användning av jämlikhetspredikatet och införandet av en uppsättning lämpliga axiom för jämlikhet. Implementering av negation som misslyckande behöver dock bara om-halvorna av definitionerna utan axiomen för jämlikhet.

Till exempel är genomförandet av programmet ovan:

canfly(X) iff bird(X), not abnormal(X).
abnormal(X) iff wounded(X).
bird(X) iff X = john or X = mary.
X = X.
not john = mary.
not mary = john.

Begreppet slutförande är nära besläktat med McCarthys omskrivningssemantik för standardresonemang och till den slutna världens antagande .

Som ett alternativ till kompletteringssemantiken kan negation som misslyckande också tolkas epistemiskt, som i den stabila modellsemantiken för svarsuppsättningsprogrammering . I denna tolkning betyder inte (B i ) bokstavligen att Bi inte är känd eller inte tros. Den epistemiska tolkningen har fördelen att den mycket enkelt kan kombineras med klassisk negation, som i "utökad logikprogrammering", för att formalisera sådana fraser som "det motsatta kan inte visas", där "motsats" är klassisk negation och "inte kan visa ”är den epistemiska tolkningen av negation som misslyckande.

Kunskapsrepresentation

Det faktum att Horn-klausuler kan ges en procedurell tolkning och, tvärtom, att målreducerande förfaranden kan förstås som Horn-klausuler + bakåtriktat resonemang innebär att logikprogram kombinerar deklarativa och processuella representationer av kunskap . Inkluderingen av negation som misslyckande innebär att logisk programmering är en slags icke-monoton logik .

Trots sin enkelhet jämfört med klassisk logik har denna kombination av Hornklausuler och negation som misslyckande visat sig vara överraskande uttrycksfull. Till exempel ger den en naturlig representation för de vanliga lagarna om orsak och verkan, som formaliseras av både situationskalkylen och händelseberäkningen . Det har också visat sig motsvara helt naturligt lagstiftningens halvformella språk. I synnerhet krediterar Prakken och Sartor framställningen av den brittiska nationalitetslagen som ett logikprogram med att vara "enormt inflytelserikt för utvecklingen av beräkningsrepresentationer av lagstiftning, vilket visar hur logisk programmering möjliggör intuitivt tilltalande representationer som direkt kan distribueras för att generera automatiska slutsatser" .

Varianter och tillägg

Prolog

Huvudartikel: Prolog

Programmeringsspråket Prolog utvecklades 1972 av Alain Colmerauer . Det kom fram från ett samarbete mellan Colmerauer i Marseille och Robert Kowalski i Edinburgh. Colmerauer arbetade med förståelse av naturligt språk , med logik för att representera semantik och med upplösning för att besvara frågor. Under sommaren 1971 upptäckte Colmerauer och Kowalski att den logiska formen av logik kan användas för att representera formella grammatiker och att upplösningssatser kan användas för analys. De observerade att vissa teoremprovers, som hyperupplösning, beter sig som parsers bottom-up och andra, som SL-resolution (1971), beter sig som top-down parsers.

Det var på sommaren 1972 som Kowalski, som åter arbetade med Colmerauer, utvecklade den procedurella tolkningen av konsekvenser. Denna dubbla deklarativa/procedurella tolkning blev senare formaliserad i Prolog -notationen

H :- B1, …, Bn.

som kan läsas (och användas) både deklarativt och procedurmässigt. Det blev också klart att sådana klausuler kan begränsas till bestämda klausuler eller Hornklausuler , där H, ..., alla är atomiska predikatlogikformler, och att SL-upplösning kan begränsas (och generaliseras) till LUSH- eller SLD-upplösning . Kowalskis procedurtolkning och LUSH beskrevs i ett memo från 1973, publicerat 1974. B1Bn

Colmerauer, tillsammans med Philippe Roussel, använde denna dubbla tolkning av klausuler som grund för Prolog, som implementerades sommaren och hösten 1972. Det första Prolog-programmet, som också skrevs 1972 och implementerades i Marseille, var ett franskt frågesvarssystem . Användningen av Prolog som ett praktiskt programmeringsspråk fick stor fart genom utvecklingen av en kompilator av David Warren i Edinburgh 1977. Experiment visade att Edinburgh Prolog kunde konkurrera med bearbetningshastigheten för andra symboliska programmeringsspråk som Lisp . Edinburgh Prolog blev de facto -standarden och påverkade starkt definitionen av ISO -standard Prolog.

Abduktiv logikprogrammering

Abduktiv logikprogrammering är en förlängning av normal logisk programmering som gör att vissa predikat, deklarerade som abducerbara predikat, kan vara "öppna" eller odefinierade. En klausul i ett abduktivt logikprogram har formen:

H :- B1, …, Bn, A1, …, An.

var Hfinns en atomformel som inte är abducerbar, alla är bokstäver vars predikat inte är abducerbara, och det är atomformler vars predikat är abducerbara. De abducerbara predikaten kan begränsas av integritetsbegränsningar, som kan ha formen: BiAi

false :- L1, …, Ln.

där de är godtyckliga bokstäver (definierade eller abducerbara och atomiska eller negerade). Till exempel: Li

canfly(X) :- bird(X), normal(X).
false :- normal(X), wounded(X).
bird(john).
bird(mary).
wounded(john).

där predikatet normalär abducerbart.

Problemlösning uppnås genom att härleda hypoteser uttryckta i termer av de abducerbara predikaten som lösningar på problem som ska lösas. Dessa problem kan antingen vara observationer som måste förklaras (som i klassiskt abduktivt resonemang ) eller mål som ska lösas (som i normal logisk programmering). Till exempel normal(mary)förklarar hypotesen observationen canfly(mary). Dessutom innebär samma hypotes den enda lösningen X = marypå målet att hitta något som kan flyga: 

:- canfly(X).

Abduktiv logikprogrammering har använts för feldiagnos, planering, bearbetning av naturligt språk och maskininlärning. Det har också använts för att tolka Negation som misslyckande som en form av abduktivt resonemang.

Metalogisk programmering

Eftersom matematisk logik har en lång tradition av att skilja mellan objektspråk och metaspråk, tillåter logisk programmering också metallnivåprogrammering . Det enklaste metalogiska programmet är den så kallade " vanilj " metatolkaren: 

    solve(true).
    solve((A,B)):- solve(A),solve(B).
    solve(A):- clause(A,B),solve(B).

där true representerar en tom konjunktion och klausul (A, B) betyder att det finns en klausul på objektnivå med formen A:- B.

Metallogisk programmering gör det möjligt att kombinera representationer på objektnivå och metallnivå, som i naturligt språk. Det kan också användas för att implementera logik som anges som slutsatsregler . Metalogic används i logikprogrammering för att implementera metaprogram, som manipulerar andra program, databaser, kunskapsbaser eller axiomatiska teorier som data.

Begränsning av logisk programmering

Huvudartikel: Constraint logic programmering

Begränsningslogikprogrammering kombinerar logisk programmering av hornklausul med begränsningslösning . Det utvidgar Horn -klausuler genom att låta vissa predikat, deklarerade som begränsningspredikat, förekomma som bokstavar i klausulernas kropp. Ett begränsningslogikprogram är en uppsättning klausuler i formuläret:

H :- C1, …, Cn ◊ B1, …, Bn.

var Hoch alla är atomformler, och det är begränsningar. Deklarativt läses sådana klausuler som vanliga logiska konsekvenser: BiCi

H if C1 and … and Cn and B1 and … and Bn.

Även om predikaten i klausulernas huvuden definieras av begränsningslogikprogrammet, är predikaten i begränsningarna fördefinierade av någon domänspecifik modellteoretisk struktur eller teori.

Procedurellt löses delmål vars predikat definieras av programmet genom målreduktion, som i vanlig logisk programmering, men begränsningar kontrolleras för tillfredsställelse av en domenspecifik begränsningslösare, som implementerar semantiken i begränsningspredikat. Ett första problem löses genom att reducera det till en tillfredsställande kombination av begränsningar.

Följande begränsningslogikprogram representerar en leksaks temporal databas över john'shistoria som lärare: 

teaches(john, hardware, T) :- 1990 ≤ T, T < 1999.
teaches(john, software, T) :- 1999 ≤ T, T < 2005.
teaches(john, logic, T) :- 2005 ≤ T, T ≤ 2012.
rank(john, instructor, T) :- 1990 ≤ T, T < 2010.
rank(john, professor, T) :- 2010 ≤ T, T < 2014.

Här ≤och <är villkors predikat, med sina vanliga avsedda semantik. Följande målklausul frågar databasen för att ta reda på när johnbåde undervisas logicoch var en professor:

:- teaches(john, logic, T), rank(john, professor, T).

Lösningen är 2010 ≤ T, T ≤ 2012.

Begränsningslogikprogrammering har använts för att lösa problem inom områden som anläggningsteknik , maskinteknik , digital kretsverifiering, automatiserad tidtabell , flygtrafikledning och finansiering. Det är nära besläktat med abduktiv logikprogrammering .

Samtidig logikprogrammering

Huvudartikel: Samtidig logikprogrammering

Samtidig logisk programmering integrerar begrepp för logisk programmering med samtidig programmering . Utvecklingen fick en stor drivkraft på 1980 -talet genom valet av systemprogrammeringsspråk för det japanska femte generationens projekt (FGCS) .

Ett samtidigt logikprogram är en uppsättning bevakade hornklausuler i formen:

H :- G1, …, Gn | B1, …, Bn.

Konjunktionen kallas klausulens vakt och är åtagandeoperatören. Deklarativt läses bevakade hornklausuler som vanliga logiska konsekvenser: G1, ... , Gn |

H if G1 and … and Gn and B1 and … and Bn.

Men procedurmässigt, när det finns flera klausuler vars huvuden H matchar ett givet mål, utförs alla klausulerna parallellt och kontrollerar om deras vakter håller. Om vakterna i mer än en klausul håller, görs ett beslutat val mot en av klausulerna, och utförandet fortsätter med delmålen i den valda klausulen. Dessa delmål kan också köras parallellt. Således implementerar samtidig logisk programmering en form av "don't care nondeterminism", snarare än "don't know nondeterminism". G1, ... , Gn B1, ..., Bn

Till exempel definierar följande samtidiga logikprogram ett predikat shuffle(Left, Right, Merge) , som kan användas för att blanda två listor Leftoch Rightkombinera dem till en enda lista Mergesom bevarar ordningen av de två listorna Leftoch Right: 

shuffle([], [], []).
shuffle(Left, Right, Merge) :-
    Left = [First | Rest] |
    Merge = [First | ShortMerge],
    shuffle(Rest, Right, ShortMerge).
shuffle(Left, Right, Merge) :-
    Right = [First | Rest] |
    Merge = [First | ShortMerge],
    shuffle(Left, Rest, ShortMerge).

Här []representerar den tomma listan och [Head | Tail]representerar en lista med det första elementet Headföljt av listan Tail, som i Prolog. (Observera att den första förekomsten av | i den andra och tredje klausulen är listkonstruktorn, medan den andra förekomsten av | är åtagandeoperatören.) Programmet kan till exempel användas för att blanda listorna [ace, queen, king]och [1, 4, 2]genom att åberopa målklausulen: 

shuffle([ace, queen, king], [1, 4, 2], Merge).

Programmet kommer till exempel icke-deterministiskt att skapa en enda lösning Merge = [ace, queen, 1, king, 4, 2].

Förmodligen är samtidig logisk programmering baserad på meddelandeöverföring, så den är föremål för samma obestämdhet som andra samtidiga meddelandeöverförande system, till exempel Actors (se Obestämbarhet i samtidig beräkning ). Carl Hewitt har hävdat att samtidig logisk programmering inte är baserad på logik i hans bemärkelse att beräkningssteg inte logiskt kan härledas. Vid samtidig logisk programmering är emellertid alla resultat av en avslutande beräkning en logisk följd av programmet, och alla delresultat av en delberäkning är en logisk konsekvens av programmet och det återstående målet (processnätverk). Beräkningarnas obestämbarhet innebär således att inte alla logiska konsekvenser av programmet kan härledas.

Samtidig begränsning av logisk programmering

Huvudartikel: Samtidig begränsning av logisk programmering

Concurrent constraint logic programmering kombinerar concurrent logic programmering och constraint logic programmering , using constraints to control concurrency. En klausul kan innehålla ett skydd, som är en uppsättning begränsningar som kan blockera tillämpningen av klausulen. När vakterna i flera klausuler är nöjda, gör samtidig begränsningslogikprogrammering ett engagerat val att bara använda en.

Induktiv logisk programmering

Huvudartikel: Induktiv logisk programmering

Induktiv logikprogrammering handlar om att generalisera positiva och negativa exempel i bakgrundskunskap: maskininlärning av logikprogram. Det senaste arbetet inom detta område, som kombinerar logisk programmering, inlärning och sannolikhet, har gett upphov till det nya området statistiskt relationellt lärande och probabilistisk induktiv logisk programmering .

Logikprogrammering av högre ordning

Flera forskare har utökat logikprogrammering med högre ordningsfunktioner som härrör från logik av högre ordning , till exempel predikatvariabler. Sådana språk inkluderar Prolog -tilläggen HiLog och λProlog .

Linjär logisk programmering

Att basera logisk programmering inom linjär logik har resulterat i utformningen av logiska programmeringsspråk som är betydligt mer uttrycksfulla än de som bygger på klassisk logik. Hornklausulprogram kan endast representera tillståndsförändring genom ändringen av argument till predikat. I linjär logisk programmering kan man använda den omgivande linjära logiken för att stödja tillståndsförändringar. Några tidiga konstruktioner av logiska programmeringsspråk baserade på linjär logik inkluderar LO [Andreoli & Pareschi, 1991], Lolli, ACL och Forum [Miller, 1996]. Forum ger en målinriktad tolkning av all linjär logik.

Objektorienterad logikprogrammering

F-logik utökar logisk programmering med objekt och ramsyntax.

Logtalk utökar programmeringsspråket Prolog med stöd för objekt, protokoll och andra OOP -koncept. Den stöder de flesta standardkompatibla Prolog-system som backend-kompilatorer.

Transaktionslogikprogrammering

Transaktionslogik är en förlängning av logisk programmering med en logisk teori om tillståndsmodifierande uppdateringar. Den har både en modellteoretisk semantik och en procedurell. En implementering av en delmängd av transaktionslogik är tillgänglig i Flora-2- systemet. Andra prototyper är också tillgängliga .

Se även

Citat

Källor

Allmänna introduktioner

Andra källor

Vidare läsning

externa länkar