Investigation of Finitary Calculi for the Temporal Logics by Means of Infinitary Calculi. - Regimantas Pliuskevicius (MFCS, 1990)

Investigation of Finitary Calculus for a Discrete Linear Time Logic by means of Infinitary Calculus. - Regimantas Pliuskevicius (Baltic Computer Science, 1991)

Logical Foundation for Logic Programming Based on First Order Linear Temporal Logic. - Regimantas Pliuskevicius (RCLP, 1991)

Design Complete Sequential Calculus for Continuous Fixpoint Temporal Logic. - Regimantas Pliuskevicius (JELIA, 1992)

Complete Sequential Calculi for the First Order Symmetrical Linear Temporal Logic with Until and Since. - Regimantas Pliuskevicius (LFCS, 1992)

The Analityc Tableaux for Linear Temporal Logic. - Regimantas Pliuskevicius (TABLEAUX, 1992)

Saturation Replaces Induction for a Miniscoped Linear Temporal Logic. - Regimantas Pliuskevicius (Formal Methods in Programming and Their Applications, 1993)

On the Saturation Principle for a Linear Temporal Logic. - Regimantas Pliuskevicius (Kurt Gödel Colloquium, 1993)

On Saturated Calculi for a Linear Temporal Logic. - Regimantas Pliuskevicius (MFCS, 1993)

The Analytic Tableaux for Linear Minscoped Temporal Logic. - Regimantas Pliuskevicius (SCAI, 1993)

On Specialization of Derivations in Axiomatic Equality Theories. - Aida Pliuskeviciene; Regimantas Pliuskevicius; Michal Walicki; Sigurd Meldal (LFCS, 1994)

Saturated deductive systems for temporal specifications. - Regimantas Pliuskevicius (SEKE, 1994)

The Saturated Tableaux for Linear Miniscoped Horn-like Temporal Logic. - Regimantas Pliuskevicius (J. Autom. Reason., 1994)

On the Replacement of Induction for a First Order Linear Temporal Logic. - Regimantas Pliuskevicius (WOCFAI, 1995)

Similarity Saturation for First Order Linear Temporal Logic with UNLESS. - Regimantas Pliuskevicius (JELIA, 1996)

On Saturation with Flexible Function Symbols. - Regimantas Pliuskevicius (MFCS, 1996)

On the Completeness and Decidability of a Restricted First Order Linear Temporal Logic. - Regimantas Pliuskevicius (Kurt Gödel Colloquium, 1997)

Replacement of Induction by Similarity Saturation in a First Order Linear Temporal Logic. - Regimantas Pliuskevicius (J. Appl. Non Class. Logics, 1998)

A Deductive Decision Procedure for a Restricted FTL. - Regimantas Pliuskevicius (ARW, 2000)

On an omega-Decidable Deductive Procedure for Non-Horn Sequents of a Restricted FTL. - Regimantas Pliuskevicius (Computational Logic, 2000)

Deduction-Based Decision Procedure for a Clausal Miniscoped Fragment of FTL. - Regimantas Pliuskevicius (IJCAR, 2001)

Decision Procedure for Temporal Logic of Belief and Actions. - Regimantas Pliuskevicius; Aida Pliuskeviciene (Informatica, 2004)

Decision Procedure for a Fragment of Mutual Belief Logic with Quantified Agent Variables. - Regimantas Pliuskevicius; Aida Pliuskeviciene (CLIMA, 2005)

Termination of Derivations in a Fragment of Transitive Distributed Knowledge Logic. - Regimantas Pliuskevicius; Aida Pliuskeviciene (Informatica, 2008)

A New Method to Obtain Termination in Backward Proof Search For Modal Logic S4. - Regimantas Pliuskevicius; Aida Pliuskeviciene (J. Log. Comput., 2010)

Loop-Type Sequent Calculi for Temporal Logic. - Romas Alonderis; Regimantas Pliuskevicius; Aida Pliuskeviciene; Haroldas Giedra (J. Autom. Reason., 2020)

Loop-Check Specification for a Sequent Calculus of Temporal Logic. - Romas Alonderis; Regimantas Pliuskevicius; Aida Pliuskeviciene; Haroldas Giedra (Stud Logica, 2022)