Order:
Disambiguations
Grigori Mints [38]G. Mints [18]G. E. Mints [12]Giorgi Mints [2]
Grigori Efroimovich Mints [2]
  1.  61
    Dynamic topological logic.Philip Kremer & Grigori Mints - 2005 - Annals of Pure and Applied Logic 131 (1-3):133-158.
    Dynamic topological logic provides a context for studying the confluence of the topological semantics for S4, topological dynamics, and temporal logic. The topological semantics for S4 is based on topological spaces rather than Kripke frames. In this semantics, □ is interpreted as topological interior. Thus S4 can be understood as the logic of topological spaces, and □ can be understood as a topological modality. Topological dynamics studies the asymptotic properties of continuous maps on topological spaces. Let a dynamic topological system (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   36 citations  
  2.  16
    Dynamic topological logic.Philip Kremer & Giorgi Mints - 2005 - Annals of Pure and Applied Logic 131 (1-3):133-158.
    Dynamic topological logic provides a context for studying the confluence of the topological semantics for S4, topological dynamics, and temporal logic. The topological semantics for S4 is based on topological spaces rather than Kripke frames. In this semantics, □ is interpreted as topological interior. Thus S4 can be understood as the logic of topological spaces, and □ can be understood as a topological modality. Topological dynamics studies the asymptotic properties of continuous maps on topological spaces. Let a dynamic topological system (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   34 citations  
  3.  43
    Epsilon substitution method for elementary analysis.Grigori Mints, Sergei Tupailo & Wilfried Buchholz - 1996 - Archive for Mathematical Logic 35 (2):103-130.
    We formulate epsilon substitution method for elementary analysisEA (second order arithmetic with comprehension for arithmetical formulas with predicate parameters). Two proofs of its termination are presented. One uses embedding into ramified system of level one and cutelimination for this system. The second proof uses non-effective continuity argument.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   23 citations  
  4.  45
    Indexed systems of sequents and cut-elimination.Grigori Mints - 1997 - Journal of Philosophical Logic 26 (6):671-696.
    Cut reductions are defined for a Kripke-style formulation of modal logic in terms of indexed systems of sequents. A detailed proof of the normalization (cutelimination) theorem is given. The proof is uniform for the propositional modal systems with all combinations of reflexivity, symmetry and transitivity for the accessibility relation. Some new transformations of derivations (compared to standard sequent formulations) are needed, and some additional properties are to be checked. The display formulations [1] of the systems considered can be presented as (...)
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   23 citations  
  5.  35
    A Short Introduction to Modal Logic.Grigori Mints - 1992 - Stanford, CA, USA: Center for the Study of Language and Information.
    A Short Introduction to Modal Logic presents both semantic and syntactic features of the subject and illustrates them by detailed analyses of the three best-known modal systems S5, S4 and T. The book concentrates on the logical aspects of ...
    Direct download  
     
    Export citation  
     
    Bookmark   9 citations  
  6.  37
    Cut elimination for a simple formulation of epsilon calculus.Grigori Mints - 2008 - Annals of Pure and Applied Logic 152 (1):148-160.
    A simple cut elimination proof for arithmetic with the epsilon symbol is used to establish the termination of a modified epsilon substitution process. This opens a possibility of extension to much stronger systems.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   7 citations  
  7.  32
    A proof of topological completeness for S4 in.Grigori Mints & Ting Zhang - 2005 - Annals of Pure and Applied Logic 133 (1-3):231-245.
    The completeness of the modal logic S4 for all topological spaces as well as for the real line , the n-dimensional Euclidean space and the segment etc. was proved by McKinsey and Tarski in 1944. Several simplified proofs contain gaps. A new proof presented here combines the ideas published later by G. Mints and M. Aiello, J. van Benthem, G. Bezhanishvili with a further simplification. The proof strategy is to embed a finite rooted Kripke structure for S4 into a subspace (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   8 citations  
  8.  30
    The complexity of the disjunction and existential properties in intuitionistic logic.Sam Buss & Grigori Mints - 1999 - Annals of Pure and Applied Logic 99 (1-3):93-104.
    This paper considers the computational complexity of the disjunction and existential properties of intuitionistic logic. We prove that the disjunction property holds feasibly for intuitionistic propositional logic; i.e., from a proof of A v B, a proof either of A or of B can be found in polynomial time. For intuitionistic predicate logic, we prove superexponential lower bounds for the disjunction property, namely, there is a superexponential lower bound on the time required, given a proof of A v B, to (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   8 citations  
  9. Axiomatizing the next-interior fragment of dynamic topological logic.Philip Kremer, Grigori Mints & V. Rybakov - 1997 - Bulletin of Symbolic Logic 3:376-377.
  10.  34
    Epsilon substitution for first- and second-order predicate logic.Grigori Mints - 2013 - Annals of Pure and Applied Logic 164 (6):733-739.
    The epsilon substitution method was proposed by D. Hilbert as a tool for consistency proofs. A version for first order predicate logic had been described and proved to terminate in the monograph “Grundlagen der Mathematik”. As far as the author knows, there have been no attempts to extend this approach to the second order case. We discuss possible directions for and obstacles to such extensions.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  11.  45
    Propositional logic of continuous transformations in Cantor space.Grigori Mints & Ting Zhang - 2005 - Archive for Mathematical Logic 44 (6):783-799.
  12.  27
    Linear lambda-terms and natural deduction.G. Mints - 1998 - Studia Logica 60 (1):209-231.
  13.  96
    Proof theory in the USSR 1925–1969.Grigori Mints - 1991 - Journal of Symbolic Logic 56 (2):385-424.
    We present a survey of proof theory in the USSR beginning with the paper by Kolmogorov [1925] and ending (mostly) in 1969; the last two sections deal with work done by A. A. Markov and N. A. Shanin in the early seventies, providing a kind of effective interpretation of negative arithmetic formulas. The material is arranged in chronological order and subdivided according to topics of investigation. The exposition is more detailed when the work is little known in the West or (...)
    Direct download (7 more)  
     
    Export citation  
     
    Bookmark   6 citations  
  14. Epsilon-substitution method for the ramified language and Δ 1 1 -comprehension rule.Grigori Mints & S. Tupailo - 1999 - In ¸ Itecantini1999. Springer.
     
    Export citation  
     
    Bookmark   5 citations  
  15. Strong termination for the epsilon substitution method.Grigori Mints - 1996 - Journal of Symbolic Logic 61 (4):1193-1205.
    Ackermann proved termination for a special order of reductions in Hilbert's epsilon substitution method for the first order arithmetic. We establish termination for arbitrary order of reductions.
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  16. Thoralf Skolem and the epsilon substitution method for predicate logic.Grigori Mints - 1996 - Nordic Journal of Philosophical Logic 1 (2):133-146.
  17.  12
    Failure of interpolation in constant domain intuitionistic logic.Grigori Mints, Grigory Olkhovikov & Alasdair Urquhart - 2013 - Journal of Symbolic Logic 78 (3):937-950.
  18.  5
    Non-Deterministic Epsilon Substitution for ID1: Effective Proof.Grigori Mints - 2012 - In Ulrich Berger, Hannes Diener, Peter Schuster & Monika Seisenberger (eds.), Logic, Construction, Computation. De Gruyter. pp. 325-342.
    No categories
    Direct download  
     
    Export citation  
     
    Bookmark   2 citations  
  19.  17
    A simple proof of second-order strong normalization with permutative conversions.Makoto Tatsuta & Grigori Mints - 2005 - Annals of Pure and Applied Logic 136 (1-2):134-155.
    A simple and complete proof of strong normalization for first- and second-order intuitionistic natural deduction including disjunction, first-order existence and permutative conversions is given. The paper follows the Tait–Girard approach via computability predicates and saturated sets. Strong normalization is first established for a set of conversions of a new kind, then deduced for the standard conversions. Difficulties arising for disjunction are resolved using a new logic where disjunction is restricted to atomic formulas.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  20.  17
    The completeness of provable realizability.G. E. Mints - 1989 - Notre Dame Journal of Formal Logic 30 (3):420-441.
  21.  11
    A normal form for logical derivations implying one for arithmetic derivations.G. Mints - 1993 - Annals of Pure and Applied Logic 62 (1):65-79.
    We describe a short model-theoretic proof of an extended normal form theorem for derivations in predicate logic which implies in PRA a normal form theorem for the arithmetic derivations . Consider the Gentzen-type formulation of predicate logic with invertible rules. A derivation with proper variables is one where a variable b can occur in the premiss of an inference L but not below this premiss only in the case when L is () or () and b is its eigenvariable. Free (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  22.  53
    Normal deduction in the intuitionistic linear logic.G. Mints - 1998 - Archive for Mathematical Logic 37 (5-6):415-425.
    We describe a natural deduction system NDIL for the second order intuitionistic linear logic which admits normalization and has a subformula property. NDIL is an extension of the system for !-free multiplicative linear logic constructed by the author and elaborated by A. Babaev. Main new feature here is the treatment of the modality !. It uses a device inspired by D. Prawitz' treatment of S4 combined with a construction $<\Gamma>$ introduced by the author to avoid cut-like constructions used in $\otimes$ (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  23.  15
    The logic of transitive and dense frames: from the step-frame analysis to full cut-elimination.S. Ghilardi & G. Mints - 2014 - Logic Journal of the IGPL 22 (4):585-596.
  24.  88
    Cut-elimination for simple type theory with an axiom of choice.G. Mints - 1999 - Journal of Symbolic Logic 64 (2):479-485.
    We present a cut-elimination proof for simple type theory with an axiom of choice formulated in the language with an epsilon-symbol. The proof is modeled after Takahashi's proof of cut-elimination for simple type theory with extensionality. The same proof works when types are restricted, for example for second-order classical logic with an axiom of choice.
    Direct download (7 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  25.  31
    Interpolation theorems for intuitionistic predicate logic.G. Mints - 2001 - Annals of Pure and Applied Logic 113 (1-3):225-242.
    Craig interpolation theorem implies that the derivability of X,X′ Y′ implies existence of an interpolant I in the common language of X and X′ Y′ such that both X I and I,X′ Y′ are derivable. For classical logic this extends to X,X′ Y,Y′, but for intuitionistic logic there are counterexamples. We present a version true for intuitionistic propositional logic, and more complicated version for the predicate case.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  26.  4
    Variation in the deduction search tactics in sequential calculi.G. E. Mints - 1969 - In A. O. Slisenko (ed.), Studies in constructive mathematics and mathematical logic. New York,: Consultants Bureau. pp. 52--59.
    Direct download  
     
    Export citation  
     
    Bookmark   2 citations  
  27. Notes on Constructive Negation.Grigori Mints - 2006 - Synthese 148 (3):701-717.
    We put together several observations on constructive negation. First, Russell anticipated intuitionistic logic by clearly distinguishing propositional principles implying the law of the excluded middle from remaining valid principles. He stated what was later called Peirce’s law. This is important in connection with the method used later by Heyting for developing his axiomatization of intuitionistic logic. Second, a work by Dragalin and his students provides easy embeddings of classical arithmetic and analysis into intuitionistic negationless systems. In the last section, we (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  28.  29
    Effective Cut-elimination for a Fragment of Modal mu-calculus.Grigori Mints - 2012 - Studia Logica 100 (1-2):279-287.
    A non-effective cut-elimination proof for modal mu-calculus has been given by G. Jäger, M. Kretz and T. Studer. Later an effective proof has been given for a subsystem M 1 with non-iterated fixpoints and positive endsequents. Using a new device we give an effective cut-elimination proof for M 1 without restriction to positive sequents.
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  29.  19
    An extension of the omega-rule.Ryota Akiyoshi & Grigori Mints - 2016 - Archive for Mathematical Logic 55 (3-4):593-603.
    The Ω\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\Omega $$\end{document}-rule was introduced by W. Buchholz to give an ordinal-free proof of cut-elimination for a subsystem of analysis with Π11\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\Pi ^{1}_{1}$$\end{document}-comprehension. W. Buchholz’s proof provides cut-free derivations by familiar rules only for arithmetical sequents. When second-order quantifiers are present, they are introduced by the Ω\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\Omega $$\end{document}-rule and some residual cuts are not (...)
    No categories
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  30.  45
    In Memoriam: Albert G. Dragalin 1941–1998.S. Artemov, B. Kushner, G. Mints, E. Nogina & A. Troelstra - 1999 - Bulletin of Symbolic Logic 5 (3):389-391.
  31.  14
    Preface.Sergei Artemov, Yuri Matiyasevich, Grigori Mints & Anatol Slissenko - 2010 - Annals of Pure and Applied Logic 162 (3):173-174.
  32. Kearnes, KA, Kiss, EW and Valeriote, MA, A geometric.M. Borisavljevit, S. Buss, G. Mints, T. Coquand, A. A. Ivanov & D. Macpherson - 1999 - Annals of Pure and Applied Logic 99:261.
     
    Export citation  
     
    Bookmark  
  33.  45
    2000-2001 Spring Meeting of the Association for Symbolic Logic.Michael Detlefsen, Erich Reck, Colin McLarty, Rohit Parikh, Larry Moss, Scott Weinstein, Gabriel Uzquiano, Grigori Mints & Richard Zach - 2001 - Bulletin of Symbolic Logic 7 (3):413-419.
  34.  11
    Logic Colloquium ’96: Proceedings of the Colloquium held in San Sebastián, Spain, July 9–15, 1996.Jesus M. Larrazabal, Daniel Lascar & Grigori Mints - 1998 - Springer.
    The 1996 European Summer Meeting of the Association of Symbolic Logic was held held the University of the Basque Country, at Donostia (San Se bastian) Spain, on July 9-15, 1996. It was organised by the Institute for Logic, Cognition, Language and Information (ILCLI) and the Department of Logic and Philosophy of Sciences of the University of the Basque Coun try. It was supported by: the University of Pais Vasco/Euskal Herriko Unib ertsitatea, the Ministerio de Education y Ciencia (DGCYT), Hezkuntza Saila (...)
    Direct download  
     
    Export citation  
     
    Bookmark  
  35. Matematicheskai︠a︡ logika: katalog zarubezhnykh knig Biblioteki Akademii nauk SSSR, 1950-1971 gg.I. A. Lifshits, G. E. Mints & Akademiia Nauk Sssr - 1974 - Leningrad: Biblioteka Akademii nauk SSSR. Edited by G. E. Mint︠s︡.
    No categories
     
    Export citation  
     
    Bookmark  
  36.  5
    COLOG-88: International Conference on Computer Logic, Tallinn, USSR, December 12-16, 1988, Proceedings.Per Martin-Löf & Grigori Mints - 1990 - Springer Verlag.
    This volume contains several invited papers as well as a selection of the other contributions. The conference was the first meeting of the Soviet logicians interested in com- puter science with their Western counterparts. The papers report new results and techniques in applications of deductive systems, deductive program synthesis and analysis, computer experiments in logic related fields, theorem proving and logic programming. It provides access to intensive work on computer logic both in the USSR and in Western countries.
    Direct download  
     
    Export citation  
     
    Bookmark  
  37.  10
    Mechanical Proof-Search and the Theory of Logical Deduction in the Ussr.S. J. Maslov, G. E. Mints & V. P. Orevkov - 1971 - Revue Internationale de Philosophie 25 (4=98):575-584.
    A survey of works on automatic theorem-proving in the ussr 1964-1970. the philosophical problems are not touched.
    Direct download  
     
    Export citation  
     
    Bookmark   1 citation  
  38.  13
    Analog of Herbrand's Theorem for Prenex Formulas of Constructive Predicate Calculus.G. E. Mints - 1969 - Journal of Symbolic Logic 36 (3):47--51.
  39.  61
    Cut Elimination for S4C: A Case Study.Grigori Mints - 2006 - Studia Logica 82 (1):121-132.
    S4C is a logic of continuous transformations of a topological space. Cut elimination for it requires new kind of rules and new kinds of reductions.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
  40.  17
    Cut-free formulations for a quantified logic of here and there.Grigori Mints - 2010 - Annals of Pure and Applied Logic 162 (3):237-242.
    A predicate extension SQHT= of the logic of here-and-there was introduced by V. Lifschitz, D. Pearce, and A. Valverde to characterize strong equivalence of logic programs with variables and equality with respect to stable models. The semantics for this logic is determined by intuitionistic Kripke models with two worlds with constant individual domain and decidable equality. Our sequent formulation has special rules for implication and for pushing negation inside formulas. The soundness proof allows us to establish that SQHT= is a (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  41.  10
    Choice of terms in quantifier rules of constructive predicate calculus.G. E. Mints - 1969 - Journal of Symbolic Logic 36 (3):43--46.
  42. Donostia-San Sebastián, Spain, July 9–15, 1996.G. Mints, M. Otero, S. Ronchi Della Rocca & K. Segerberg - 1997 - Bulletin of Symbolic Logic 3 (2).
  43.  14
    1996 European Summer Meeting of the Association for Symbolic Logic.G. Mints, M. Otero, S. Ronchi Della Rocca & K. Segerberg - 1997 - Bulletin of Symbolic Logic 3 (2):242-277.
  44.  4
    Games, Logic, and Constructive Sets.Grigori Mints & Reinhard Muskens (eds.) - 2003 - Center for the Study of Language and Inf.
    Mathematical game theory has been embraced by a variety of scholars: social scientists, biologists, linguists, and now, increasingly, logicians. This volume illustrates the recent advances of game theory in the field. Logicians benefit from things like game theory's ability to explain informational independence between connectives; meanwhile, game theorists have even begun to benefit from logical epistemic analyses of game states. In concert with such pioneering work, this volume also present surprising developments in classical fields, including first-order logic and set theory.
    Direct download  
     
    Export citation  
     
    Bookmark  
  45. ¸ Itecantini1999.Grigori Mints & S. Tupailo - 1999 - Springer.
    No categories
     
    Export citation  
     
    Bookmark  
  46.  5
    Imbedding operations associated with Kripke's “semantics”.G. E. Mints - 1969 - In A. O. Slisenko (ed.), Studies in constructive mathematics and mathematical logic. New York,: Consultants Bureau. pp. 60--63.
  47.  24
    Journal of Soviet Mathematics.G. E. Mints, U. V. Matiasevic, A. O. Slisenko, Justus Diller & Martin Stein - 1987 - Journal of Symbolic Logic 52 (2):561-561.
    Direct download  
     
    Export citation  
     
    Bookmark  
  48.  9
    On Imbedding Operators.G. E. Mints & V. P. Orevkov - 1969 - In A. O. Slisenko (ed.), Studies in constructive mathematics and mathematical logic. New York,: Consultants Bureau. pp. 64--66.
  49.  44
    Resolution calculus for the first order linear logic.Grigori Mints - 1993 - Journal of Logic, Language and Information 2 (1):59-83.
    This paper presents a formulation and completeness proof of the resolution-type calculi for the first order fragment of Girard's linear logic by a general method which provides the general scheme of transforming a cutfree Gentzen-type system into a resolution type system, preserving the structure of derivations. This is a direct extension of the method introduced by Maslov for classical predicate logic. Ideas of the author and Zamov are used to avoid skolomization. Completeness of strategies is first established for the Gentzen-type (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  50.  11
    Reduction of finite and infinite derivations.G. Mints - 2000 - Annals of Pure and Applied Logic 104 (1-3):167-188.
    We present a general schema of easy normalization proofs for finite systems S like first-order arithmetic or subsystems of analysis, which have good infinitary counterparts S ∞ . We consider a new system S ∞ + with essentially the same rules as S ∞ but different derivable objects: a derivation d∈S ∞ + of a sequent Γ contains a derivation Φ∈S of Γ . Three simple conditions on Φ including a normal form theorem for S ∞ + easily imply a (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
1 — 50 / 66