Vuonna matemaattinen logiikka , The resoluutio sääntö tai periaate päätöslauselma of Robinson on sääntö päättelyn logiikkaa , että yleistää modus ponens . Tätä sääntöä käytetään pääasiassa automaattisissa todistusjärjestelmissä , se on loogisen ohjelmointikielen Prolog perusta .
Modus ponens -sääntö kirjoitetaan ja luetaan: p: stä ja "p merkitsee q: ta" johdin q: n. Voimme kirjoittaa implikaation "p merkitsee q" uudestaan kuten "p on väärä tai q on tosi". Täten kirjoitetaan modus ponens -sääntö .
Ratkaisusääntö, se yleistää modus ponens -säännön, koska sitä sovelletaan kaikkiin lausekkeisiin . Lauseke on kaava, joka on literaalien (atomi- tai atomilause, jota edeltää negaatio) disjunktio ("tai"). Esimerkiksi on lause, jossa on kaksi literaalia ("ei p" ja "q"). Siten ehdotuslogiikassa päätöslauselmasääntö kirjoitetaan:
Toisin sanoen, kun otetaan huomioon kaksi lauseketta ja , päätämme . Johdettu kaava, ts kutsutaan ratkaisija on ja . Tietenkin sääntösovellus annetaan permutaatiolle lähellä literaaleja.
Esimerkiksi :
missä merkitsee ristiriitaa (tyhjä lauseke).
In predikaattilogiikalla atomi kaavat ovat muotoa jossa on predikaatti symboli ja ovat termejä, jotka koostuvat vakioita, muuttujia ja toiminta symboleja. Preesikaatti-logiikan resoluutiosääntö on samanlainen kuin propositio-logiikan resoluutiosääntö, mutta kahden lausekkeen jakamat atomikaavat eivät saa olla identtisiä, mutta yksilöitäviä . Kaksi atomikaavaa ei ole määritettävissä, jos muuttujat korvataan termeillä, jotka tekevät molemmista kaavoista identtiset (katso yhtenäistäminen ). Esimerkiksi :
on resoluutiosäännön soveltaminen predikaattilogiikassa. Se lukee: "P (a)": sta ja "(kaikille x: lle, ei P (x) tai Q (x): lle", päätän "Q (a)". Täällä atomikaava ja atomikaava ovat yksilöitävissä substituutiolla . Yleisemmin predikaattilogiikan ratkaisemista koskeva sääntö on:
missä on atomikaavojen pääasiallinen yhdistäjä ja .
Resoluutio voidaan suorittaa kahdella litraalilla, jos ne liittyvät identtisiin atomikaavoihin tai unifioimattomiin kaavoihin .
Esimerkiksi atomikaavat
ja jos a ja c ovat vakioita,
ovat korvaamattomia . Toisaalta
ja jos a, b ja c ovat vakioita,
ei voida yhtenäistää, koska vakioita ei voida korvata.
Korvaus antaa mahdollisuuden käyttää päätöslauselmaa Q, välillä ja , joka tuottaa
Korvaus mahdollistaa resoluution soveltamisen P: hen, välillä ja tuottaa
Yleensä resoluution periaatetta käytetään todisteiden suorittamiseen kumoamalla. Sen osoittamiseksi, että kaava on kaavojen looginen seuraus, osoitamme, että joukko on epäjohdonmukainen.
Käytännössä on välttämätöntä aloittaa asettamalla kaikki kaavat lausemuotoon, sillä ne on laitettava esiliitteisiin (kaikki kvantitorit alussa) ja sitten skolemisoitava ne .
Osoittaaksemme, että joukko lausekkeita on epäjohdonmukainen, meidän on onnistuttava luomaan tyhjä lauseke soveltamalla päätöslauselmaa niin monta kertaa kuin tarpeen.
Haluamme osoittaa, että kolme kaavaa
tulosta kaava .
Ensimmäinen kaava vastaa kahta lausetta ja muodostaa siten ne
Toinen kaava antaa välittömästi lausekkeen
ja kolmas
.
Halutun seurauksen kieltäminen antaa
Erottelussa on ja jossa yhden tuottaa
Päätöslauselmalla de ja tuotamme
Lopuksi ja anna tyhjä lauseke.
Ratkaisun periaate on täydellinen, jos harkittu lausekeryhmä on epäjohdonmukainen, onnistumme aina luomaan tyhjän lausekkeen. Toisaalta, koska johdonmukaisuusongelmaa (tyydyttävyyttä) ei voida ratkaista predikaattilogiikassa, ei ole olemassa menetelmää kertoa meille, mitkä päätöslauselmat on suoritettava ja missä järjestyksessä päästään tyhjään lausekkeeseen.
Voidaan helposti löytää esimerkkejä, joissa "uppoaa" äärettömän määrän lausekkeita tuottamatta koskaan tyhjää lauseketta, kun taas sen olisi saanut aikaan tekemällä oikeat valinnat.
Prosessin ohjaamiseksi on kehitetty erilaisia strategioita. Prolog- järjestelmä perustuu esimerkiksi lauseiden kirjoittamisjärjestykseen ja lauseissa olevien literaalien järjestykseen. Muut järjestelmät, kuten CyC , käyttävät rajausstrategiaa (kulutetuista resursseista riippuen) loputtomien haarojen syntymisen välttämiseksi.
Haken osoitti, että n sukalla varustettujen laatikoiden periaatteen kumottaminen (englanniksi tämä on kyyhkysreiän periaate ) on vähintään 2 n / 10 pituinen .
Harjoituksia resoluutiosäännön manipuloimiseksi , joka on kehitetty ENS Rennesissä