Computing Witnesses Using the SCAN Algorithm

1. Probleemstelling

Het artikel behandelt kwantoreneliminatie van de tweede orde (SOQE), het probleem om een logisch equivalent eerste-ordeformule $\psi$ te vinden voor een gegeven tweede-ordeformule $\exists X \phi$ (waarbij $\phi$ eerste-orde is). Hoewel SOQE in het algemeen onbeslisbaar is, bestaan er praktische algoritmen voor specifieke subclasses.

De auteurs introduceren een generaler probleem genaamd Gedwongen kwantoreneliminatie van de tweede orde (WSOQE). In plaats van alleen een equivalent eerste-ordeformule te vinden, is het doel om een getuige te vinden: een tuple van eerste-ordepredicaten $\alpha$ zodanig dat:
$$\exists X \phi \equiv \phi[X \leftarrow \alpha]$$
Dit betekent dat de tweede-ordeformule equivalent is aan de eerste-ordeformule die wordt verkregen door de predikaatvariabelen $X$ te substitueren met specifieke eerste-ordefinities $\alpha$.

Betekenis van WSOQE:

• Het overbrugt de kloof tussen SOQE en Formulevergelijkingen (FEQ) (het vinden van $\alpha$ zodanig dat $\models \phi[X \leftarrow \alpha]$).
• Het is cruciaal voor toepassingen in kennisrepresentatie (vergeten/projectie), modale correspondentietheorie en programmacorrectheid (het vinden van lusinvarianten).
• In tegenstelling tot standaard SOQE, dat alleen het resultaat produceert, biedt WSOQE de definitie van de geëlimineerde predicaten, waardoor de structuur van de kennisbasis behouden blijft.

2. Methodologie: Het WSCAN-algoritme

De auteurs stellen WSCAN voor, een extensie van het bestaande SCAN-algoritme (een op saturatie gebaseerd bewijssysteem voor SOQE). De kernmethodologie omvat twee hoofdfasen:

A. De SCAN-afleiding

Het algoritme werkt op clausulverzamelingen. Het transformeert de invoerformule naar clausulnormaalvorm en voert een saturatieproces uit met behulp van een specifiek inferentiecalculus $\mathcal{I}$:

1. Constraint-resolutie & Factoring: In plaats van standaard unificatie introduceren deze regels ongelijkheidsconstraints (bijv. $t \not\simeq t'$) tussen termen.
2. Constraint-eliminatie: Unificeert termen om constraints te verwijderen.
3. Verwijderingsregels:
   • Uitgebreide zuiverheidsverwijdering: Verwijdert clausules die $X$ bevatten als $X$ alleen met één polariteit voorkomt (allemaal positief of allemaal negatief).
   • Gezuiverde clausuleverwijdering: Verwijdert een clausule $P$ die $X$ bevat als "voldoende veel" inferenties zijn uitgevoerd zodat de resterende clausulverzameling logisch de resolutie-sluiting van $P$ impliceert. Dit wordt geformaliseerd via een forward redundancy-criterium dat variabele-eliminatie en subsumptie omvat.

Het proces gaat door totdat alle $X$-literalen zijn geëlimineerd, wat resulteert in een eerste-orde clausulverzameling $N^*$ die equivalent is aan $\exists X N$.

B. Getuigconstructie (Bottom-Up)

De nieuwe bijdrage is de extractie van een getuige $\sigma$ uit de afleidingsgeschiedenis. Het algoritme construeert de getuige achterwaarts (van de eindtoestand naar de begintoestand):

1. Basisgeval: Als de eindclausulverzameling $N_m$ geen $X$ bevat, is de identiteitssubstitutie een getuige.
2. Inductiestap: Voor elke afleidingsstap $S_i$ die $N_{i-1}$ transformeert naar $N_i$, berekent het algoritme een substitutie $\tau_{S_i}$ zodanig dat als $\sigma_i$ een getuige is voor $N_i$, dan $\tau_{S_i}\sigma_i$ een getuige is voor $N_{i-1}$.
   • Voor standaard inferentiestappen (Resolutie, Factoring, etc.) is $\tau$ de identiteit.
   • Voor Uitgebreide zuiverheidsverwijdering stelt $\tau$ $X$ in op $\top$ of $\bot$, afhankelijk van de polariteit.
   • Voor Gezuiverde clausuleverwijdering (het complexe geval) construeert het algoritme een getuige op basis van de lokale resolutie-sluiting van de verwijderde clausule.

C. Omgaan met oneindige getuigen

De resolutie-sluiting die wordt gebruikt voor gezuiverde clausules kan oneindig zijn, wat leidt tot oneindige getuigen (uitgedrukt als oneindige conjuncties). Het artikel introduceert twee oplossingen:

1. Fixpuntgetuigen: De oneindige getuige wordt uitgedrukt als een grootste fixpunt ($gfp$) in fixpuntlogica. Dit biedt een eindige representatie van de potentieel oneindige definitie.
2. Eerste-orde getuigen (Acyclische voorwaarde): De auteurs definiëren een voorwaarde genaamd $k$-acyclisch gezuiverd. Als de "gezuiverde subsumptiegrafiek" geassocieerd met een verwijderingsstap acyclisch is, kan de getuige worden berekend als een eindige, eerste-orde predikaat met behulp van een gebonden iteratie van de resolutie-sluiting.

3. Belangrijkste bijdragen

1. WSCAN-algoritme: Een complete methode om getuigen te berekenen voor SOQE op clausulverzamelingen, als extensie van het SCAN-algoritme.
2. Correctheidsbewijzen:
   • Bewijs dat de geconstrueerde substitutie $\sigma$ een geldige getuige is ($\exists X N \equiv N\sigma$).
   • Een nieuw correctheidsbewijs voor het originele SCAN-algoritme, afgeleid uit de logica van de getuigconstructie.
3. Garantie voor eerste-orde getuigen: Identificatie van de voorwaarde acyclische zuivering, die garandeert dat de resulterende getuige een eerste-ordeformule is (waarmee oneindige of fixpuntexpressies worden vermeden).
4. Extensie van Ackermann's Lemma: De auteurs bewijzen dat hun methode Ackermann's Lemma (een klassieke methode voor SOQE) omvat en uitbreidt naar gevallen waarin het predikaat met gemengde polariteit voorkomt.
5. Omgaan met achtergrondtheorieën: De methode is uitgebreid om redenering over gelijkheid (via paramodulatie) en eerste-orde achtergrondtheorieën te behandelen, waardoor het in staat is om problemen met grafbereikbaarheid en andere constrained Horn-clausuleproblemen op te lossen.
6. Prototype-implementatie: Een prototype-implementatie in het GAPT-softwarepakket (General Architecture for Proof Theory, versie 2.19.0).

4. Resultaten en Evaluatie

• Implementatie: Het prototype is getest op 44 voorbeelden (uit de literatuur en zelfgemaakt).
• Prestaties:
  • SCAN-afleidingen werden gevonden voor 90,9% van de voorbeelden (40/44) binnen een time-out van 10 seconden.
  • De berekening van de getuige was extreem snel (gemiddeld 0,619 ms) in vergelijking met het vinden van de afleiding (gemiddeld 375 ms).
  • De grootte van de getuigen was over het algemeen klein (gemiddeld 6,9 symbolen).
• Mogelijkheden: Het systeem slaagde erin eerste-orde getuigen te berekenen voor afleidingen die eerder oneindige getuigen opleverden of fixpuntlogica vereisten, specifiek in gevallen die betrekking hadden op acyclische zuiveringsgrafieken.
• Beperkingen:
  • De methode vereist dat de invoer een clausulverzameling is (universeel gekwantificeerde domeinvariabelen).
  • Het kan geen gevallen afhandelen waar Skolemisatie vereist is en niet ongedaan kan worden gemaakt (bijv. $\exists X \exists u \exists v (X(u) \land \neg X(v))$), aangezien de resulterende getuige Skolem-constanten zou bevatten die niet in de oorspronkelijke taal aanwezig zijn.
  • De zoekruimte voor afleidingen kan groot zijn; de huidige implementatie gebruikt backtracking maar is niet geoptimaliseerd voor enorme clausulverzamelingen.

5. Betekenis

Dit werk is significant omdat het het SCAN-algoritme transformeert van een tool die kwantoren enkel elimineert naar een tool die de definities van de geëlimineerde predicaten synthetiseert.

• Theoretische brug: Het verenigt de velden van kwantoreneliminatie van de tweede orde (SOQE) en formulevergelijkingen (FEQ), en laat zien dat ze twee kanten van dezelfde medaille zijn.
• Praktische toepassing: Door expliciete eerste-ordefinities (getuigen) te bieden, is de methode direct toepasbaar op:
  • Kennisrepresentatie: Het creëren van uniforme interpolanten en het vergeten van predicaten terwijl de logische structuur behouden blijft.
  • Verificatie: Het automatisch genereren van lusinvarianten voor programmacorrectheid (het oplossen van constrained Horn-clausules).
  • Modale logica: Het berekenen van correspondentieaxioma's voor modale logica's.

Het artikel stelt vast dat voor een brede klasse van afleidingen (die met acyclische zuiveringsgrafieken) het complexe tweede-ordeprobleem kan worden gereduceerd tot het vinden van een eindige, eerste-orde getuige, wat een krachtig nieuw hulpmiddel biedt voor geautomatiseerd redeneren.