Automatiserad teorembevisande

Automatiserad teorembevisning (även känd som ATP eller automatiserad deduktion ) är ett underområde av automatiserat resonemang och matematisk logik som handlar om att bevisa matematiska satser med datorprogram . Automatiserade resonemang över matematiska bevis var en stor drivkraft för utvecklingen av datavetenskap .

Logiska grunder

Medan rötterna till formaliserad logik går tillbaka till Aristoteles , såg man i slutet av 1800-talet och början av 1900-talet utvecklingen av modern logik och formaliserad matematik. Frege 's Begriffsschrift (1879) introducerade både en komplett propositionskalkyl och vad som i huvudsak är modern predikatlogik . Hans grunder för aritmetik , publicerad 1884, uttryckte (delar av) matematik i formell logik. Detta tillvägagångssätt fortsattes av Russell och Whitehead i deras inflytelserika Principia Mathematica , först publicerad 1910–1913, och med en reviderad andra upplaga 1927. Russell och Whitehead trodde att de kunde härleda all matematisk sanning genom att använda axiom och slutledningsregler för formell logik, i princip öppna processen för automatisering. År 1920 Thoralf Skolem ett tidigare resultat av Leopold Löwenheim , vilket ledde till Löwenheim-Skolem-satsen och, 1930, till föreställningen om ett Herbrand-universum och en Herbrand-tolkning som möjliggjorde (o)tillfredsställelse av första ordningens formler (och därmed giltigheten av ett teorem) för att reduceras till (potentiellt oändligt många ) propositionella tillfredsställbarhetsproblem.

1929 visade Mojżesz Presburger att teorin om naturliga tal med addition och likhet (nu kallad Presburger-arithmetik till hans ära) är avgörbar och gav en algoritm som kunde avgöra om en given mening i språket var sann eller falsk. Kort efter detta positiva resultat publicerade Kurt Gödel emellertid On Formally Undecidable Propositions of Principia Mathematica and Related Systems ( 1931), och visade att det i alla tillräckligt starka axiomatiska system finns sanna påståenden som inte kan bevisas i systemet. Detta ämne vidareutvecklades på 1930-talet av Alonzo Church och Alan Turing , som å ena sidan gav två oberoende men likvärdiga definitioner av beräkningsbarhet , och å andra sidan gav konkreta exempel på oavgjorda frågor.

Första implementeringar

Strax efter andra världskriget blev de första allmänna datorerna tillgängliga. 1954 Martin Davis Presburgers algoritm för en JOHNNIAC vakuumrörsdator vid Institute for Advanced Study i Princeton, New Jersey. Enligt Davis, "Dess stora triumf var att bevisa att summan av två jämna tal är jämn". Mer ambitiös var Logic Theory Machine 1956, ett deduktionssystem för propositionslogiken i Principia Mathematica , utvecklat av Allen Newell , Herbert A. Simon och JC Shaw . Även på en JOHNNIAC, konstruerade Logic Theory Machine bevis från en liten uppsättning propositionella axiom och tre deduktionsregler: modus ponens , (propositionell) variabelsubstitution och ersättning av formler enligt deras definition. Systemet använde heuristisk vägledning och lyckades bevisa 38 av de första 52 satserna i Principia .

Logic Theory Machines "heuristiska" tillvägagångssätt försökte efterlikna mänskliga matematiker, och kunde inte garantera att ett bevis kunde hittas för varje giltig teorem ens i princip. Däremot uppnådde andra, mer systematiska algoritmer, åtminstone teoretiskt, fullständighet för första ordningens logik. Inledande tillvägagångssätt förlitade sig på resultaten från Herbrand och Skolem för att omvandla en första ordningens formel till successivt större uppsättningar av propositionsformler genom att instansiera variabler med termer från Herbrands universum . Propositionsformlerna kunde sedan kontrolleras för otillfredsställelse med hjälp av ett antal metoder. Gilmores program använde konvertering till disjunktiv normalform , en form där tillfredsställelsen av en formel är uppenbar.

Problemets beslutbarhet

Beroende på den bakomliggande logiken varierar problemet med att avgöra en formels giltighet från trivialt till omöjligt. För det frekventa fallet av propositionell logik är problemet avgörbart men co-NP-komplett , och därför tros endast exponentiella tidsalgoritmer existera för allmänna bevisuppgifter. För en första ordningens predikatkalkyl säger Gödels fullständighetssats att satserna (bevisbara påståenden) är exakt de logiskt giltiga välformade formlerna, så identifiering av giltiga formler är rekursivt uppräknad : givet obegränsade resurser kan vilken giltig formel så småningom som helst bevisas. Men ogiltiga formler (de som inte ingår i en given teori) kan inte alltid erkännas.

Ovanstående gäller första ordningens teorier, såsom Peano-aritmetik . Men för en specifik modell som kan beskrivas av en första ordningens teori kan vissa påståenden vara sanna men oavgörbara i teorin som används för att beskriva modellen. Till exempel, genom Gödels ofullständighetsteorem , vet vi att varje teori vars egentliga axiom är sanna för de naturliga talen inte kan bevisa att alla första ordningens påståenden är sanna för de naturliga talen, även om listan över riktiga axiom tillåts vara oändlig uppräknad. Det följer att en automatiserad satsbevisare kommer att misslyckas med att avslutas när den söker efter ett bevis just när det påstående som undersöks är oavgörbart i teorin som används, även om det är sant i modellen av intresse. Trots denna teoretiska gräns kan satsbevisare i praktiken lösa många svåra problem, även i modeller som inte helt beskrivs av någon första ordningens teori (som heltal).

Relaterade problem

Ett enklare, men relaterat, problem är bevisverifiering , där ett befintligt bevis för ett teorem är certifierat giltigt. För detta krävs i allmänhet att varje enskilt bevissteg kan verifieras av en primitiv rekursiv funktion eller program, och därför är problemet alltid avgörbart.

Eftersom bevisen som genereras av automatiserade teorembevisare vanligtvis är mycket stora, är problemet med beviskomprimering avgörande och olika tekniker som syftar till att göra bevisarens utdata mindre, och följaktligen lättare att förstå och kontrollera, har utvecklats.

Korrekturassistenter kräver att en mänsklig användare ger tips till systemet. Beroende på graden av automatisering kan provaren i huvudsak reduceras till en korrekturkontroll, där användaren tillhandahåller beviset på ett formellt sätt, eller så kan betydande bevisuppgifter utföras automatiskt. Interaktiva provare används för en mängd olika uppgifter, men även helautomatiska system har bevisat ett antal intressanta och hårda satser, inklusive åtminstone en som har gäckat mänskliga matematiker under lång tid, nämligen Robbins gissningar . Dessa framgångar är dock sporadiska och arbete med svåra problem kräver vanligtvis en skicklig användare.

En annan distinktion görs ibland mellan teorembevisande och andra tekniker, där en process anses vara teorembevisande om den består av ett traditionellt bevis, som börjar med axiom och producerar nya inferenssteg med hjälp av inferensregler. Andra tekniker skulle inkludera modellkontroll , som i det enklaste fallet innebär brute-force-uppräkning av många möjliga tillstånd (även om den faktiska implementeringen av modellcheckers kräver mycket smarthet och inte bara reduceras till brute force).

Det finns hybridsatsbevisande system som använder modellkontroll som en slutledningsregel. Det finns också program som skrevs för att bevisa ett visst teorem, med ett (oftast informellt) bevis på att om programmet slutar med ett visst resultat, så är satsen sann. Ett bra exempel på detta var det maskinstödda beviset för fyrfärgssatsen , som var mycket kontroversiellt som det första påstådda matematiska beviset som var i huvudsak omöjligt att verifiera av människor på grund av den enorma storleken på programmets beräkning (sådana bevis kallas icke -översiktsbara bevis ). Ett annat exempel på ett programassisterat bevis är det som visar att spelet Connect Four alltid kan vinnas av den första spelaren.

Industriell användning

Kommersiell användning av automatiserad teoremprovning är mestadels koncentrerad till konstruktion och verifiering av integrerade kretsar . Sedan Pentium FDIV-felet har de komplicerade flyttalsenheterna hos moderna mikroprocessorer designats med extra noggrannhet. AMD , Intel och andra använder automatiserade teorem för att verifiera att division och andra operationer är korrekt implementerade i deras processorer.

Första ordningens sats bevisar

I slutet av 1960-talet började byråer som finansierade forskning inom automatiserat avdrag betona behovet av praktiska tillämpningar. Ett av de första fruktbara områdena var programverifiering , varvid första ordningens satsbevisare tillämpades på problemet med att verifiera riktigheten av datorprogram på språk som Pascal, Ada, etc. Noterbart bland tidiga programverifieringssystem var Stanford Pascal Verifier utvecklad av David Luckham vid Stanford University . Detta baserades på Stanford Resolution Prover som också utvecklats på Stanford med hjälp av John Alan Robinsons resolutionsprincip . Detta var det första automatiska avdragssystemet som visade en förmåga att lösa matematiska problem som tillkännagavs i Notices of the American Mathematical Society innan lösningarna formellt publicerades. [ citat behövs ]

Första ordningens satsbevisande är ett av de mest mogna underområdena för automatiserad satsbevisande. Logiken är tillräckligt uttrycksfull för att tillåta specifikation av godtyckliga problem, ofta på ett någorlunda naturligt och intuitivt sätt. Å andra sidan är det fortfarande semi-avgörbart, och ett antal sunda och kompletta kalkyler har utvecklats, vilket möjliggör helautomatiska system. Mer uttrycksfull logik, såsom logik av högre ordning , tillåter ett bekvämt uttryck av ett bredare spektrum av problem än första ordningens logik, men teorembevisande för dessa logiker är mindre välutvecklat.

Benchmarks, tävlingar och källor

Kvaliteten på implementerade system har gynnats av att det finns ett stort bibliotek med standardriktmärken - The Thousands of Problems for Theorem Provers (TPTP) Problem Library - samt från CADE ATP System Competition (CASC), en årlig tävling av första -ordningssystem för många viktiga klasser av första ordningens problem.

Några viktiga system (alla har vunnit minst en CASC-tävlingsdivision) listas nedan.

Theorem Prover Museum är ett initiativ för att bevara källorna till teoremprover-systemen för framtida analys, eftersom de är viktiga kulturella/vetenskapliga artefakter. Den har källorna till många av de ovan nämnda systemen.

Populära tekniker

Mjukvarusystem

Se även: Korrekturassistent § Jämförelse , och Kategori:Satsbevisande programvarusystem
Jämförelse
namn Licens typ webb-service Bibliotek Fristående Senaste uppdatering ( format ÅÅÅÅ-mm-dd )
ACL2 3-klausul BSD Nej Nej Ja maj 2019
Prover9/Otter Allmängods Via System på TPTP Ja Nej 2009
Jape GPLv2 Ja Ja Nej 15 maj 2015
PVS GPLv2 Nej Ja Nej 14 januari 2013
Leo II BSD-licens Via System på TPTP Ja Ja 2013
EQP ? Nej Ja Nej maj 2009
LEDSEN GPLv3 Ja Ja Nej 27 augusti 2008
PhoX ? Nej Ja Nej 28 september 2017
KeYmaera GPL Via Java Webstart Ja Ja 11 mars 2015
Gandalf ? Nej Ja Nej 2009
E GPL Via System på TPTP Nej Ja 4 juli 2017
SNARK Mozilla Public License 1.1 Nej Ja Nej 2012
Vampyr Vampyrlicens Via System på TPTP Ja Ja 14 december 2017
Theorem Proving System (TPS) TPS distributionsavtal Nej Ja Nej 4 februari 2012
SPASS FreeBSD-licens Ja Ja Ja november 2005
IsaPlanner GPL Nej Ja Ja 2007
Nyckel GPL Ja Ja Ja 11 oktober 2017
prinsessa lgpl v2.1 Via Java Webstart och System på TPTP Ja Ja 27 januari 2018
iProver GPL Via System på TPTP Nej Ja 2018
Metasats Gratisprogram Nej Nej Ja juli 2022
Z3 Theorem Prover MIT-licens Ja Ja Ja 19 november 2019

Gratis mjukvara

Proprietär programvara

  • Acumen RuleManager (kommersiell produkt)
  • ALLIGATOR (CC BY-NC-SA 2.0 UK)
  • CARINE
  • KIV (fritt tillgänglig som plugin för Eclipse )
  • Prover Plug-In (kommersiellt säker motorprodukt)
  • ProverBox
  • Wolfram Mathematica
  • ResearchCyc
  • Spjuts modulära aritmetiska teoremprovare

Se även

Anteckningar

externa länkar

Hämtad från " https://en.wikipedia.org/w/index.php?title=Automated_theorem_proving&oldid=1136357083 "