Monadic annenordens logikk - Monadic second-order logic
I matematisk logikk er monadisk annenordenslogikk ( MSO ) fragmentet av andreordenslogikk der andreordens kvantifisering er begrenset til kvantifisering over sett. Det er spesielt viktig i logikken til grafer , på grunn av Courcelles teorem , som gir algoritmer for å evaluere monadiske andreordens formler over grafer med begrenset trebredde .
Andreordens logikk tillater kvantifisering over predikater . MSO er imidlertid fragmentet der andreordens kvantifisering er begrenset til monadiske predikater (predikater som har et enkelt argument). Dette blir ofte beskrevet som kvantifisering over "sett" fordi monadiske predikater tilsvarer uttrykkskraft til sett (settet med elementer som predikatet er sant for).
Beregningskompleksitet av evaluering
Eksistensiell monadisk andreordens logikk (EMSO) er fragmentet av MSO der alle kvantifiseringer over sett må være eksistensielle kvantifiseringer , utenfor noen annen del av formelen. Førsteordens kvantifiserere er ikke begrenset. I analogi med Fagins teorem , ifølge hvilken eksistensiell (ikke-monadisk) andreordens logikk fanger nøyaktig den beskrivende kompleksiteten til kompleksitetsklassen NP , har klassen av problemer som kan uttrykkes i eksistensiell monadisk andreordens logikk blitt kalt monadisk NP . Begrensningen til monadisk logikk gjør det mulig å påvise atskillelser i denne logikken som ikke er bevist for ikke-monadisk andreordens logikk. For eksempel, i logikken til grafer , tilhører testing om en graf er koblet fra monadisk NP, ettersom testen kan representeres av en formel som beskriver eksistensen av et skikkelig delsett av hjørner uten kanter som forbinder dem med resten av grafen ; det komplementære problemet, å teste om en graf er koblet sammen, tilhører imidlertid ikke monadisk NP. Eksistensen av et analogt par komplementære problemer, hvorav bare ett har en eksistensiell andreordens formel (uten begrensning til monadiske formler) tilsvarer ulikheten til NP og coNP , et åpent spørsmål i beregningskompleksitet.
Når vi derimot ønsker å kontrollere om en boolsk MSO -formel er tilfredsstilt av et inngitt endelig tre , kan dette problemet løses i lineær tid i treet, ved å oversette den boolske MSO -formelen til en treautomat og evaluere automat på treet . Når det gjelder spørringen, er imidlertid kompleksiteten til denne prosessen generelt ikke -elementær . Takket være Courcelles teorem kan vi også evaluere en boolsk MSO -formel i lineær tid på en inndatagraf hvis trebredden på grafen er begrenset av en konstant.
For MSO -formler som har ledige variabler , når inndataene er et tre eller har begrenset trebredde, er det effektive tellingsalgoritmer for å produsere settet med alle løsningene, noe som sikrer at inngangsdataene er forhåndsbehandlet i lineær tid og at hver løsning deretter blir produsert i en lineær forsinkelse i størrelsen på hver løsning, dvs. konstant forsinkelse i det vanlige tilfellet der alle ledige variabler i spørringen er førsteordens variabler (dvs. de representerer ikke sett). Det er også effektive algoritmer for å telle antall løsninger med MSO-formelen i så fall.
Beslutbarhet og kompleksitet av tilfredshet
Tilfredsstillelsesproblemet for monadisk andreordens logikk kan generelt ikke avgjøres fordi denne logikken faller under førsteordens logikk .
Den monadiske andreordens teori om det uendelige komplette binære treet , kalt S2S, kan avgjøres . Som en konsekvens av dette resultatet kan følgende teorier avgjøres:
- Den monadiske andreordens teori om trær.
- Den monadiske andreordens teorien om under etterfølger (S1S).
- wS2S og wS1S, som begrenser kvantifisering til begrensede delmengder (svak monadisk andreordens logikk). Vær oppmerksom på at for binære tall (representert med delsett), er tillegg definert selv i wS1S.
For hver av disse teoriene (S2S, S1S, wS2S, wS1S) er kompleksiteten i beslutningsproblemet ikke -elementær .
Bruk av MSOs tilfredsheten på trær i verifikasjon
Monadisk andreordens logikk for trær har applikasjoner innen programvareverifisering og, mer generelt, formell verifikasjon takket være dens avgjørbarhet og betydelige uttrykkskraft. Beslutningsprosedyrer for tilfredshet er implementert. Slike prosedyrer ble brukt for å bevise egenskapene til programmer som manipulerer koblede datastrukturer, som en form for Shape -analyse så vel som for symbolsk resonnement i maskinvareverifisering.
Referanser
 |
Denne logikkrelaterte artikkelen er en stub . Du kan hjelpe Wikipedia ved å utvide den . |
