Variabelsplitting: konsistens og kompleksitet
Roger Antonsen
Konteksten for dette er fri-variabel kalkyler for beviss?k,
dvs. sekventkalkyler, tabl?metoder og matrisemetoder hvor man for
universelt kvantifiserte formler setter inn frie variable i stedet for
vilk?rlige termer (som er det vanlige). Det kreves generelt for
konsistensen av slike kalkyler at variable m? instansieres p? en
*rigid* m?te; det vil si at alle ulike forekomster av en gitt variabel
m? erstattes med *samme* term. Dette kravet gj?r at slike metoder er
mindre fleksible og effektive enn n?dvendig, for man har tilfeller der
ulike forekomster av en gitt variabel (i forskjellige grener av en
utledning) er, logisk sett, *uavhengige* av hverandre.
Variabelsplitting er en teknikk som gir betingelser for n?r slike variabelforekomster er uavhengige av hverandre eller ikke, noe som muliggj?r at uavhengige forekomster *ikke* trenger ? instansieres med samme term. Dette gj?res ved ? sette navn p? grener og variable, samt analysere avhengighetsforholdet mellom beta-regler (regler som forgrener) og gamma-regler (regler som setter inn frie variable). Jeg har nylig klart ? vise at man ved hjelp av variabelsplitting kan oppn? en eksponensiell forbedring mph. bevislengde i forhold til kalkyler uten variabelsplitting. Det er fortsatt et ?pent problem om det ogs? er mulig ? oppn? en ikke-element?r forbedring.
Jeg vil gi tilstrekklig bakgrunnsmateriale om fri-variabel kalkyler til at det meste vil v?re forst?elig for de som kjenner litt til sekventkalkyler (à la Gentzen), tabl?metoder (à la Beth/Smullyan/Fitting) eller falsifikasjonstr?r (à la Jervell). Deretter vil jeg definere en sekventkalkyle for f?rste-ordens logikk med variabelsplitting og (om tiden strekker til): (1) Gi eksempler som viser hva dette er bra for. (2) Skissere beviset for at systemet er konsistent. (3) Vise at systemet gir en eksponensiell forbedring mhp. bevislengde for en bestemt klasse formler.