| An extension of the omega-rule. | 2 | 0.44 | 2016 |
| ADC method of proof search for intuitionistic propositional natural deduction. | 1 | 0.35 | 2016 |
| Failure of interpolation in constant domain intuitionistic logic. | 0 | 0.34 | 2013 |
| Epsilon substitution for first- and second-order predicate logic. | 2 | 0.70 | 2013 |
| Effective Cut-elimination for a Fragment of Modal mu-calculus | 2 | 0.48 | 2012 |
| Intuitionistic Existential Instantiation and Epsilon Symbol | 0 | 0.34 | 2012 |
| Cut-Elimination For The Mu-Calculus With One Variable | 3 | 0.50 | 2012 |
| The gödel-tarski translations of intuitionistic propositional formulas | 0 | 0.34 | 2012 |
| Cut-free formulations for a quantified logic of here and there | 2 | 0.38 | 2010 |
| Decidability of the class e by Maslov's inverse method | 3 | 0.45 | 2010 |
| Logic, Language, Information and Computation | 0 | 0.34 | 2010 |
| Preface: Logic, Language, Information and Computation | 0 | 0.34 | 2009 |
| Proof search tree and cut elimination | 0 | 0.34 | 2008 |
| Cut Elimination for S4C: A Case Study | 2 | 0.39 | 2006 |
| Cut Elimination for a Simple Formulation of PAε | 0 | 0.34 | 2006 |
| Notes on Constructive Negation | 3 | 0.54 | 2006 |
| Unwinding a non-effective cut elimination proof | 1 | 0.48 | 2006 |
| S4 is Topologically Complete for (0, 1): a Short Proof | 0 | 0.34 | 2006 |
| A proof of topological completeness for S4 in (0, 1) | 2 | 0.43 | 2005 |
| A simple proof of second-order strong normalization with permutative conversions | 4 | 0.50 | 2005 |
| Propositional logic of continuous transformations in Cantor space | 6 | 1.12 | 2005 |
| Dynamic topological logic | 28 | 4.57 | 2005 |
| Completeness Of Indexed Epsilon-Calculus | 0 | 0.34 | 2003 |
| Extended normal for theorems for logical proofs from axioms | 0 | 0.34 | 2000 |
| Cut-Elimination for Simple Type Theory with An Axiom of Choice | 1 | 0.37 | 1999 |
| The complexity of the disjunction and existential properties in intuitionistic logic | 14 | 1.10 | 1999 |
| Normal deduction in the intuitionistic linear logic | 4 | 0.69 | 1998 |
| Linear Lambda-Terms and Natural Deduction | 5 | 0.71 | 1998 |
| Indexed systems of sequents and cut-elimination | 20 | 1.62 | 1997 |
| Existential Instantiation and Strong Normalization | 3 | 0.58 | 1997 |
| Three Faces of Natural Deduction | 0 | 0.34 | 1997 |
| Epsilon substitution method for elementary analysis | 19 | 3.53 | 1996 |
| Strong Termination For The Epsilon Substitution Method | 4 | 0.66 | 1996 |
| Strategies for Resolution Method in Non-classical Logics (Abstract) | 0 | 0.34 | 1993 |
| Resolution calculus for the first order linear logic. | 13 | 1.21 | 1993 |
| Complexity of Subclasses of the Intuitionistic Propositional Calculus | 3 | 0.50 | 1992 |
| Condensed Detachment is Complete for Relevance Logic: A Computer-Aided Proof. | 4 | 0.70 | 1991 |
| Proof theory in the USSR 1925-1969 | 5 | 0.71 | 1991 |
| Type-theoretical Semantics of Some Declarative Languages | 0 | 0.34 | 1991 |
| Propositional Logic Programming and Priz System | 2 | 0.43 | 1990 |
| COLOG-88, International Conference on Computer Logic, Tallinn, USSR, December 1988, Proceedings | 21 | 23.55 | 1990 |
| The Completeness of Provable Realizability | 10 | 1.48 | 1989 |
| The programming system PRIZ | 12 | 10.42 | 1988 |
| Corrigendum: Semantics of a Declarative Language | 0 | 0.34 | 1987 |
| Some Formal Systems of the Logic Programming | 1 | 0.37 | 1987 |
| Justification of the structural synthesis of programs | 33 | 8.06 | 1982 |
