Žinoma, kad baigtinumas ir grįžimas išvedimo paieškos medžiu yra kelios iš pačių svarbiausių išvedimų paieškos neklasikinėse logikose problemų. Šitame straipsnyje pateikiami sekvenciniai skaičiavimai modalumo logikoms S5 ir KD45, kuriuose nėra dubliavimo ir išvedimų paieška nereikalauja grįžimo. Tai indeksiniai skaičiavimai su tam tikromis indeksinėmis aksiomomis. Pagrindinės pristatomų skaičiavimų naujovės yra metakintamųjų naudojimas (kartu su natūraliaisiais skaičiais) indeksuose ir visų teigiamų modalumo 2 įeičių numeravimas natūraliais skaičiais.
Šis kūrinys yra platinamas pagal Kūrybinių bendrijų Priskyrimas 4.0 tarptautinę licenciją.
Susipažinkite su autorių teisėmis žurnalo politikoje skiltyje Autorių teisės.