Ž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.