You are here: TUCS > PUBLICATIONS > Publication Search > Matematik med lite logik: Logi...
Matematik med lite logik: Logik för strukturerade härledningar
Ralph-Johan Back, Matematik med lite logik: Logik för strukturerade härledningar. TUCS Lecture Notes 8, Turku Centre for Computer Science, 2008.
Abstract:
Strukturerade härledningar bygger vidare på en tradition som initierats av Edsger W. Dijkstra, en av de stora pionjärerna i datateknisk forskning. Dijkstra och hans kolleger (Wim Feijen, Carel Scholten och Nettie van Gasteren) koncentrerade sig på att göra matematiska bevis både enkla och exakta. De utvecklade en notation som i branschen går under namnet calculational proof [9, 11, 10]. En exakt översättning skulle vara kalkylliknande bevis, men vi har valt att kalla dem linjära härledningar eller beviskedjor på svenska. Avsikten var att matematiska bevis och härledningar skulle vara mera lika beräkningar, som när man löser ekvationer, förenklar uttryck eller utför multiplikation och division för hand. Det här målet uppnås genom att utnyttja logik som en samling räkneregler, som används för att bestämma sanningen av matematiska påståenden.
Joakim von Wright och jag utvecklade strukturerade härledningar som en vidareutveckling av Dijkstras linjära härledningar. Metoden har ursprungligen presenterats i vår bok om refinement kalkylen [5] samt i en tidskriftspublikation [4]. I boken utnyttjar vi strukturerade härledningar för ett stort antal mer eller mindre komplicerade bevis inom programmeringslogiken. Dijkstras linjära härledningar baserar sig på en variant av första ordningens predikatkalkyl och på ett Hilbert-liknande bevissystem, medan vi har byggt upp strukturerade härledningar kring en klassisk standardlogik, den så kallade högre ordningens logik, och på ett Gentzen-liknande bevissystem. Strukturerade härledningar har vidareutvecklats efterhand, och kan nu ses som en syntes av klassiska Gentzenliknande bevis, Hilbert-liknande bevis och Dijkstras lineära härledningar.
Strukturerade härledningar baserar sig på explicit användningen av logik i bevisen. Då man definierar bevissystem försöker man ofta postulera så få axiom och slutledningsregler som möjligt, och sedan visa att andra användbara axiom kan härledas från de postulerade axiomen med de postulerade slutledningsreglerna. Det här gör det lättare att bevisa allmänna påståenden om bevissystemet. I praktisk användning av logik är distinktionen mellan postulerade och härledda axiom inte viktig, däremot är det viktiga att ha en bra grundsamling av teorem och härledningsregler, och att vid behov kunna härleda nya teorem och härledningsregler från denna samling.
I de följande kapitlen går vi igenom ett antal användbara regler för hur man kan resonera logiskt med konnektiver och kvantorer. Samlingen är inte uttömmande, det finns fler användbara regler än de som ges nedan, men den ger en relativt bra verktygsback för att resonera logiskt i matematiska bevis. Vi börjar med att kortfattat beskriva strukturerade härledningar, i kapitel 2. Kapitel 3 beskriver propositionskalkylen och visar hur den kan användas i strukturerade härledningar. Vi visar hur man bevisar logiska påståenden med beviskedjor, beskriver de vanliga konnektiverna i propositionskalkylen och ger deras grundegenskaper. Vi ger också de vanligaste slutledningsreglerna för propositionskalkylen, visar hur de används i strukturerade härledningar samt beskriver logiska substitutionsregler. De här slutledningsreglerna illustreras i Kapitel 4 med en samling exempelhärledningar. Kapitel 5 beskriver predikatkalkylen. Vi introducerar universell och existentiell kvantifiering, ger kvantorernas grundegenskaper samt de grundläggande slutledningsreglerna för kvantorer. Vi ger även en översikt av allmänt användbara kvantifieringsreger, samt visar hur man använder kvantifieringsreglerna i praktiska matematiska bevis. I det sista kapitlet ger vi exempel på typiska problem med härledningar där kvantifieringsreglerna utnyttjas på ett icke-trivialt sätt.
Files:
Full publication in PDF-format
BibTeX entry:
@BOOKLET{Back08e,
title = {Matematik med lite logik: Logik för strukturerade härledningar},
author = {Back, Ralph-Johan},
number = {8},
series = {TUCS Lecture Notes},
publisher = {Turku Centre for Computer Science},
year = {2008},
}
Belongs to TUCS Research Unit(s): Learning and Reasoning Lab