02357 Array-baseret logik og systemer

Forelæsninger og øvelser i bygning 325, rum 201.

Forelæsningerne vil finde sted hver tirsdag 13-17, startende 30. januar 2007. Normalt vil der være to timers forelæsninger efterfulgt af øvelser ved PC.

Kontakt person: Peter Falster, IMM, DTU, Bygning 325, rum 218, email: pfa@imm.dtu.dk

Forudsætninger:
Grundlæggende matematik og programmering. Herudover vil det være en fordel at have kendskab til linear algebra, diskret matematik, grafteori og logik.

Lektionerne vil være baseret på engelske artikler, noter og overheads.
Evaluering: Rapport over mindre projekt-opgave.
Point: 5.

Bemærkninger: Faget består af en kombineret teori/øvelseperiode og en afsluttende projektperiode. Deltagerne inddeles i arbejdsgrupper der skal samarbejde om øvelser/projekt.

I forbindelse med kurset er der øvelser dels i det matematiske sprog Q'Nial (Nested Interactive Array Language) og dels i Array Technology's Array Database.

Kursusmål:
Arraybaseret logik er en ny IT niche, der mere generelt betegnes arraybaseret teknologi. Til grund for teknologien ligger en teori, der sikrer at logiske systemer er fejlfrie - af betydning for jernbanedrift, elforsyning og generelt infrastruktur, hvor der stilles krav til sikkerhed. Jernbanernes færdselslov for kørsel med tog bestemmer hvorledes sporskifterne skal stilles, for at danne en sikker togvej fra station A til station B og overholdes af sikringsanlægget i form af signaler. Tilsvarende for elforsyning er der sikkerhedskrav for ind- og udkobling af udstyr, hvor teorien sikrer at brydere sluttes og brydes i den rigtige rækkefølge såvel af personsikkerhedsgrunde men også af forsyningsgrunde. Teorien har også fundet anvendelse til konfigurering af produkter og indlejrede styringer, for eksempel i audio-video produkter, mobile computing og fejltolerante kontrolsystemer. Kursets formål er at give deltagerne teoretisk indsigt i den arraybaserede logik, som er frembragt indenfor området systemlære.

Kursusindhold:
Arraybaseret logik har videnskabeligt grundlag i en geometrisk-algebraisk formalisering af logikken. Den arraybaserede logik behandler logikken som en fysisk disciplin udfra en opfattelse af tildeling af logiske sandhedsværdier som fysiske målinger. Logikken er således fortolket i lyset af fysikken, som oprindelig påpeget af C.S. Peirce.

I kurset gennemgås (1) det videnskabelige grundlag for denne teknologi, med særlig vægt på den arrayteoretiske formulering af logikken, (2) det teknologiske grundlag, herunder komprimering af store datamængder, metodegrundlag, orienteret mod bl.a. constraint resolution, state-event, OLAP og relationsdatabaser, (3) produkter for komponent software og brugervenlig interface til teorien, (4) illustrative anvendelser indenfor jernbaner, elforsyning, telekommunikation, kontrolsystemer, ingeniørmæssig konstruktion og verifikation og teknisk-økonomiske produktionssystemer.

Specifikke emner der behandles i kurset er:

Introduktion

• Om kurset, praktisk information
• Formål med kurset
• Motivering ved showcases (jernbaner, pumper, sygehus, tele, etc.)
• Introduktion til det matematiske arraysprog Q'Nial

• Fælles nøglebegreber fra fysik-logik-matematik henv. Økonomi og produktion
• System- og konstruktionsbegrebet
• Måleskalaer
• Målinger og deres repræsentation ved digrafer - binære relationer
• Introduktion til klassisk udsagnslogik og følgeslutning
• De tre opfattelser af logik og logik som en fysisk disciplin

• En måleskala for sandhedsværdier
• Om begrebet negation
• Booles geniale iagttagelse
• Sandhedstabeller som geometriske objekter
• En geometrisk illustration
• Negation som gruppegenerator
• Produktgruppen C2*C2*C2 defineret ved et simpelt konnektiv
• Geometrisk fortolkning af De Morgan's love
• De trivielle, simple og sammensatte konnektiver
• Om meningsindholdet af de logiske konnektiver implikation og følgerigtighed
• Begreberne tilstrækkelig og nødvendig
• Fra præmisser på klassisk tabelform til arrays ved ydre produkter

• Præmisserne i Galileis dom - eksempel
• Præmisser som primitive elementer og topologi som gensidig kobling af logiske variable
• Jevon's logiske maskine 1869, og dens grundlæggende konstruktionsprincipper
• Inferens/logisk følgeslutning og begrebet kolligering
• Eliminering af tvangsbindinger og fjernelse af alle ulovlige løsninger ved sammensætning af primitive elementer
• Følgeslutning fortolket som en geometrisk løsning
• Bestemmelse af alle løsninger
• Fra logisk til formelt gyldige beviser
• Kontingente systemer og konsistens - med et lån fra fysikken
• Transitivitet og det udelukkede tredjes princip, komposition af relationer

• Boole's development process
• Tilstand af logiske variable, tilstandsvektor
• Deduktion og abduktion

• Produktgruppen af logiske indre produkter og specielt det relative produkt
• Eksempler på anvendelse af det relative produkt

• Introduktion til Array Technology's array data base, Array Studio.

• Isomorfe arrayrepræsentationer med henblik på fuldstændighed, kompakthed og hastighed,
• Data komprimering herunder komprimering af løsningsrum
• State-propagation
• Teknologier for anvendelsen af teorien
  • Constraint resolution
  • Relationsdatabasen (OLTP:On-line transaction processing, Produktionssystemer, GIS)
  • State-event
  • OLAP (On-line Analytical Processing)

• Sikringssystem for jernbaner
• Sikkerhed i elforsyningssystemer
• Ruteplanlægning for telenetværk
• Fejltolerante kontrolsystemer.
• Relationsdatabasen, specielt binære relationer og normalisering
• Teknisk-økonomiske produktionssystemer, herunder styklister, omkostningsberegning, tidsplanlægning
• Fra array-baseret logik til arrayteori

Links:
Array Technology A/S's Array Studio og om Anvendelser: www.arraytechnology.com
Nial Systems Limited's Q'Nial: www.nial.com

Kontakt person:
Peter Falster, IMM, DTU, Bygning 325, rum 218, email: pfa@imm.dtu.dk

Sidst updateret: 19.1.07, fkc@imm.dtu.dk