Redenen voor succes bij het bewijzen van geautomatiseerde stellingen

Het lijkt mij (althans volgens boeken en artikelen over het onderwerp dat ik lees) dat het gebied van geautomatiseerde stellingneming een soort van kunst of experimentele empirische techniek is van het combineren van verschillende benaderingen, maar geen wetenschap die probeert uit te leggen WAAROM zijn methoden werk in verschillende situaties en om klassen van situaties te vinden waarvoor ze werken. Of misschien ben ik niet op de hoogte van sommige resultaten of het probleem is te moeilijk.

Is het op een rigoureuze manier opgehelderd waarom bijvoorbeeld de resolutie van Robinson beter werkt dan Gilmore's verzadiging? (intuïtieve reden is natuurlijk dat de meeste algemene spreider al informatie over oneindig veel termen uit het universum van Herbrand bevat, maar het is alleen maar intuïtie, geen concrete reden, en ook dat je niet weet wanneer je moet stoppen met zoeken naar een bewijs van een formule A in het geval A en niet (A) zijn beide onbewijsbaar is geen rigoureuze verklaring van onbeslisbaarheid van eerste orde logica).

Ik heb zelfs een artikel gezien dat er gevallen zijn waarbij het algoritme van het Londense museum (brute force search, in essentie) beter presteert dan resolutie!

Misschien heeft iemand enkele grote klassen formules gevonden waarop de resolutie goed werkt?
Misschien een probabilistische analyse van testmethoden?

Bij voorbaat dank.

11

3 antwoord

Misschien ben je wel geïnteresseerd in het prachtige kleine boek `` The Efficiency of Theorem Proving Strategies: A Comparative and Asymptotic Analysis '' van David A. Plaisted en Yunshan Zhu. Ik heb de 2e editie die paperback is en vrij goedkoop was. Ik plak de (nauwkeurige) blurb:

`` Dit boek is uniek omdat het asymptotische grenzen geeft aan de groottes van de zoekruimten die worden gegenereerd door veelvoorkomende strategieën om stellingen te bewijzen. Op deze manier kan iemand een theoretisch inzicht verwerven in de efficiëntie van vele verschillende stellingtestmethoden. Dit is een fundamenteel nieuw instrument in de vergelijkende studie van theoretische strategieën. ''

Nu vanuit een kritisch perspectief: er bestaat geen twijfel over dat geavanceerde asymptotische analyses zoals deze erg belangrijk zijn (en voor mij zijn de onderliggende ideeën mooi en diepgaand). Maar vanuit het perspectief van de beoefenaar die feitelijk geautomatiseerde stellingen gebruikt, zijn deze analyses vaak te grof om praktisch bruikbaar te zijn. Een gerelateerd verschijnsel doet zich voor bij beslissingsprocedures voor echte gesloten velden. Sinds Davenport-Heinz is bekend dat algemene kwantoreliminatie over echte gesloten velden inherent dubbel exponentieel w.r.t. is. het aantal variabelen in een ingevoerde Tarski-formule. Een volledige RCF kwantoreliminatiemethode met deze dubbel exponentiële complexiteit is CAD van Collins. Maar velen (Renegar, Grigor'ev/Vorobjov, Canny, ...) hebben enkel exponentiële procedures gegeven voor het puur existentiële fragment. Hoon Hong heeft een interessante analyse van deze situatie uitgevoerd. De asymptotische complexiteiten van drie beslissingsprocedures die door Hong worden beschouwd in `` Vergelijking van verschillende beslissingsalgoritmen voor de existentiële theorie van de reals '' zijn als volgt:

(Laat $ n $ het aantal variabelen zijn, $ m $ het aantal polynomen, $ d $ hun totale graad en $ L $ de bitbreedte van de coëfficiënten)

CAD: $ L ^ 3 (md) ^ {2 ^ {O (n)}} $

Grigor'ev/Vorobjov: $ L (md) ^ {n ^ 2} $

Renegar: $ L (log L) (logboeklog L) (md) ^ {O (n)} $

Dus voor puur existentiële formules zou men verwachten dat de G/V- en R-algoritmen CAD veel beter presteren. Maar in de praktijk is dit niet het geval. In het aangehaalde artikel geeft Hong redenen waarom, met als belangrijkste punt dat de asymptotische analyses enorme loerende constante factoren negeren die de enkelvoudige exponentiële algoritmen in de praktijk niet toepasbaar maken. In de voorbeelden die hij geeft ($ n = m = d = L = 2 $), zou CAD een invoerzin in een fractie van een seconde beslissen, terwijl de enkelvoudig exponentiële procedures meer dan een miljoen jaar zouden duren. De moraal lijkt een herinnering te zijn aan het feit dat een complexiteitstheoretische versnelling w.r.t. voldoende grote invoerproblemen moeten niet worden verward met een snellere w.r.t. praktische invoerproblemen.

In elk geval denk ik dat de situatie met asymptotische analyses in geautomatiseerde stelling bewijzen vergelijkbaar is. Dergelijke analyses zijn belangrijke theoretische vorderingen, maar zijn vaak te grof om de dagelijkse beoefenaar te beïnvloeden die in de praktijk geautomatiseerde stellingstestinstrumenten gebruikt.

(* Men moet vermelden Galen Huntington's mooie 2008 proefschrift in Berkeley onder Branden Fitelson waarin hij laat zien dat Canny's alleen-exponentiële procedure kan worden gemaakt om te werken aan de kleine voorbeelden beschouwd door Hong in de bovengenoemde paper. Dit is aanzienlijke vooruitgang. vergelijkt echter niet de praktijk met het dubbel-exponentiële CAD.)

11
toegevoegd
Graag gedaan. Ik hoop dat het helpt!
toegevoegd de auteur sheats, de bron

Een manier om naar deze vraag te kijken is werk in terminatieanalyse van logica-programma's (googelen van "beëindigingsanalyse van logische programma's" is geen slechte manier om een ​​deel van het relevante onderzoek te vinden.)

Bijvoorbeeld, als de regels waar ik naar kijk er zo uitzien:

lt(zero,succ(Y)).  
lt(succ(X),succ(Y)) <= lt(X,Y).

Ik weet dat die resolutie zal slagen of uiteindelijk falen voor elke vraag? Lt (n, X) waarbij n een grondterm is, omdat elke subgoal die ontstaat, een kleiner eerste argument zal hebben dan het subdoel dat tot zijn generatie heeft geleid. Aan de andere kant, als de regels die ik bekijk er zo uitzien:

path(X,Z) <= path(X,Y), path(Y,Z).

Ik weet dat, gegeven een n pad (,) feiten, ik hoogstens een eindig aantal andere pad (,) feiten kan afleiden (in de volgorde n 2 ), die ervoor zorgt dat de verzadiging wordt beëindigd (ervan uitgaande dat wat ik zie als verzadiging, is wat u ziet als de verzadiging van Gilmore).

(Een dieper onderzoek van waar het verschil tussen deze methoden vandaan komt, is te vinden in Chaudhuri, Pfenning en Price, Een logische karakterisering van vooruit en achteruit ketenen in de inverse methode . Journal of Automated Reasoning, 40 (2-3), pp. 133-177. 2008., maar het antwoord hierboven leek relevanter voor de vraag.)

2
toegevoegd
Dank je. Ik heb wat artikelen over dat onderwerp bekeken. Maar nog steeds als de auteurs zeggen dat één methode "vaker" eindigt dan andere, zijn ze waarschijnlijk afhankelijk van enkele intuïtieve redenen en experimenten. Het lijkt erop dat het probleem van het vergelijken (zelfs probabilistisch), bijvoorbeeld resolutie en brute kracht, nu te moeilijk is.
toegevoegd de auteur Joe, de bron

Sorry, ik kan om wat voor reden dan ook geen reactie op uw vraag plaatsen (misschien heb ik meer reputatie nodig), dus ik zal het u hier gewoon vragen:

  • Wat is de verzadiging van Gilmore precies? Nog nooit van gehoord.
  • Over welk papier had je het? (Over waar de brute kracht beter presteert dan resolutie.)

Meer over het onderwerp van de vraag:

Ik weet niet zeker of je vraag (ik beperk het hier :): 'hoe goed doet resolutie het doet' veel zin heeft. Oplossing is slechts een formele methode om elke 'meest direct volgende'-clausule uit een reeks clausules te krijgen. Dat is een resolutiestap.

Er wordt niets gespecificeerd over hoe u nu naar een bewijs zoekt via een oplossing. Er zijn tientallen manieren om dat te doen. Je kunt gewoon brute kracht doen zonder enige intelligentie, of je kunt het doen via een soort heuristiek. Of in logica programmeren wanneer je vraagt ​​of een clausule Q waar is, ontken je Q, voeg je het toe aan de reeks andere gegeven clausules en probeer je de lege clausule op te lossen. Wanneer je je beperkt tot Horn-clausules, kun je een SLD-resolutie doen die veel gerichter is. Nog steeds, ook met SLD-resolutie, wordt het opengelaten voor de tover welke clausule en welk letterlijke om te kiezen.

D.w.z. in ieder geval blijft het een beetje zoeken waar je mee bezig bent. Prolog maakt bijvoorbeeld gebruik van Diepte-eerste zoekopdracht maar sommige anderen gebruiken iteratief verdiepen zoeken. De volgorde wordt meestal bepaald door de volgorde van de definities (in uw fact-bestand), maar u kunt ook proberen hier wat heuristiek toe te passen.

Deze heuristiek of in het algemeen de volgorde van hoe u de resolutie doet, bepaalt de prestaties van uw prover.

0
toegevoegd
Gilmore's verzadigingsmethode bestaat uit 1) substitutievariabelen door grondtermen (saturatie) en 2) controle op onbevredelijkheid van de verkregen set gesloten clausules (bijvoorbeeld met behulp van DPLL). De papieren zijn van R. Statman: 1. De predikaatrekening is geen Kalmar-elementaire versnelling van de vergelijkingsberekening.- Preprint, Cambridge, 1975. 2. Grenzen voor proof-search en versnelling in de predikaatrekening, - Ann. Wiskunde. Logica, 1978, 15, № 3, p. 225-287.
toegevoegd de auteur Joe, de bron
Zie ook de paper van V. P. Orevkov "Het algoritme van het Britse museum kan effectiever zijn dan de resolutie" (in het Russisch). "Resolutie is slechts een formele methode om een ​​'meest direct volgende' clausule uit een reeks clausules te halen". Natuurlijk, en ik vraag om rigoureus te doen (althans een probabilistische) vergelijking van de resolutie met andere methoden.
toegevoegd de auteur Joe, de bron