| Publication | Date of Publication | Type |
|---|
| Normalization Proof for Derivations in PA after P. Cohen | 2021-12-03 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5854738 | 2021-03-17 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5215789 | 2020-02-13 | Paper |
| Intuitionistic Existential Instantiation and Epsilon Symbol | 2020-02-04 | Paper |
| Three faces of natural deduction | 2019-01-15 | Paper |
| The programming system PRIZ | 2018-12-11 | Paper |
| Type-theoretical semantics of some declarative languages | 2018-12-11 | Paper |
| Non-deterministic Epsilon Substitution Method for PA and ID 1 | 2017-09-27 | Paper |
| An extension of the omega-rule | 2016-05-13 | Paper |
| ADC method of proof search for intuitionistic propositional natural deduction | 2016-04-28 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3464619 | 2016-01-27 | Paper |
| The logic of transitive and dense frames: from the step-frame analysis to full cut-elimination | 2015-02-12 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4981452 | 2014-06-24 | Paper |
| Failure of Interpolation in Constant Domain Intuitionistic Logic | 2014-01-07 | Paper |
| Nikolai Aleksandrovich Shanin (obituary) | 2013-12-17 | Paper |
| Epsilon substitution for first- and second-order predicate logic | 2013-04-15 | Paper |
| Effective cut-elimination for a fragment of modal mu-calculus | 2012-10-01 | Paper |
| The Gödel-Tarski Translations of Intuitionistic Propositional Formulas | 2012-07-23 | Paper |
| Preface to the special issue dedicated to Nikolai Alexandrovich Shanin on the occasion of his 90th birthday | 2011-09-12 | Paper |
| Cut-free formulations for a quantified logic of here and there | 2011-09-12 | Paper |
| Countable Version of Omega-Rule | 2011-05-27 | Paper |
| Decidability of the Class E by Maslov’s Inverse Method | 2010-09-03 | Paper |
| Analysis and Extension of Omega-Rule | 2009-04-30 | Paper |
| Cut elimination for a simple formulation of epsilon calculus | 2008-03-28 | Paper |
| Proof Search Tree and Cut Elimination | 2008-03-25 | Paper |
| Unwinding a Non-effective Cut Elimination Proof | 2007-05-02 | Paper |
| Notes on constructive negation | 2006-08-18 | Paper |
| S4 is Topologically Complete for (0,1): a Short Proof | 2006-07-06 | Paper |
| Cut elimination for S4C: A case study | 2006-03-17 | Paper |
| A simple proof of second-order strong normalization with permutative conversions | 2005-09-22 | Paper |
| Dynamic topological logic | 2005-01-31 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4453638 | 2004-03-07 | Paper |
| Completeness of indexed \(\varepsilon\)-calculus | 2003-10-29 | Paper |
| Nikolai Aleksandrovich Shanin (on his 80th birthday) | 2003-08-28 | Paper |
| A termination proof for epsilon substitution using partial derivations | 2003-08-17 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4793026 | 2003-02-18 | Paper |
| Interpolation theorems for intuitionistic predicate logic | 2002-12-11 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2751819 | 2002-03-26 | Paper |
| Linear lambda-terms and natural deduction | 2001-12-07 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2702564 | 2001-07-24 | Paper |
| Reduction of finite and infinite derivations | 2001-07-09 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2703802 | 2001-03-18 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4941993 | 2001-02-05 | Paper |
| Extended normal form theorems for logical proofs from axioms | 2000-08-23 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4495850 | 2000-08-13 | Paper |
| In Memoriam: Albert G. Dragalin 1941–1998 | 2000-06-07 | Paper |
| Normal deduction in the intuitionistic linear logic | 2000-05-15 | Paper |
| The complexity of the disjunction and existential properties in intuitionistic logic | 2000-02-15 | Paper |
| A method of epsilon substitution for the predicate logic with equality | 1999-11-22 | Paper |
| Cut-elimination for simple type theory with an axiom of choice | 1999-09-12 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4250039 | 1999-06-17 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4397029 | 1998-06-25 | Paper |
| Indexed systems of sequents and cut-elimination | 1998-04-15 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4360861 | 1998-04-15 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4376065 | 1998-02-08 | Paper |
| Strong termination for the epsilon substitution method | 1997-09-15 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5688802 | 1997-03-16 | Paper |
| Epsilon substitution method for elementary analysis | 1996-10-15 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4325774 | 1996-04-22 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4312461 | 1995-04-24 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4281258 | 1994-09-26 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4282590 | 1994-09-26 | Paper |
| Complexity of subclasses of the intuitionistic propositional calculus | 1994-06-22 | Paper |
| Resolution calculus for the first order linear logic | 1994-02-22 | Paper |
| A normal form for logical derivations implying one for arithmetic derivations | 1993-08-09 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4694212 | 1993-06-29 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3999386 | 1993-01-23 | Paper |
| Condensed detachment is complete for relevance logic: A computer-aided proof | 1992-06-27 | Paper |
| Proof theory in the USSR 1925–1969 | 1992-06-27 | Paper |
| A NORMAL FORM THEOREM FOR SECOND-ORDER CLASSICAL LOGIC WITH AN AXIOM OF CHOICE | 1992-06-25 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3972527 | 1992-06-25 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5202652 | 1990-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3471707 | 1990-01-01 | Paper |
| Nikolai Aleksandrovich Shanin (on his seventieth birthday) | 1990-01-01 | Paper |
| The completeness of provable realizability | 1989-01-01 | Paper |
| Resolution calculi for modal logics | 1989-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3832565 | 1989-01-01 | Paper |
| The programming system PRIZ | 1988-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3800028 | 1988-01-01 | Paper |
| Corrigendum to ``Semantics of a declarative language | 1987-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3782841 | 1987-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3793768 | 1987-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4725709 | 1986-01-01 | Paper |
| Semantics of a declarative language | 1986-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3755451 | 1986-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3768868 | 1986-01-01 | Paper |
| Description semantics in utopist language and automatic program synthesis | 1985-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3768867 | 1985-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3718146 | 1984-01-01 | Paper |
| The PRIZ system and propositional calculus | 1983-01-01 | Paper |
| Justification of the structural synthesis of programs | 1982-01-01 | Paper |
| A new reduction sequence for arithmetic | 1982-01-01 | Paper |
| Primitive recursive estimate of strong normalization for predicate calculus | 1982-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3666280 | 1982-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3674650 | 1982-01-01 | Paper |
| Closed categories and the theory of proofs | 1981-01-01 | Paper |
| What can be done with PRA? | 1980-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3659785 | 1980-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3859764 | 1980-01-01 | Paper |
| NIKOLAI ALEKSANDROVICH SHANIN (on his sixtieth birthday) | 1980-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3866100 | 1979-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3880842 | 1979-01-01 | Paper |
| Finite investigations of transfinite derivations | 1978-01-01 | Paper |
| Transfinite expansions of arithmetic formulas | 1978-01-01 | Paper |
| E theorems | 1977-01-01 | Paper |
| Heyting predicate calculus with epsilon symbol | 1977-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4145693 | 1977-01-01 | Paper |
| Derivability of admissible rules | 1976-01-01 | Paper |
| Cut-elimination theorem for relevant logics | 1976-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4149746 | 1976-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4172048 | 1976-01-01 | Paper |
| Theory of proofs (arithmetic and analysis) | 1975-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4079564 | 1975-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4081218 | 1975-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4108298 | 1975-01-01 | Paper |
| The Skolem method in intuitionistic calculi | 1974-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4047537 | 1974-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4133596 | 1974-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4145692 | 1974-01-01 | Paper |
| Quantifier-free and one-quantifier systems | 1973-01-01 | Paper |
| Exact estimates of the provability of transfinite induction in the initial segments of arithmetic | 1973-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4133602 | 1973-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4152522 | 1973-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4766963 | 1972-01-01 | Paper |
| On predicate and operator variants of the formation of theories of constructive mathematics | 1972-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5626610 | 1971-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5634868 | 1971-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5638266 | 1971-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5590052 | 1969-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5596257 | 1969-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5556396 | 1968-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5560260 | 1968-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5560261 | 1968-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5560262 | 1968-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5569430 | 1968-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5569431 | 1968-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5598335 | 1968-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5604435 | 1968-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5604437 | 1968-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5604438 | 1968-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5607207 | 1968-01-01 | Paper |
| On the construction of conservative logical deductions | 1968-01-01 | Paper |
| Sovability of the problem of deducibility in LJ for a class of formulas not containing negative occurrences of quantifiers | 1968-01-01 | Paper |
| On some calculi of modal logic | 1968-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5551112 | 1967-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5551113 | 1967-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5551114 | 1967-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5573966 | 1967-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5579477 | 1967-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5579478 | 1967-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5581591 | 1967-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5581593 | 1967-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5581595 | 1967-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5588607 | 1967-01-01 | Paper |
| Corrigenda and addenda to the article 'On predicate and operator variants of the formation of the theories of constructive mathematics' | 1967-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5536261 | 1966-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5579476 | 1966-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5553292 | 1965-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5559243 | 1965-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5343328 | 1963-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5344165 | 1962-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5596800 | 1962-01-01 | Paper |
