Search Results

Documents authored by Grigoriev, Dima

Document
DOI: 10.4230/LIPIcs.STACS.2025.8
Tropical Proof Systems: Between R(CP) and Resolution

Authors: Yaroslav Alekseev, Dima Grigoriev, and Edward A. Hirsch

Published in: LIPIcs, Volume 327, 42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025)

Abstract
Propositional proof complexity deals with the lengths of polynomial-time verifiable proofs for Boolean tautologies. An abundance of proof systems is known, including algebraic and semialgebraic systems, which work with polynomial equations and inequalities, respectively. The most basic algebraic proof system is based on Hilbert’s Nullstellensatz [Paul Beame et al., 1996]. Tropical ("min-plus") arithmetic has many applications in various areas of mathematics. The operations are the real addition (as the tropical multiplication) and the minimum (as the tropical addition). Recently, [Bertram and Easton, 2017; Dima Grigoriev and Vladimir V. Podolskii, 2018; Joo and Mincheva, 2018] demonstrated a version of Nullstellensatz in the tropical setting. In this paper we introduce (semi)algebraic proof systems that use min-plus arithmetic. For the dual-variable encoding of Boolean variables (two tropical variables x and x ̅ per one Boolean variable x) and {0,1}-encoding of the truth values, we prove that a static (Nullstellensatz-based) tropical proof system polynomially simulates daglike resolution and also has short proofs for the propositional pigeon-hole principle. Its dynamic version strengthened by an additional derivation rule (a tropical analogue of resolution by linear inequality) is equivalent to the system Res(LP) (aka R(LP)), which derives nonnegative linear combinations of linear inequalities; this latter system is known to polynomially simulate Krajíček’s Res(CP) (aka R(CP)) with unary coefficients. Therefore, tropical proof systems give a finer hierarchy of proof systems below Res(LP) for which we still do not have exponential lower bounds. While the "driving force" in Res(LP) is resolution by linear inequalities, dynamic tropical systems are driven solely by the transitivity of the order, and static tropical proof systems are based on reasoning about differences between the input linear functions. For the truth values encoded by {0,∞}, dynamic tropical proofs are equivalent to Res(∞), which is a small-depth Frege system called also DNF resolution. Finally, we provide a lower bound on the size of derivations of a much simplified tropical version of the {Binary Value Principle} in a static tropical proof system. Also, we establish the non-deducibility of the tropical resolution rule in this system and discuss axioms for Boolean logic that do not use dual variables. In this extended abstract, full proofs are omitted.
Cite as

Yaroslav Alekseev, Dima Grigoriev, and Edward A. Hirsch. Tropical Proof Systems: Between R(CP) and Resolution. In 42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 327, pp. 8:1-8:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{alekseev_et_al:LIPIcs.STACS.2025.8,
  author =	{Alekseev, Yaroslav and Grigoriev, Dima and Hirsch, Edward A.},
  title =	{{Tropical Proof Systems: Between R(CP) and Resolution}},
  booktitle =	{42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025)},
  pages =	{8:1--8:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-365-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{327},
  editor =	{Beyersdorff, Olaf and Pilipczuk, Micha{\l} and Pimentel, Elaine and Thắng, Nguy\~{ê}n Kim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2025.8},
  URN =		{urn:nbn:de:0030-drops-228332},
  doi =		{10.4230/LIPIcs.STACS.2025.8},
  annote =	{Keywords: Cutting Planes, Nullstellensatz refutations, Res(CP), semi-algebraic proofs, tropical proof systems, tropical semiring}
}
Document
DOI: 10.4230/DagRep.6.11.168
Algorithms and Effectivity in Tropical Mathematics and Beyond (Dagstuhl Seminar 16482)

Authors: Stéphane Gaubert, Dima Grigoriev, Michael Joswig, and Thorsten Theobald

Published in: Dagstuhl Reports, Volume 6, Issue 11 (2017)

Abstract
This report documents the Dagstuhl Seminar on Algorithms and Effectivity in Tropical Mathematics and Beyond, which took place from November 27 -- December 02, 2016. The report contains an executive summary as well as abstracts of the talks which reflect recent progress in the topic of the meeting.
Cite as

Stéphane Gaubert, Dima Grigoriev, Michael Joswig, and Thorsten Theobald. Algorithms and Effectivity in Tropical Mathematics and Beyond (Dagstuhl Seminar 16482). In Dagstuhl Reports, Volume 6, Issue 11, pp. 168-184, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@Article{gaubert_et_al:DagRep.6.11.168,
  author =	{Gaubert, St\'{e}phane and Grigoriev, Dima and Joswig, Michael and Theobald, Thorsten},
  title =	{{Algorithms and Effectivity in Tropical Mathematics and Beyond (Dagstuhl Seminar 16482)}},
  pages =	{168--184},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2017},
  volume =	{6},
  number =	{11},
  editor =	{Gaubert, St\'{e}phane and Grigoriev, Dima and Joswig, Michael and Theobald, Thorsten},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.6.11.168},
  URN =		{urn:nbn:de:0030-drops-71073},
  doi =		{10.4230/DagRep.6.11.168},
  annote =	{Keywords: Algorithms in tropical mathematics, complexity, effective bounds, optimization, zero-sum games}
}
Document
DOI: 10.4230/LIPIcs.STACS.2015.379
Tropical Effective Primary and Dual Nullstellens"atze

Authors: Dima Grigoriev and Vladimir V. Podolskii

Published in: LIPIcs, Volume 30, 32nd International Symposium on Theoretical Aspects of Computer Science (STACS 2015)

Abstract
Tropical algebra is an emerging field with a number of applications in various areas of mathematics. In many of these applications appeal to tropical polynomials allows to study properties of mathematical objects such as algebraic varieties and algebraic curves from the computational point of view. This makes it important to study both mathematical and computational aspects of tropical polynomials. In this paper we prove tropical Nullstellensatz and moreover we show effective formulation of this theorem. Nullstellensatz is a next natural step in building algebraic theory of tropical polynomials and effective version is relevant for computational aspects of this field.
Cite as

Dima Grigoriev and Vladimir V. Podolskii. Tropical Effective Primary and Dual Nullstellens"atze. In 32nd International Symposium on Theoretical Aspects of Computer Science (STACS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 30, pp. 379-391, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{grigoriev_et_al:LIPIcs.STACS.2015.379,
  author =	{Grigoriev, Dima and Podolskii, Vladimir V.},
  title =	{{Tropical Effective Primary and Dual Nullstellens"atze}},
  booktitle =	{32nd International Symposium on Theoretical Aspects of Computer Science (STACS 2015)},
  pages =	{379--391},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-78-1},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{30},
  editor =	{Mayr, Ernst W. and Ollinger, Nicolas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2015.379},
  URN =		{urn:nbn:de:0030-drops-49286},
  doi =		{10.4230/LIPIcs.STACS.2015.379},
  annote =	{Keywords: tropical algebra, tropical geometry, Nullstellensatz}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact