Searcharxiv⌕ Search

arXiv subjects

Emil Jeřábek

Publications and source records attributed to Emil Jeřábek.

28 records · Page 2Linked to original sources
arXiv2015

Integer factoring and modular square roots

Buresh-Oppenheim proved that the NP search problem to find nontrivial factors of integers of a special form belongs to Papadimitriou's class PPA, and is probabilistically reducible to a problem in PPP. In this paper, we use ideas from bounded arithmetic to extend these results to arbitrary integers. We show that general integer factoring is reducible in randomized polynomial time to a PPA problem and to the problem WEAKPIGEON in PPP. Both reductions can be derandomized under the assumption of the generalized Riemann hypothesis. We also show (unconditionally) that PPA contains some related problems, such as square root computation modulo n, and finding quadratic nonresidues modulo n.

cs.CC↗
arXiv2015

Rules with parameters in modal logic I

We study admissibility of inference rules and unification with parameters in transitive modal logics (extensions of K4), in particular we generalize various results on parameter-free admissibility and unification to the setting with parameters. Specifically, we give a characterization of projective formulas generalizing Ghilardi's characterization in the parameter-free case, leading to new proofs of Rybakov's results that admissibility with parameters is decidable and unification is finitary for logics satisfying suitable frame extension properties (called cluster-extensible logics in this paper). We construct explicit bases of admissible rules with parameters for cluster-extensible logics, and give their semantic description. We show that in the case of finitely many parameters, these logics have independent bases of admissible rules, and determine which logics have finite bases. As a sideline, we show that cluster-extensible logics have various nice properties: in particular, they are finitely axiomatizable, and have an exponential-size model property. We also give a rather general characterization of logics with directed (filtering) unification. In the sequel, we will use the same machinery to investigate the computational complexity of admissibility and unification with parameters in cluster-extensible logics, and we will adapt the results to logics with unique top cluster (e.g., S4.2) and superintuitionistic logics.

cs.LO↗
arXiv2014

Open induction in a bounded arithmetic for TC^0

The elementary arithmetic operations $+,\cdot,\le$ on integers are well-known to be computable in the weak complexity class $\mathrm{TC}^0$, and it is a basic question what properties of these operations can be proved using only $\mathrm{TC}^0$-computable objects, i.e., in a theory of bounded arithmetic corresponding to $\mathrm{TC}^0$. We will show that the theory $\mathit{VTC}^0$ extended with an axiom postulating the totality of iterated multiplication (which is computable in $\mathrm{TC}^0$) proves induction for quantifier-free formulas in the language $\langle +,\cdot,\le \rangle$ (IOpen), and more generally, minimization for $Σ^b_0$ formulas in the language of Buss's $S_2$.

cs.LO↗
arXiv2013

Blending margins: The modal logic K has nullary unification type

We investigate properties of the formula $p \to \Box p$ in the basic modal logic K. We show that K satisfies an infinitary weaker variant of the rule of margins $ϕ\to \Boxϕ/ ϕ, \negϕ$, and as a consequence, we obtain various negative results about admissibility and unification in K. We describe a complete set of unifiers (i.e., substitutions making the formula provable) of $p \to \Box p$, and use it to establish that K has the worst possible unification type: nullary. In well-behaved transitive modal logics, admissibility and unification can be analyzed in terms of projective formulas, introduced by Ghilardi; in particular, projective formulas coincide for these logics with formulas that are admissibly saturated (i.e., derive all their multiple-conclusion admissible consequences) or exact (i.e., axiomatize a theory of a substitution). In contrast, we show that in K, the formula $p \to \Box p$ is admissibly saturated, but neither projective nor exact. All our results for K also apply to the basic description logic ALC.

cs.LO↗
arXiv2013

Cluster expansion and the boxdot conjecture

The boxdot conjecture asserts that every normal modal logic that faithfully interprets T by the well-known boxdot translation is in fact included in T. We confirm that the conjecture is true. More generally, we present a simple semantic condition on modal logics $L_0$ which ensures that the largest logic where $L_0$ embeds faithfully by the boxdot translation is $L_0$ itself. In particular, this natural generalization of the boxdot conjecture holds for S4, S5, and KTB in place of T.

math.LO↗
arXiv2012

Root finding with threshold circuits

We show that for any constant d, complex roots of degree d univariate rational (or Gaussian rational) polynomials---given by a list of coefficients in binary---can be computed to a given accuracy by a uniform TC^0 algorithm (a uniform family of constant-depth polynomial-size threshold circuits). The basic idea is to compute the inverse function of the polynomial by a power series. We also discuss an application to the theory VTC^0 of bounded arithmetic.

cs.DS↗
arXiv2012

The ubiquity of conservative translations

We study the notion of conservative translation between logics introduced by Feitosa and D'Ottaviano. We show that classical propositional logic (CPC) is universal in the sense that every finitary consequence relation over a countable set of formulas can be conservatively translated into CPC. The translation is computable if the consequence relation is decidable. More generally, we show that one can take instead of CPC a broad class of logics (extensions of a certain fragment of full Lambek calculus FL) including most nonclassical logics studied in the literature, hence in a sense, (almost) any two reasonable deductive systems can be conservatively translated into each other. We also provide some counterexamples, in particular the paraconsistent logic LP is not universal.

math.LO↗
arXiv2012

The complexity of admissible rules of Łukasiewicz logic

We investigate the computational complexity of admissibility of inference rules in infinite-valued Łukasiewicz propositional logic (Ł). It was shown in [13] that admissibility in Ł is checkable in PSPACE. We establish that this result is optimal, i.e., admissible rules of Ł are PSPACE-complete. In contrast, derivable rules of Ł are known to be coNP-complete.

cs.LO↗
arXiv2012

Sequence encoding without induction

We show that the universally axiomatized, induction-free theory PA^- is a sequential theory in the sense of Pudlák [5], in contrast to the closely related Robinson's arithmetic.

math.LO↗