Showing 1–7 of 7 results for author: Gencer, C

Intuitionistic modal logics: new and simpler decidability proofs for FIK and LIK

Authors: Philippe Balbiani, Cigdem Gencer

Abstract: In this note, by integrating ideas concerning terminating tableaux-based procedures in modal logics and finite frame property of intuitionistic modal logic IK, we provide new and simpler decidability proofs for FIK and LIK. In this note, by integrating ideas concerning terminating tableaux-based procedures in modal logics and finite frame property of intuitionistic modal logic IK, we provide new and simpler decidability proofs for FIK and LIK. △ Less

Submitted 24 March, 2025; originally announced March 2025.

Intuitionistic modal logics: a minimal setting

Authors: Philippe Balbiani, Çigdem Gencer

Abstract: We introduce an intuitionistic modal logic strictly contained in the intuitionistic modal logic IK and being an appropriate candidate for the title of ``minimal normal intuitionistic modal logic''. We introduce an intuitionistic modal logic strictly contained in the intuitionistic modal logic IK and being an appropriate candidate for the title of ``minimal normal intuitionistic modal logic''. △ Less

Submitted 26 February, 2025; originally announced February 2025.

Local Intuitionistic Modal Logics and Their Calculi

Authors: Philippe Balbiani, Han Gao, Çiğdem Gencer, Nicola Olivetti

Abstract: We investigate intuitionistic modal logics with locally interpreted $\square$ and $\lozenge$. The basic logic LIK is stronger than constructive modal logic WK and incomparable with intuitionistic modal logic IK. We propose an axiomatization of LIK and some of its extensions. We propose bi-nested calculi for LIK and these extensions, thus providing both a decision procedure and a procedure of finit… ▽ More We investigate intuitionistic modal logics with locally interpreted $\square$ and $\lozenge$. The basic logic LIK is stronger than constructive modal logic WK and incomparable with intuitionistic modal logic IK. We propose an axiomatization of LIK and some of its extensions. We propose bi-nested calculi for LIK and these extensions, thus providing both a decision procedure and a procedure of finite countermodel extraction. △ Less

Submitted 11 March, 2024; originally announced March 2024.

A Natural Intuitionistic Modal Logic: Axiomatization and Bi-nested Calculus

Authors: Philippe Balbiani, Han Gao, Çiğdem Gencer, Nicola Olivetti

Abstract: We introduce FIK, a natural intuitionistic modal logic specified by Kripke models satisfying the condition of forward confluence. We give a complete Hilbert-style axiomatization of this logic and propose a bi-nested calculus for it. The calculus provides a decision procedure as well as a countermodel extraction: from any failed derivation of a given formula, we obtain by the calculus a finite coun… ▽ More We introduce FIK, a natural intuitionistic modal logic specified by Kripke models satisfying the condition of forward confluence. We give a complete Hilbert-style axiomatization of this logic and propose a bi-nested calculus for it. The calculus provides a decision procedure as well as a countermodel extraction: from any failed derivation of a given formula, we obtain by the calculus a finite countermodel of it. △ Less

Submitted 12 September, 2023; originally announced September 2023.

Hazelcast Jet: Low-latency Stream Processing at the 99.99th Percentile

Authors: Can Gencer, Marko Topolnik, Viliam Ďurina, Emin Demirci, Ensar B. Kahveci, Ali Gürbüz Ondřej Lukáš, József Bartók, Grzegorz Gierlach, František Hartman, Ufuk Yılmaz, Mehmet Doğan, Mohamed Mandouh, Marios Fragkoulis, Asterios Katsifodimos

Abstract: Jet is an open-source, high-performance, distributed stream processor built at Hazelcast during the last five years. Jet was engineered with millisecond latency on the 99.99th percentile as its primary design goal. Originally Jet's purpose was to be an execution engine that performs complex business logic on top of streams generated by Hazelcast's In-memory Data Grid (IMDG): a set of high-performa… ▽ More Jet is an open-source, high-performance, distributed stream processor built at Hazelcast during the last five years. Jet was engineered with millisecond latency on the 99.99th percentile as its primary design goal. Originally Jet's purpose was to be an execution engine that performs complex business logic on top of streams generated by Hazelcast's In-memory Data Grid (IMDG): a set of high-performance, in-memory, partitioned and replicated data structures. With time, Jet evolved into a full-fledged, scale-out stream processor that can handle out-of-order streams and exactly-once processing guarantees. Jet's end-to-end latency lies in the order of milliseconds, and its throughput in the order of millions of events per CPU-core. This paper presents main design decisions we made in order to maximize the performance per CPU-core, alongside lessons learned, and an empirical performance evaluation. △ Less

Submitted 18 March, 2021; originally announced March 2021.

About the unification types of the modal logics determined by classes of deterministic frames

Authors: Philippe Balbiani, Çiğdem Gencer, Maryam Rostamigiv, Tinko Tinchev

Abstract: The unification problem in a propositional logic is to determine, given a formula F, whether there exists a substitution s such that s(F) is in that logic. In that case, s is a unifier of F. When a unifiable formula has minimal complete sets of unifiers, the formula is either infinitary, finitary, or unitary, depending on the cardinality of its minimal complete sets of unifiers. In this paper, we… ▽ More The unification problem in a propositional logic is to determine, given a formula F, whether there exists a substitution s such that s(F) is in that logic. In that case, s is a unifier of F. When a unifiable formula has minimal complete sets of unifiers, the formula is either infinitary, finitary, or unitary, depending on the cardinality of its minimal complete sets of unifiers. In this paper, we study the unification types of some modal logics determined by classes of deterministic frames. △ Less

Submitted 16 April, 2020; originally announced April 2020.

About the unification type of simple symmetric modal logics

Authors: Philippe Balbiani, Çiğdem Gencer

Abstract: The unification problem in a normal modal logic is to determine, given a formula F, whether there exists a substitution s such that s(F) is in that logic. In that case, s is a unifier of F. We shall say that a set of unifiers of a unifiable formula F is complete if for all unifiers s of F, there exists a unifier t of F in that set such that t is more general than s. When a unifiable formula has no… ▽ More The unification problem in a normal modal logic is to determine, given a formula F, whether there exists a substitution s such that s(F) is in that logic. In that case, s is a unifier of F. We shall say that a set of unifiers of a unifiable formula F is complete if for all unifiers s of F, there exists a unifier t of F in that set such that t is more general than s. When a unifiable formula has no minimal complete set of unifiers, the formula is nullary. In this paper, we prove that KB, KDB and KTB possess nullary formulas. △ Less

Submitted 11 February, 2019; originally announced February 2019.