Email (print-outs) 1990-2014
1990-1994
1995-1998
1998-2000
2000-2012
1994-2001
Foundations of Mathematics (FOM) digest 2002-2011
Friedman, Harvey; Foundations of Mathematics (FOM) digest 2003-2010
Conferences
Russian
Conference proceedings 1976-2001
2012
English
Conference Materials from St. Petersberg 2014
Philosophy, Mathematics, Linguistics: Aspects of Interaction 2009
Miscellaneous Documents undated
Association for Symbolic Logic 1997-2011
Joint Mathematics Meetings 2012 Jan. 4-7
Collegium Logicum - Cut-Elimination 2005 Jul. 4-6
Mathematics - XXI Century - PDMI 70th Anniversary 2010 Sep. 13-18
MFCS & CSL 2010
Lecture Notes in Logic 1974, 1990, 1996
The Rolf Schock Prizes 1997
Universality of Science 1995-1996
Methods of Logic in Mathematics III 2006 Jun. 1-7
European Foundation for Logic, Language and Information 1992 Aug.
BRICS Proof Theory and Complexity 1998 Aug. 3-7
First International Wormshop 2012 Apr. 16-19
Mathematische Logik 1998 Jan. 18-24
Proof Theory: Workshop on Logic, Foundational Research, and Mathematics 2003 Oct. 9-11
Model Computation - Principles, Algorithms, Applications 6/16/2000
1st North American Summer School in Logic, Language, and Information 2002 Jun. 24-30
WoLLIC 2005 Proceedings 2005 Jul. 19-22
ILCLI 1993-2003
Takeuti Symposium 2003 Dec. 17-19
Natural Deduction 2001
WoLLIC 2006
Conferences 2006
Logic in the Netherlands 1998 Feb.
Banff International Research Station 2007 Feb. 18-23
Shell Oil Symposium Series 11/5/1995
9th International Conogress of Logic, Methodology, and Philosophy of Science 1991 Aug. 7-14
10th International Conogress of Logic, Methodology, and Philosophy of Science 1995 Aug. 19-25
Nato ASI Report 1993 Aug. 13-24
Godel's Excursions Into Intuitionistic Logic 1983 Jul. 10-12
Summer School and Conference on Mathematical Logic 1988 Sep. 13-23
Logic Colloquium 2004 Jul. 25-31
Logic Colloquium 1990 Jul. 15-22
Computer Science Logic 1992 Jul. 13-17
Proof Theory and Algorithms Workshops 2003 Mar. 23-28
DAYS Shanin 1999
Markov 2003
CSR 2006
Mathematische Logik 1995 Apr. 2-8
HPLMC-02 2002 Nov. 7-9
Nasslli 2003 Jun. 17-21
Classical Logic and Computation 2010
Symbolic Logic and Computer Science 1995 Sep. 17-20
Logic colloquium, Berlin 1989
Colloquium on Modal Logic 1991
1992
1992-1994
1994
1994-1995
1994-1999
Logic colloquium 1995 Aug 9-17
1995
1996
International Conference TABLEAUX'97-Analytic Tableaux and Related Methods 1997-03
1997
1997-1998
Logic in Action: An NWO Spinoza Award Project 1997-1998
1998
17th International Conference on Automated Deduction, Carnegie Mellon University 2000 Jun 17-20
Constructivism in Non-Classical Logics and Computer Science 2000 Sep 30-Oct 2
LCCS'2001: Proceedings of the International Workshop on Logic and Complexity in Computer Science, Universite Paris, France 2001 Sep 3-5
Logic-Based Program Synthesis: State of the Art and Future Trends, 2002 AAAI Spring Symposium 2002
Conference in Honor of the 60th Birthday of Friedman, Harvey M. 2009 May 14-17
Leeds Symposium on Proof Theory and Constructivism 2009 Jul 3-16
Algebra and Coalgebra meet Proof Theory 2013
Department files
CAST 1995
Funding 1994-2008
Feferman, Solomon symposium 2004
DTL 2004
Drafts 1992-2009
Dept 2008
Dept 2005-2006
2005
Computer Science Department 2006
Publications
GM published articles in Russian undated
A Normal Form Theorem For Second-Order Classical Logic with an Axiom of Choice (2 copies) 1989
A normal form for logical derivations implying one for arithmetic derivations (2 copies) 1993
A New Reduction Sequence for Arithmetic undated
A New Reduction Sequence for Arithmetic 1982
Development and present state of epsilon substitution method undated
Beklemisher's construction of Eo Stanford talk undated
Abstract for Banff 2007
Model elimination and cut elimination undated
Abstract for Contibuted Talk 2004
BSL 3, N3 Winter Meeting of the Association for Symbolic Logic 1997
Bull. ASL V1.N3 Winter Meeting of the Association for Symbolic Logic 1995
A Completeness Proof for Propositional S4 in Cantor Space (2 copies) 2001
ADC Method of Proof Search for Intuitonistic Prepositional Natural Deduction 2012
Admissible and Derived Rules undated
An Approach to an e-Substitution Method dor ID1 2001
Applications of Proof-theoretic Transformation (Abstract) 1998
A proof of topological completeness for S4 in (0,1) (2 copies) 2004
A simple proof of second-order strong normalization with permutative conversions (2 copies) 2005
A simple proof of the coherence theorem fro Cartesian closed categories undated
A termination proof for epsilon substitution using partial derivations (3 copies) 2003
Applications of Proof-theoretic Transformation (Abstract) 1998
Axiomatization of a Skolem Function in Intuitionistic Logic (3 copies) 2000
Classical and Intuitionistic Geometric Logic (3 copies) 2012
Logical Investigations (2 copies) 2000
Closed Categories and the Theory of Proofs undated
Closed Categories and the Theory of Proofs (office copy) 1992
Completeness of Indexed e-Calculus (2 copies) 2003
Complexity of Subclasses of the Intuitionistic Propositional Calculus (2 copies) 1990
Condensed Detachment is Complete for Relevance Logic: A Computer-Aided Proof 1991
Corrigenda and Addenda to the Article "On Predicate and Operator Variants of the Formation of the Theories of Constructive Mathematics" 1967
Cut-elimination and Normal Forms of Sequent Derivations 1994
Cut elimination for a simple formulation of epsilon calculus (2 copies) 2007
Cut Elimination for S4C: A Case Study 2006
Abstracts of the AMS 1985
Cut-Elimination for Simple Type Theory with an Axiom of Choice (3 copies) 1999
Cute-Free Calculi of the S5 Type (3 copies) undated
Cut-Free Formulations for a quantified logic of here and there 2010
Decidability of the Class 3 by Maslov's Inverse Method 1971
Decidability of the Class 3 by Maslov's Inverse Method 2010
Disjunctive interpretation of the LJ-Calculus e.u. Implicative complexity of axiomatics undated
Epsilon Substitution for Predicate Logic 2010
Epsilon substitution method for elementary analysis 1996
Epsilon substitution method for elementary analysis 1993
Epsilon-Substitution Method for Ramified Language and Comprehension Rule (2 copies) 1999
Existential Instantiation and Strong Normalization 1997
Theoretical Computer Science: Extended normal form theorems for logical proofs from axioms (2 copies) 2000
J Soviet Math 8, N3 1977
Exact Estimates of the Provability of Transfinite Induction in the Initial Segments of Arithmetic 1972
Failure of Interpolation in Constant Domain Intuitionistic Logic (2 copies) 2013
Finite Investigations of Transfinite Derivations undated
Fixing Frege 2005
Failure of Interpolation in Constant Domain Intuitionistic Logic (2 copies) 2013
Justification of the Structural Synthesis of Programs 1982
Interpolation Theorems for intuitionistic predicate logic (2 copies) 2002
In Memoriam: Albert G. Dragalin (10 copies) 1999
Indexed Systems of Sequents and Cut-Elimination (2 Copies) 1997
Implicative Complexity of Axiomatic Systems undated
Heyting Predicate Calculus with Epsilon Symbol undated
Herbrand's Theorem for the Predicate Calculus with Equality and Functional Symbols (3 copies) 1966
Gentzen-Type Systems and Resolution Rule Part II. Predicate Logic undated
Lecture Notes in Computer Science 1988
Gentzen-Type Systems and Hilbert's Epsilon Substitution Method. I (2 copies) 1994
Selected Papers in Proof Theory, Bibliopolis and North-Holland p. 221-294 (2 copies) 1992
Linear Lambda-Terms and Natural Deduction (2 copies) 1998
Logical Equations in Monadic Logic (3 copies) 2008
Mechanical Proof-Search and the Theory of Logical Deduction in the USSR 1971
New Trends in Foundations of Mathematics 2009
Nikolai Aleksandrovich Shanin (obituary) (3 copies) 2013
Normal Forms for Sequent Derivations (2 copies) undated
Email with Subject: Contraction in Sequent Derivations 1997
Normal Deduction in the Intuitionistic Linear Logic (2 copies) 1996
Normalization of Finite Terms and Derivations via Infinite Ones (3 copies) 1992
Normalization Theorems for the Intuitionistic Systems (2 copies) 1990
Notes on Constructive Negation (4 copies) 2006
Normal Forms for Sequent Derivations 1996
Normalization of Finite Terms and Derivations via Infinite Ones 1992
on E-Theorems (2 copies) undated
On Novikov's Hypothesis undated
On Some Calculi of Modal Logic undated
On the Construction of Conservative Logical Deductions undated
On the Semantics of Modal Logic (2 copies) 1971
Proof Search Tree and Cut-Elimination undated
Proof Theory and Category Theory 1992
Formal Systems for Classical Analysis undated
Proof Theory in the USSR (2 copies) 1991
Propositional logic of continuous transformations in Cantor space (2 copies) 2004
Propositional Logic Programming undated
Proof Theory in the USSR 1991
Propositional Logic Programming undated
Propositional Logic Programming and the Priz System 1990
Quantifier-Free and One-Quantifier Systems 1972
Reduction of finite and infinite derivations 2000
The Programming System PRIZ 1988
Thoraf Skolem and the Epsilon Substitution Method for Predicate Logic (2 copies) 1996
The Completeness of Structural Synthesis Rules (2 copies) 1982
The Completeness of Provable Realizability (2 copies) 1989
Reduction of finite and infinite derivations 2000
Reduction to Theories of Lower Order 1996
Reflection and Transfinite Induction (2 copies) undated
Resolution Calculi fro Modal Logics (2 copies) 1989
Resolution Calculus for the First Order Linear Logic (2 copies) 1993
Resolution Strategies for the Intuitionistic Logic (3 copies) 1994
Semantics of a Declarative Language 1986
Computers and Artificial Intelligence 1990
Skolem's Method of Elimination of Positive Quantifiers in Sequential Calculi (2 copies) 1966
Solvability of the Problem of Deducibility in LJ for a Class of Formulas not Containing Negative Occurrences of Quantifiers (2 copies) undated
Some formal systems of the logic programming 1987
Strong Termination for the Epsilon Substitution Method (2 copies) 1996
Stability of E-theorems and Program Verification (7 copies) undated
What Can Be Done in PRA 1975
Transfer of Sequent Calculus Strategies to Resolution for S4 (2 copies) 1996
Three Faces of Natural Deduction (2 copies) 1997
The Universality of the Canonical Tree (2 copies) 1976
The Use of Abstract Language in Elementary Metamathematics: Some Pedagogic Examples 1975
The complexity of the disjunction and existential properties in intuitionistic logic (2 copies) 1998
The Epsilon Substitution Method and Continuity (2 copies) 2002
The Independence of the Postulates of Natural Calculi undated
The Skolem Method in Intuitionistic Calculi 1972
The PRIZ system and Propositional Calculus 0
Friedman, Harvey
Subject files
Partial Copies undated
B3AAA4AX undated
Halmosh undated
J.V. Neumann undated
Schwichtenberg and Wainer undated
Trakhtenbrot and Barzdin 1993
V. Dalen Brouwer 2005
Moschovakis 1974
Normann 1980
Walters 1975
Mitchell 2000
Lyndon 1966
Leisenring 1969
Lewis and Papa undated
Thinking About Mathematics undated
Gentzen undated
Girard 10/29/2009
Jervell 4/17/2009
Fitting and Smullyan undated
Krantz 7/25/2007
Harrison undated
Kunen undated
Girard undated
Edwards undated
Pohlers 2005
Lambda-calculus and Combinators in the 20th Century 7/24/2009
RPR Handouts (my copies) 6/13/2000
Provability Logic 38292
Using the Borsuk-Ulam Theorem 2003
Shoenfild 1993
Thinking About Mathematics undated
Epsilon 2000-2001
Epsilon 2000
Epsilon 2003
Epsilon 1995-1997
Epsilon 1997
Workbooks 2005-2006
Epsilon undated
Epsilon 2001-2005
Papadi 1994
Epgytest undated
Epsotransp 2006
Epsilon and Henry undated
A New Approach to Epsilon-Substitution Method 37245
Epsilon Substitution Method for ID1 17-18 Jan.
von Neumann's Example 38203
APAL Paper 2003
Migoa Report Etc. undated
Epgy undated
M294 Epsilon 2004
Workbooks 2010
Epsilon 2009
Epsilon 1998
Epsilon 2003
A New Approach to Epsilon-Substitution Method 36944
Normalization undated
Normalization 2010
Epsilon undated
Epsilon Oct. 1991 - Feb. 1992
Epsilon-Symbol 1983 - July 1991
Akiyoshi Ryota undated
KO^M/APAR. undated
Arai undated
Aczel 1974
Ackermann undated
Avigad undated
Baaz undated
Beklemishev 2011 Mar.
Barendregt undated
Babaev undated
Brouwer undated
Bovykin undated
Beeson undated
Buss undated
Buchholz undated
Coquand undated
Ciabattoni undated
Carlson undated
Cantini undated
Corsi undated
Delzell undated
Ferreira undated
Fernandez undated
Dragalin/ Pap. undated
Fitting undated
Fisher undated
Gabbay undated
Gavril undated
Ghilardi undated
Girard undated
Gurevich undated
Gowers undated
Gordeev undated
Hrubevs undated
Hirsch undated
Kaye undated
Jager undated
Sieg undated
Shanin undated
Simpson undated
Scott D. undated
Seely undated
Feferman undated
Van Benthem undated
Troelstra undated
Trakhtenbrot undated
Towsner undated
Taitslin undated
Takeuti undated
Wilken undated
Urquhart undated
Tseitin undated
Tupailo undated
Visser undated
Voevodsky undated
Voronkov undated
Statman undated
Slavnov undated
Sommer undated
Tait undated
Tatsuta undated
Tao undated
Wainer undated
Weiermann undated
Ting undated
Olkhovikov undated
Pappinghaus undated
Oliva 40626
Okada 1999
Parikh 2001
Parsons undated
Pauly 2005
Pearce undated
Plato undated
Zach undated
Zaslavsky undated
Zakhryashev undated
McCarthy 1978-1981
Martin undated
Miller undated
Moschovakis undated
Leivant undated
Leitgeb undated
Levin undated
Lifschitz undated
Kopke 2006
Heusinger undated
Harrison undated
Hales undated
Lando 2011
Kripke 2000
Lambek undated
Maslov undated
Wilken undated
Wolter undated
Manin 2011
Maksimova undated
Nerode undated
Muravitski 2008
Mundici undated
Kohlenbach undated
Kohlenbach A-F undated
Kushner undated
Kohlenbach 2010
Kreisel undated
Kremer undated
Five Notes on the Application of Proof Theory to Computer Science 12/10/1971
Kreisel Elements undated
Fresh 12 undated
Fresh undated
PT 2012 2010/2011
General Interest 2008-2009
Proof Mining 2010
Here There 2009
Ebar Transp. 2008
Logical Ideal 2010
Modal Logic 2009
Modal Logic Genint 2009
Schwichtenberg undated
Students 2006
Summer Project 2004
Tinker 2009
Teaching undated
Teach 2007
Ergod Articles undated
Zadachnik 2001
Workshop 2007
Wollic 2006
VPUE Grant 2002
Visitors 2006
Travel 2005-2009
Logic Seminar 2010-2011
Seminars 2011-2012
Seminars 2008-2010
Seminars undated
Seminar Talks undated
Seminars 2010
Sabbatical undated
Pohlers undated
Rusgrant 2003/2013
Reviews Ref. Report undated
Rumfit undated
Rayo 2010
Rathjen undated
Queiroz undated
Prawitz undated
Sasha 2007-2010
Sasha 2003-2004
Sasha undated
Topics in Logic: An Introduction to Proof Mining 2008
Pratt, Scott L. Hist. 94 Schroder-Heister 1999
Sazonov 2001
Schutte 1992
Schein 2007
Powers, Thomas M. Hist. 94 Schellinx 2002
Rybakov 2002
MTA 1999-2001
PT 2005 II 2005
PT 2005 I 2005
PT05 Lect 2005
Logic 2 undated
PT05 Lect 2005
MTA 06 Transpar 2006
Fresh 06 2006
PHILMATH 2004
Berkeley Set Theory 2004
MTA 06 2006
General Interest undated
Rec. Theory undated
Topics 2009
Topics 2010
Topics 354 2009
General Interest 2008
Topics Transp. 2010
TR 2005
Gen. Interest 2010
Sasha 2001
Truth undated
Linguistics undated
Sasha 2004-2006
Assorted Mathematical Documents undated
Chang & Keisler undated
Bag of Proofs 1994
International Conference Tableaux 1999
The Ergodic Theoretical Proof of Szemeredi's Theorem 1982
A Formalization of Principle-Based Conception of Modality 2/6/2003
Interplay Between Proof Theory and Constructivist Ideology in the USSR 1950-1970
Completeness of Indexed e-Calculus 6/1/2002
Extensions of the Substitution Mehod to Impredicative Systems 2003
Semantical Analysis of Induitionalistic Logic undated
Contributions of G. Takeuti undated
Intuitionistic Frege Systems Are Polynomially Equivalent undated
Topological Semantics of Propositional Int undated
Substitution Method for Subsystems of Analysis 10/22/1993
Skolen and Epsilon Substitution Method undated
Effective Content of Non-Effective Proofs 6/1/2006
Effective Proofs and Existence in Mathematics 5/4/2006
Review of Logical Aspects of Computation: Contributions and Distractions 10/4/2006
Existential Instantiation for Intuistionistic Logic 1997
Proof Theory and Consistency Proofs 2/27/2005
Normalization in the First Order e-Calculus 1992
Best Approximation in L1 undated
Lecture Slides undated
Hard Analysis: New Life of Old Ideas 10/12/2010
Describing the Ordinal of Mathematical Analysis 5/19/2010
Epsilon Substitution Method 2010, Mar. 17-18
Fixing Frege 2005
Epsilon Substitution Method for ID1 Jan. 17-18
Three Faces of Natural Deduction undated
Sequent Formulation undated
A Simple Substitution Method for ID1 20 Mar.
A Proof of Topological Completeness for S4C in Cantor Space 17 Dec.
A Simple Proof of Strong Normalization w/ Permutative Conversions undated
Epsilon Substitution Method 2005
Dynamic Topological Logic undated
The Logic of Continuous Transformations 2003
Problems Around e-Calculus undated
Strong Termination for the Epsilon Substitution Method undated
The Undecidability of Dynamical Topological Logics undated
Intuitionistic Frege Systems Are Polynomially Equivalent 2/24/2004
Natural Deduction and its Neighbors 2000
Uniqueness Proofs in Approximation Theory undated
A New Construction of Interpolants 5/21/2002
A Mild Extension of First Order Predicate Logic undated
Miscellaneous Proofs undated
Reformulation in e-Language undated
A Review of Effective Bounds on Strong Unicity in L1-Approximation 4/16/2002
Define a Node undated
Sets undated
A Gentzen-style Formulation of the System B undated
Tran5P 10 undated
Decidable Theories 2013
Failure of Interpolation in the Intuitionistic Logic of Constant Domains 3/6/2012
Mathematical Logic undated
Decidable Second Order Theories 5/31/2011
Countable Version of Omega-Rule 5/17/2011
Tantu 2011 Jun. 15-17
Elementary Intuitionistic Theories undated
Set Theory 2011
Decidable Second Order Theories Transpar 2011
Category Theory and Structural Proof Theory 2010
Bslid. tex undated
Hard Analysis: New Life of Old Ideas 2010
Abstract undated
New Trends in Foundations of Mathematics 2008
Reduction to Theories of Lower Order 2009
Transpar 2001-2002
Transpar 2001
Incomplete Proofs and Program Synthesis 2002
A Review by G Mints of W. Buszkowski, Methematical Linguistics 2002
Transpar 2002
Transparencies undated
Transpar 2002
Transpar 2 2002
Transpar undated
Transpar undated
Transpar undated
Transparencies undated
Logic Exercises undated
E Class 2002
EPS06 Class 2006
TR Girard WDW 2007
Fresh 07 2007
Constructive Math 351 B 2006
A Formalization of Principle-Based Conception of Modality 12/16/2002
An Accelerated e-Substitution Method undated
An e-Sub Method for Arithmetic with Predicates 2/22/2001
A New e-Substitution Method for CR Nov. 1999 - Aug. 2000
A New Construction of Interpolants 5/21/2002
A Note of Completeness of an Epsilon Substitution Calculus 1/26/1995
A Proof of a Theorem by Ikeda and Arai 11/1/1995
A Simple Strong Normalization Proof with E and V undated
A Syntactic Proof of a Preservation Result 1/21/2001
Boolean Equations 3/23/1999
Conservation over PRA 3/14/1994
Continuity Theorem for Effective Operators in Metric Spaces 11/19/1996
Cut Elimination for Provability Logic 4/30/2005
EPSCORRESP undated
Extension of e-Substitution Method to ID1 1/6/2006
Finite Model Property for S4C 2/10/2006
Hilbert's Program and the Substitution Method 1/12/1998
Hilbert's Substitution Method 5/3/1994
Modulation and Interpolation 10/17/2002
Natural Deduction and Normalization for Quantified Modal Logic w/ Equality 1995
Normalization as an e-Substitution Process 11/15/1994
Normalizing IS4 2/20/1998
Normalization Proof for Derivations in PA After P. Cohen 7/10/1997
On Maslov's Inverse Method 12/2/1997
Partial Proofs and Cut-Introduction 1/11/1999
Proof Search Under Shanin 5/13/1999
Quine and Modality undated
Resolution Rule for Diagrams undated
Simplified Strong Normalization Proof for Logic with Existence 7/22/1997
Solving Equations in Modal Logic 3/1/2007
Strong Normalization for Infinite 5/8/1997
Tait-Style Strong 9/12/1997
Topology and Logic 8/12/2004
Work of A.A. Markov on Stepwise Semantics 11/14/2002
Cut Elimination for S4C undated
Relationship Between Proof Theory and Model Theory 4/21/2003
Abstracts 2002-2006
A Completeness Proof for Propositional S4 9/24/2002
An Approach to an e-Substitution Method undated
An e-Substitution Method for Predicate Logic 6/13/1994
A Proof of Topological Completeness for S4 undated
A Termination Proof for e-Substitution undated
Axiomatization of a Skolem Function undated
Chapter OTL undated
Classical MLL = IMLL 9/7/1999
Completeness of Indexed e-Calculus undated
A Completeness Proof for Propositional S4 7/14/1995
Cut Elimination for a Simple Formulation of Epsilon Calculus undated
Cut Elimination for Simple Type Theory with an Axiom 10/1/1997
Dynamic Topological Logic 3/19/2004
Epsilon-Substitution Method for Ramified Language and Comprehension Rule 12/30/1994
Existential Instantiation and Strong Normalization 1/27/1997
Extended Normal Form Theorem for Logical Proofs from Axioms 1999
Incomplete Prioofs and Program Synthesis, Extended Abstract 1/10/2002
Indexed Systems of Sequents and Cut-Elimination 10/12/1995
Interpolation undated
Intuitionistic Frege Systems Are Polynomially Equivalent 8/5/2004
Linear Terms undated
Notes on Constructive Negation undated
Propositional Logic of Continuous Transformations in Cantor Space 12/9/2004
Quick Cut-Elimination for Monotone Cuts 2001 Apr.
Reductions of Finite and Infinite Derivatives 4/19/1999
Reductions to Theories of Lower Order 5/7/1996
Russell Anticipation of Intuitionistic Logic undated
S4 is Topologically Complete for R undated
Skolemization and Quick Cut-Elimination undated
Strong Termination for the Epsilon Substitution Method 10/10/1995
Terminating Epsilon Substitution undated
The Complexity of the Disjunction and Existence 8/11/1998
The Epsilon Substitution Method and Continuity undated
Thor Skolem undated
Three Faces of Natural Deduction 6/27/1997
Topological Completeness of Propositional Int 6/14/2000
Transfer of Sequent 2/3/1995
Proof Search Tree and Cut-Elimination 8/8/2007
Logical Equations in Monadic Logic 8/8/2007
Unwinding a Non-Effective Cut-Elimination Proof undated
Letters to Answer undated
Letters undated
Kriesel undated
Stanford undated
Grad Students undated
Invitations undated
Interpolation undated
IGPL-JLC 2010 Apr.
Help to Russia undated
Guests 7/17/2006
Grad Workshop undated
Log Prog 2006-2011
Logic Program 2003
LMH 2005-2009
Maslovs 1993
Markov undated
Masters 2003-2004
Log Seminar 2002-2003
Lists undated
Log Search 2001-2005
Logic Lunch 2001-2002
Logic Flyer undated
Past Conferences undated
Notes of Talks (Others) 9/4/2001
Meetings 2001-2005
Quine undated
PT Workshop 2005
Problems undated
Serger 8/28/2006
Proof Mining 2010
Constructive Math Topics 2008
Banalytic undated
Ebar undated
Conference 2001
Cade Tutorial undated
ASL Reviews undated
AMS Notices undated
Annual Report 2009-2011
AMS Notices undated
Aslo 2005-2014
Historically important diss with GM notes + comments 1993
Natural Deduction + notes 1965
Russia textbook important in his field 1974
Programming book important in his work + notes 1985
Predilation analysis 1973
Inscription to GM 1999
Very rare Georgian logician + Georgian publishing company 1985
Standard Russian textbook in Math Logic 1983
Bibliography that includes GM papers 1989
Inscription + notes 1993
Popular lecture in its original form 1979-1982
Maslov translated from The French 1987
By GM and Maslov 1965
GM notations pg 216 1979
Contains paper by GM: special book or topic 1978
by Novikov Math Logic early textbook in the field 1959
Textbook Algebra, geometry with intuitionistic logic insert 1975
Theories for Admissible Sets: A Unifying Approach to Proof Theory 1986
GM's well used copy of this important text 1982
Extensive notes 1956
Fraenkel and Bar-Hillel Text on Set Theory in Russian with extensive card of notes and extensive annotation 1966
K. Schutte Proof Theory + Notes 1977
Hilbert's tenth problem 1993
MOCKBA MNP + extensive notes 1981
Girard - Dissertationes Mathematicae + extensive notes 1976
Kreisel 1981
The Problems of Philosophy: Third Edition 1979
Constructive Math 1970
Famous Mathematica - G.M. Edition 2004
Institute of Imformatics Systems 1991
Abstracts and Resumes 1966
Early G.M. Papers 1966-1967
Grisha an Editor 1983
Inscription 1986
A History of Philosophy and Logic in Russia 1995
Theory of Algorithms 1954
G.M. Papers 2007
G.M.'s Notations 1995-2013
Annals of Pure and Applied Logic 2005, May.
Information and Computation 2009, Oct.
First Order Modal Logic undated
Abstacts undated
Papers undated
VITAS
VITA etc. 1997
Archive Trips etc. 1992
History undated
CSLI 1994
J. Ayers 10/1/2001
Anna undated
Days SPB undated
Cohen 1997
Freidson 1998
Hohmas 1994-1995
ICM 1999
Kestrel 1999
Kremer 1996-1997
LLC 01 2001
Maslova 1997-1999
Markov Volume 1997-2000
Nog 1997
Onthologies 1996
Orevkov 1993-1994
Proof Checking 1994-1996
Proposal 1995-2000
Rybakov 1995
Satisfiability 1999
Seminars 1991-2000
Seregine undated
Smirnov 1996
Soros 1994
Springer Files 1993
Summa 2001
Talks Mine 1993
Techn Report, CSLI 11/15/1994
Tests (General) 1993
Travel 1992-2001
Vassilyer 1998
Visitors 1996-1998
Visits (Past) 1998
Workshop 2K 2000
Zaslavsky 1996
Epsilon Calculus with Applications 3/13/2010
Journals 1991-1992
Survery, Proof Theory 1970-1979
Model Th. B 1992-1994
160B 1993-1994
Model Theory 1993
160B 1992
290B Model Theory B 1996
Proof Theory B 1995
M294 1997
Rec. Theory B 1997
Recursion Theory 1996
M294 1996
Topics in Logic 1993
Tekctb1 undated
Philosophy 159 undated
160B 1997
160B 1996
160B 1995
160A 1992-1993
160A Math Logic 1987 & 1992
Negation 2000 2000
M294 1994
Proof Theory B 1999
Proof Theory 1994
Logic Seminar Spring 2001
Modal Logic 1996
Etch undated
160B 2000
160B 2001
Model Theory A 1999
Model Theory A 1995
160B, gg undated
Proof Theory undated
Proof Theory 1992
Proof Theory A98 undated
PTB2001 2001
MTB 2000 2000
MTB 02 2002
PT 02 2002
160A 2001 2001
160A 2000 2000
Proof Theory 1987
M290B Model Theory B 2004
Proof Theory B 2003
The System ID undated
Proof Theory B 2003
Small Collection of Business Cards on G.M.'s desk undated
Center For the Study of Language and Information undated
Cut-elimination and Normal Forms of Sequent Derivations 1994, Nov.
Grigori Mints - bio, cv, etc. undated
Proofs, Categories and Computations - Essays in Honor of Grigori Mints 2010
Reviews, Evaluations undated
PHIL162/262 2003
TRUTH13N 2004
Logic 1 undated
Logic Berkeley undated
Bounded Arithmetic 1986
Absoluteness of Intuitionistic Logic 1970
Recurrence in Ergodic Theory and Combinatorial Number Theory 1981
Logic Colloquium 2004
Essays Dedicated to Johan van Benthem on the Occasion of his 50th Birthday 1999
Das Kontinuum undated
Problems of Reducing the Exhaustive Search 1996
Theoretical Computer Science 2000
Constraint Programming 1991
Godel Remembered 1983
Programming Logic 1992
Computers and Artifical Intelligence 1990
Estonian Academy of Sciences Yearbook 2008-2009
Mathematical Logic 1990
Notre Dame Journal of Formal Logic 1989
Journal of Philosophical Logic 1997
Proof Theory of Modal Logic 1996
Formalizing the Dynamics of Information 2000
Games, Logic, and Constructive Sets 2003
Vicious Circles 1996
Studia Logica 1998
Thinking About Mathematics 2000
Machine Intelligence 1991
Logic and Computer Science 1990
The Journal of Symbolic Logic 1990-1991
Automated Reasoning with Analytic Tableaux and Related Methods 1997 May.
Logic Programming and Automated Response 1992 Jul.
Logic Colloquium 1990
Iterated Inductive Definitions and Subsystems of Analysis: Recent Proof-Theoretical Studies 1981
Logic Colloquium 1972-73
Proof Theory: An Introduction 1989
Logic, Methodology and Philosophy of Science VII 1986
Kreiseliana Abound and Around Georg Kreisel 1996
Pillars of Computer Science: Essays Dedicated to Boris (Boaz) Trakhtenbrot on the Occasion of His 85th Birthday 1998
Baltic Computer Science 1991
Computational Logic and Proof Theory 1993 Aug.
COLOG-88 1988 Dec.
Logic for Programming, Artificial Intelligence, and Reasoning 2006 Nov.
Correct Reasoning: Essays on Logic-Based AI in Honor of Vladmir Lifschitz 2012
Fields of Logic and Computation: Essays Dedicated to Yuri Gurevich on the Occasion of His 70th Birthday 2010
Computer Science - Theory and Applications 2006 Jun.
Locial Foundations of Computer Science 1997 Jul.
Logic Colloquium 1996
Logic, Language, Information and Computation 2011 May.
Reflections on the Foundations of Mathematics 2002
European Summer Meeting for the Association for Symbolic Logic 1996 Jul 9-15
Bulletin of the American Mathematical Society 1997 Apr.
PYC undated
PYC 0-T undated
PYC H undated
PYC ^M undated
PYC E-K undated
A undated
R undated
RUS AbB undated
Non-recursive functions, knots "with thick ropes" and self-clenching "thick" hyperspheres 1991
A Characterization Theorem for Geometric Logic 12/8/2009
OE3OP undated
About Sergei Yu Maslov undated
The Variety of Logical Hylomorphism undated
A Finite Model Theorem for the Propositional u-Calculus undated
Results on the Propositional u-Calculus undated
A Buchholz Rule for Modal fixed Point Logics undated
PhML 2014
Mathematics 21th Century PDMI 70th Anniversary 2010 Sep. 13-18
Kant's Theory of Judgment 4/23/2009
Epsilon Substitution for Predicate Logic undated
On Mints' Reduction for ccc-Calculus undated
Provable Isomorphisms of Types undated
Normal Forms and Cut-Free Proofs as Natural Transformations undated
On Gentzen's First Consistency Proof for Arithmetic 6/13/2012
On Gentzen's First Consistency Proof for Arithmetic (Revised) 3/10/2013
Structural Polymorphism 1993
Functional Polymorphism 1990
Proof search in multi-succeedent sequent calculi for intuitionistic logic undated
Proof Theory and Category Theory 1992
Proof Theory and Category Theory 2013 Jul. 24-27
Catbeam1 7/13/2013
A Reconstruction of Aristotle's Modal Syllogistic 9/9/2005
International Who's Who of Intellectuals undated
Sudoku undated
What is Truth? 4/4/2012
Register Machines undated
What is Truth Spring 2012
Manin, Mosogsky, etc. undated
MT2009 Dec. Theories 2009
Sasha 2008-2009
Comment tracer des diagrammes commutatifs? 6/24/2003
Kripke Models undated
A Short Introduction to Intuitionistic Logic undated
Rooted Frames, Partial Orders undated
Algebraic Models undatred
Topological Completeness undated
Epsilon Substitution for First- and Second-Order Predicate Logic 4/29/2011
Category Theory and Structural Proof Theory 10/27/2009
Introduction to Ergodic Theory Winter 1995
Comput. undated
Academies undated
Students 2009-2012
Seminars 2008-2009
LMH 2008-2009
Logteach 2011-2013
Kant undated
ID 2009
Estonian AS undated
Constructivity undated
Number Theory Winter 2007
The Indeterminacy of Set-Theoretic Notions undated
Confer undated
"What is Truth?" - Slides: Typos and other Observations 11/30/2013
Cantor's Disorganization Method undated
Introducing Topoi 10/18/2013
Second Order Arithmetic undated
American Academy of Arts & Sciences undated
Mathematics self-proves its own Consistency undated
O-minimal Structures - Phil350B Decidable Theories Autumn 2013
Grobner Bases 10/21/2013
Intuitionistic Hybrid Logic 4/1/2005
Intuitionistic Decision ProceduresGesamtersetzungen in Ackermanns Dissertation 10/8/2003
Univalent Foundations and the Structure Identity Principle 1/8/2013
Amalgation and Interpolation in Normal Modal Logics undated
Two Examples of Cut-Elimination for Non-classical Logics 12/13/2013
Latex undated
Submitted undated
Logic Seminar 2010
Additive Number Theory 2/7/2007
Strong Normalisation Theorem undated
Work of A.A. Markov on Stepwise Semantics of Constructive Mathematics undated
Memorandum of Agreement undated
Cut-elimination for the first order of e-calculus 10/27/1992
Ordinals from Above and Below, Part II 1/25/2011
PhML-14 undated
Invariants undated
QBF undated
Decomposing Two-Dimensional Permutations: A Three Layer Cryptoticon is Universal 8/27/2012
Carolyn undated
Kaht undated
Miscellaneous Documents undated
Proof T4 2010-2011
Intuitionistic Dual-intuistionistic Nets 2009
From Deep Inference to Proof Nets via Cut Elimination 2009
Eigenvalues, bracketing and the decidability of positive minimal intuitionistic logic undated
Transfinite Progressions: A Second Look at Completeness 2004
Functional Interpretations of Classical Systems undated
Godel incompleteness theorems and the limits of their applicability. 2010
Eskolemization in Intuitionistic Logic 2009
Tableaux and Hypersequents for Justification Logics 2011
Cut Elimination for Shallow Modal Logics 2011
Analytic Cut in Modal Logic: the System B 2011
Epsilon Substitution for First and Second Order Predicate Logic 4/29/2011
Proof TH 2010-2011
Philosophy, Mathematics, Linguistics: Aspects of Interaction 22-25 May, 2012
The Calculus Can Be Put to Work as Mathematics, not Formalism! 10/30/2012
Iterating Semantic Automata 9/3/2012
Common Law Reasoning undated
Modal Logic and Philosophy 2007
Epsilon of Fprints undated
Category Theory and Structured Proof Theory 11/9/2009
Equational/Categorical Axiomatizations of Primitive Recursive Functions and Functionals 11/10/2010
Strong Normalization with Permutative Conversions 11/16/2007
Epsilon Substitution for ID1 5/23/2009
Additive Number Theory 1/10/2007
Fitch's Paradox of Knowability 4/4/2004
First Steps in Modal Logic 12/4/2007
Catastrophic Second Step of Hilbert's Program 8/24/2012
Several Interesting Problems from Applied Logic 1/29/2013
Generalized Godel, Rosser, and Henkin Sentences undated
Epsilon Substitution for Predicate Logic 8/22/2010
Semantic Construction of Intuitionistic Logic undated
There is no 16-Clue Sudoku: Solving the Sudoku Minimum Number of Clues Problem 1/1/2012
Kolmogorov Complexity of Categories 1/8/2013
Justification of Tertium Non Datur Within Hilbert's Consistency Theory undated
Extension of Epsilon Substituition Method to ID1 6/22/2007
Recursively Mahlo Ordinals and Inductive Definitions undated
General Interest Topics in Mathematical Logic 11/18/2010
Non-Deterministic Epsilon Substituion Method for PA and ID1 7/13/2011
Annotated Bibliography on Decidability in Non-Clasical Systems undated
Craig's Interpolation Theorem for the Intuitionistic Logic and its Extensions - A Semantical Approach undated
Ordinals: Pohlers, Proof Theory 1989-1994
Renormalization and Computation 10/20/2009
Summary of Presentaions Given at the Stanford Logic Seminar 2007-2008
Simplified Strong Normalization Proof for Logic With Existence 6/6/1997
Non-Deterministic Epsilon Substituion Method for ID1: Effective Proof 1/20/2012
Idempotents in Compact Semigroups and Ramsey Theory undated
Report on Non-Deterministic Epsilopn Substitution for ID1: Effective Proof 2/5/2012
The Theory ID1 undated
Avron Hypersequent Calculus for Godal-Dummet Logic 8/24/2008
Review of Mathematical Logic undated
A Survey of Decidability Results in Non-Classical Logics 8/16/2011
Derivability of Modal Formulas Containing Only Positive Occurances of Quantifiers 8/9/2011
Generalized Kripke Forms 2006
CST undated
Notices of the American Mathematical Society 2014 Mar.
Notes on Constructive Negation 2006
No Plagiarism Here undated
Constructive Set Theory 1975 Sep.
PhML 2014
Proceedings of the Estonian Academy of Sciences 2014
Cut Elimination for tge Logic of Transivity and Density 5/6/2013
Compositional Semantics vs Arbitrary Syntax 9/27/2013
Semialgebraic and Subanalytic Geometry 3/2/2000
An introduction to o-minimal structures 9/3/1999
Pfaffian Sets and O-minimality 2012
Exponential Complexity of Satisfiability Testing for Linear-Size Boolean Formulas 2013
Satisfiability Certificates Verifiable in Subexponential Time 2011
A deterministic (2-2(k+1))^n algorithm for k-SAT based on local search 2002
Clause Shortening Combined with Pruning Yields a New Upper Bound for Deterministic SAT Algorithms 2006
MAX-SAT for Formulas with Constant Clause Density Can Be Solved Faster Than in O(2^n) Time 2006
Expressive Power and Data Complexity of Nonrecursive Query Languages for Lists and Trees 2000
On Moderately Exponential Time for SAT 2010
Simple Proof of Strong Normalization 6/20/2012
A Simple Strong Normalization Proof with Existence and Disjunction 12/11/2010
Simplified Strong Normalization Proof for Logic With Existence 11/3/1998
A Simple Strong Normalization Proof with Existence and Disjunction 8/23/2008
Dynamic Logics of Dynamical Systems undated
Proof Search in Multi-Succedent Sequent Calculi for Intuitionistic Logic 4/1/2014
Several Interesting Problems from Applied Logic 2014 Apr.
Notices of the American Mathematical Society 2014 Jan.
A Lower Bound for Intuitionistic Logic 1/25/2007
Implicit Definition and the Epistemology of Mathematics undated
Aristotle's Modal Proof Theory 2014 Mar. 4-6
Offprint from Oxford Studies in Ancient Philosophy Summer 2012
Additional papers Accession ARCH-2015-139
Grigori Mints memorial materials 2015
A Short Introduction to Modal Logic, by Grigori Mints 1992