A Strategy Language for Controlled Proof Search

Technische Samenvatting: Een Strategie-taal voor Gecontroleerde Bewijszoeking

Probleemstelling
In de automatische redenering garandeert de statische volledigheid van een logisch calculus (het bestaan van een bewijs voor elke stelling) niet de dynamische volledigheid van een bewijzer (het vermogen om dat bewijs daadwerkelijk te vinden). In semi-beslisbare logica's kunnen inferentieregels oneindig veel opvolgers genereren. Als een bewijszoekstrategie een oneerlijke exploratie hanteert — zoals een naïeve depth-first benadering die een specifieke tak onbeperkt prioriteit geeft — kan zij relevante inferenties voor altijd uitstellen, waardoor zij geldige bewijzen niet ontdekt, zelfs wanneer deze wel bestaan. Dit probleem is bijzonder acuut in frameworks zoals Pgeon, die inferentieregels scheiden van bewijszoekstrategieën, aangezien het ontwerp van het exploratiebeleid een kritieke determinant van succes is.

Methodologie
Het artikel introduceert een formele strategie-taal voor Pgeon, een meta-bewijzer-framework dat declaratieve specificaties van logische calculus compileert naar uitvoerbare bewijzers. De kern van de methodologische verschuiving is het modelleren van bewijszoeking niet als een relatie tussen toestanden, maar als de enumeratie van bewijsstoestanden via streams.

1. Formele Semantiek: Een bewijstoestand ($\Sigma$) wordt behandeld als een gedeeltelijk geconstrueerde bewijsstap. Een strategie wordt gedefinieerd als een functie $s: \Sigma \to \text{Str}(\Sigma)$, die een toestand mapt naar een stream (eindig of oneindig) van opvolgerstoestanden. Dit maakt non-determinisme expliciet:

   • Een lege stream vertegenwoordigt falen.
   • Een singleton stream vertegenwoordigt deterministisch succes.
   • Een stream met meerdere elementen vertegenwoordigt non-deterministische vertakking.
   • Oneindige streams vertegenwoordigen regels die onbegrensd veel opvolgers kunnen genereren.

2. Combinatoren: De taal biedt een set operatoren om deze strategieën te componeren, waarbij onderscheid wordt gemaakt tussen bevooroordeelde (depth-first) en eerlijke (interleaved) exploratie:

   • Sequentiële Compositie ($;$): Past één strategie toe op de resultaten van een andere.
   • Links-gebiaseerde Keuze ($\parallel$): Probeert de eerste strategie; als deze faalt (lege stream), valt zij terug op de tweede.
   • Eerlijke Sequentiële Compositie ($\&;$): Interleaft de resultaten van sequentiële toepassingen met behulp van diagonalisatie ($\triangle$), wat garandeert dat als een resultaat in eindige stappen bereikbaar is, het uiteindelijk wordt verkend.
   • Eerlijke Keuze ($\&|$): Interleaft de resultaten van twee alternatieve strategieën op een eerlijke wijze.
   • Repetitie ($*$): Gedefinieerd als een kleinste fixpunt met behulp van eerlijke sequentiële compositie ($\mu X. \text{id} \&; (s \&; X)$), wat ervoor zorgt dat alle eindige iteratiediepten worden verkend in plaats van strikt depth-first te procederen.

3. Primitieve Operaties: De taal bevat primitieve regels ($r$) en een exhaustieve toepassing-operator ($r!$) die een regel toepast op alle toelaatbare matches in een toestand.

Kernbijdragen

• Compositionele Stream-Semantiek: Het artikel biedt een compositionele algebra voor strategie-combinatoren waarbij de zoekruimte wordt gereïficeerd als een first-class object (een stream). Dit maakt het mogelijk om te redeneren over eerlijkheid en enumeratie onafhankelijk van implementatiedetails zoals stack-discipline of continuaties.
• Eerlijkheidsmechanismen: Door diagonalisatie-gebaseerde interleaving-operatoren ($\&;$ en $\&|$) te introduceren, adresseert het framework het "starvation"-probleem waarbij oneindige takken de ontdekking van eindige bewijzen verhinderen.
• Formele Strategie-taal voor Pgeon: Het werk formaliseert het strategie-component van het Pgeon-framework, waarbij de control flow van de bewijszoeking wordt geabstraheerd naar een declaratieve taal.

Resultaten en Casestudy's
Het artikel demonstreert de expressiviteit en effectiviteit van de aanpak via twee casestudy's:

1. Eerste-orde Logica (LK): De auteurs adresseren de interactie tussen afsluiting (unificatie) en regel-verzadiging. Een naïeve strategie van herhaalde regeltoepassing faalt vaak bij het vinden van bewijzen omdat zij zich te vroeg vastlegt op specifieke instantiaties. De voorgestelde strategie, $(\odot^* \&; (\alpha \parallel \delta \parallel \beta \parallel \gamma!)^*)^*$, gebruikt eerlijke compositie om pogingen tot afsluiting te interleaven met regel-verzadiging. Dit zorgt ervoor dat verschillende unificatie-keuzes over alle zoekdiepten heen worden verkend, wat voorkomt dat het systeem vastloopt in oneindige instantiatie-loops terwijl een afsluitende afleiding wordt gemist.

2. Modale Logica (S4): In S4 is de non-deterministische regel $\theta$ (willekeurige verwijdering van formules) noodzakelijk om de toepassing van de modale regel S4 mogelijk te maken, maar brengt het risico met zich mee dat formules die nodig zijn voor afsluiting worden weggegooid. Een ongecontroleerd gebruik van $\theta$ leidt tot doodlopende paden. De auteurs stellen een gecombineerde strategie voor, $\theta^* \&; \text{S4}$, die alle manieren van het verwijderen van formules verkent om S4-toepassingen eerlijk mogelijk te maken. Dit wordt geïntegreerd in een grotere strategie $((\alpha \parallel \beta \parallel T)^*; (\theta^* \&; \text{S4}))^*$, wat garandeert dat als een succesvolle toepassing van S4 een specifieke subset van verwijderde formules vereist, die configuratie uiteindelijk wordt bereikt zonder starvation.

Betekenis
Het artikel beweert dat deze aanpak een principieel en modulair fundament biedt voor het specificeren en analyseren van bewijszoekprocedures. Door inferentieregels te scheiden van zoekstrategieën en een formele taal met compositionele semantiek te bieden, stelt het framework de systematische exploratie van zoekruimtes in semi-beslisbare logica's mogelijk. Het toont aan dat dynamische volledigheid kan worden bereikt, zelfs wanneer naïeve depth-first strategieën falen, door eerlijkheid expliciet te beheren via stream-interleaving. Het werk maakt het mogelijk om over bewijszoekprocedures te redeneren op een abstract niveau, onafhankelijk van de specifieke implementatie van de bewijzer.