Indeksinis daugiasukcedentinis skaičiavimas su apverčiamomis taisyklėmis konstruktyvinei logikai
Paprastai konstruktyvinėje predikatų logikoje taikomas viensukcedentinis šios logikos skaičiavimas Jame nagrinėjami objektai yra tokios sekvencijos: A1,...., An → Θ ((Θ) ∈ ∅, A). Be viensukcedentinio skaičiavimo yra nagrinėjamas daugiasukcedentinis, turintis kai kuriuos privalumus pirmojo atžvilgiu. Daugiasukcedentinis (kaip ir veinsukcedentinis) skaičiavimas turi neapverčiamų taisyklių, kurios apsunkina automatinę įrodymo paiešką. Šiame darbe yra sukonstruotas indeksinis predikatų logikos skaičiavimas, kurio visos taisyklės yra apverčiamos ir įrodytas jo ekvivalentiškumas daugiasukcedentiniam konstruktyvinės logikos skaičiavimui.
Šis darbas apsaugotas Creative Commons priskyrimo 4.0 viešąja licencija.