Abstract In the paper, we introduce multilattice versions of the basic congruent and monotonic modal logics. In the case of congruent and monotonic ones, we also study their extensions by Gödel’s rule. We formulate these logics in the form of sequent calculi and prove syntactic embedding theorems (as a consequence, we obtain cut admissibility and decidability). Then we present them algebraically and semantically: via modal multilattices and via general and descriptive neighbourhood frames. We show the dual equivalency of the categories of modal multilattices and descriptive neighbourhood frames. Using Lindenbaum–Tarski algebras, we prove that the sequent calculi under consideration are sound and complete with respect to modal multilattices.

We present a proof searching technique for the natural deduction calculus for the prepositional linear-time temporal logic and prove its correctness. This opens the prospect to apply our technique as an automated reasoning tool in a number of emerging computer science applications and in a deliberative decision making framework across various AI applications.