127 research outputs found
Cut-elimination for the mu-calculus with one variable
No full textWe establish syntactic cut-elimination for the one-variable fragment of the modal mu-calculus. Our method is based on a recent cut-elimination technique by Mints that makes use of Buchholz' Omega-rule
Grigori Mints, a Proof Theorist in the USSR: Some Personal Recollections in a Scientific Context
No full textThe paper is based on my recollections of Grigori Mints (1939–2014) com-pleted by a survey of his research work in a scientific context. I speak mostly about the Soviet period of his life and work (until 1991), and sometimes go beyond the purely scientific aspects to show the atmosphere of these times
Decidability for Non-Standard Conversions in Typed Lambda-Calculi
No full textThis thesis studies the decidability of conversions in typed lambda-calculi, along with the algorithms allowing for this decidability. Our study takes in consideration conversions going beyond the traditional beta, eta, or permutative conversions (also called commutative conversions). To decide these conversions, two classes of algorithms compete, the algorithms based on rewriting, here the goal is to decompose and orient the conversion so as to obtain a convergent system, these algorithms then boil down to rewrite the terms until they reach an irreducible forms; and the "reduction free" algorithms where the conversion is decided recursively by a detour via a meta-language. Throughout this thesis, we strive to explain the latter thanks to the former
A proof of topological completeness for S4 in (0, 1)
No full textAbstractThe completeness of the modal logic S4 for all topological spaces as well as for the real line R, the n-dimensional Euclidean space Rn and the segment (0, 1) etc. (with □ interpreted as interior) 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 K for S4 into a subspace of the Cantor space which in turn encodes (0, 1). This provides an open and continuous map from (0, 1) onto the topological space corresponding to K. The completeness follows as S4 is complete with respect to the class of all finite rooted Kripke structures
Cut-free formulations for a quantified logic of here and there
No full textAbstractA 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 (here and there) 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 conservative extension of the logic of weak excluded middle with respect to sequents without positive occurrences of implication. The completeness proof uses a non-closed branch of a proof search tree. The interplay between rules for pushing negation inside and truth in the “there” (non-root) world of the resulting Kripke model can be of independent interest. We prove that existence is definable in terms of remaining connectives
- …
