---
_id: '13120'
abstract:
- lang: eng
  text: 'We formalized general (i.e., type-0) grammars using the Lean 3 proof assistant.
    We defined basic notions of rewrite rules and of words derived by a grammar, and
    used grammars to show closure of the class of type-0 languages under four operations:
    union, reversal, concatenation, and the Kleene star. The literature mostly focuses
    on Turing machine arguments, which are possibly more difficult to formalize. For
    the Kleene star, we could not follow the literature and came up with our own grammar-based
    construction.'
acknowledgement: "Jasmin Blanchette: This research has received funding from the Netherlands
  Organization\r\nfor Scientific Research (NWO) under the Vidi program (project No.
  016.Vidi.189.037, Lean Forward).\r\n__\r\nWe thank Vladimir Kolmogorov for making
  this collaboration possible. We\r\nthank Václav Končický for discussing ideas about
  the Kleene star construction. We thank Patrick Johnson, Floris van Doorn, and Damiano
  Testa for their small yet very valuable contributions to our code. We thank Eric
  Wieser for simplifying one of our proofs. We thank Mark Summerfield for suggesting
  textual improvements. We thank the anonymous reviewers for very helpful comments.
  Finally, we thank the Lean community for helping us with various technical issues
  and answering many questions. "
alternative_title:
- LIPIcs
article_number: '15'
article_processing_charge: No
arxiv: 1
author:
- first_name: Martin
  full_name: Dvorak, Martin
  id: 40ED02A8-C8B4-11E9-A9C0-453BE6697425
  last_name: Dvorak
  orcid: 0000-0001-5293-214X
- first_name: Jasmin
  full_name: Blanchette, Jasmin
  last_name: Blanchette
citation:
  ama: 'Dvorak M, Blanchette J. Closure properties of general grammars - formally
    verified. In: <i>14th International Conference on Interactive Theorem Proving</i>.
    Vol 268. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2023. doi:<a href="https://doi.org/10.4230/LIPIcs.ITP.2023.15">10.4230/LIPIcs.ITP.2023.15</a>'
  apa: 'Dvorak, M., &#38; Blanchette, J. (2023). Closure properties of general grammars
    - formally verified. In <i>14th International Conference on Interactive Theorem
    Proving</i> (Vol. 268). Bialystok, Poland: Schloss Dagstuhl - Leibniz-Zentrum
    für Informatik. <a href="https://doi.org/10.4230/LIPIcs.ITP.2023.15">https://doi.org/10.4230/LIPIcs.ITP.2023.15</a>'
  chicago: Dvorak, Martin, and Jasmin Blanchette. “Closure Properties of General Grammars
    - Formally Verified.” In <i>14th International Conference on Interactive Theorem
    Proving</i>, Vol. 268. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023.
    <a href="https://doi.org/10.4230/LIPIcs.ITP.2023.15">https://doi.org/10.4230/LIPIcs.ITP.2023.15</a>.
  ieee: M. Dvorak and J. Blanchette, “Closure properties of general grammars - formally
    verified,” in <i>14th International Conference on Interactive Theorem Proving</i>,
    Bialystok, Poland, 2023, vol. 268.
  ista: 'Dvorak M, Blanchette J. 2023. Closure properties of general grammars - formally
    verified. 14th International Conference on Interactive Theorem Proving. ITP: International
    Conference on Interactive Theorem Proving, LIPIcs, vol. 268, 15.'
  mla: Dvorak, Martin, and Jasmin Blanchette. “Closure Properties of General Grammars
    - Formally Verified.” <i>14th International Conference on Interactive Theorem
    Proving</i>, vol. 268, 15, Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
    2023, doi:<a href="https://doi.org/10.4230/LIPIcs.ITP.2023.15">10.4230/LIPIcs.ITP.2023.15</a>.
  short: M. Dvorak, J. Blanchette, in:, 14th International Conference on Interactive
    Theorem Proving, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023.
conference:
  end_date: 2023-08-04
  location: Bialystok, Poland
  name: 'ITP: International Conference on Interactive Theorem Proving'
  start_date: 2023-07-31
date_created: 2023-06-05T07:29:05Z
date_published: 2023-07-27T00:00:00Z
date_updated: 2023-09-25T11:04:29Z
day: '27'
ddc:
- '000'
department:
- _id: GradSch
- _id: VlKo
doi: 10.4230/LIPIcs.ITP.2023.15
external_id:
  arxiv:
  - '2302.06420'
file:
- access_level: open_access
  checksum: 773a0197f05b67feaa6cb1e17ec3642d
  content_type: application/pdf
  creator: dernst
  date_created: 2023-08-07T11:55:43Z
  date_updated: 2023-08-07T11:55:43Z
  file_id: '13982'
  file_name: 2023_LIPIcS_Dvorak.pdf
  file_size: 715976
  relation: main_file
  success: 1
file_date_updated: 2023-08-07T11:55:43Z
has_accepted_license: '1'
intvolume: '       268'
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
publication: 14th International Conference on Interactive Theorem Proving
publication_identifier:
  eissn:
  - 1868-8969
  isbn:
  - '9783959772846'
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
quality_controlled: '1'
related_material:
  link:
  - relation: software
    url: https://github.com/madvorak/grammars/tree/publish
scopus_import: '1'
status: public
title: Closure properties of general grammars - formally verified
tmp:
  image: /images/cc_by.png
  legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
  name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
  short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 268
year: '2023'
...
---
_id: '9592'
abstract:
- lang: eng
  text: The convex grabbing game is a game where two players, Alice and Bob, alternate
    taking extremal points from the convex hull of a point set on the plane. Rational
    weights are given to the points. The goal of each player is to maximize the total
    weight over all points that they obtain. We restrict the setting to the case of
    binary weights. We show a construction of an arbitrarily large odd-sized point
    set that allows Bob to obtain almost 3/4 of the total weight. This construction
    answers a question asked by Matsumoto, Nakamigawa, and Sakuma in [Graphs and Combinatorics,
    36/1 (2020)]. We also present an arbitrarily large even-sized point set where
    Bob can obtain the entirety of the total weight. Finally, we discuss conjectures
    about optimum moves in the convex grabbing game for both players in general.
article_processing_charge: No
arxiv: 1
author:
- first_name: Martin
  full_name: Dvorak, Martin
  id: 40ED02A8-C8B4-11E9-A9C0-453BE6697425
  last_name: Dvorak
  orcid: 0000-0001-5293-214X
- first_name: Sara
  full_name: Nicholson, Sara
  last_name: Nicholson
citation:
  ama: 'Dvorak M, Nicholson S. Massively winning configurations in the convex grabbing
    game on the plane. In: <i>Proceedings of the 33rd Canadian Conference on Computational
    Geometry</i>.'
  apa: Dvorak, M., &#38; Nicholson, S. (n.d.). Massively winning configurations in
    the convex grabbing game on the plane. In <i>Proceedings of the 33rd Canadian
    Conference on Computational Geometry</i>. Halifax, NS, Canada.
  chicago: Dvorak, Martin, and Sara Nicholson. “Massively Winning Configurations in
    the Convex Grabbing Game on the Plane.” In <i>Proceedings of the 33rd Canadian
    Conference on Computational Geometry</i>, n.d.
  ieee: M. Dvorak and S. Nicholson, “Massively winning configurations in the convex
    grabbing game on the plane,” in <i>Proceedings of the 33rd Canadian Conference
    on Computational Geometry</i>, Halifax, NS, Canada.
  ista: 'Dvorak M, Nicholson S. Massively winning configurations in the convex grabbing
    game on the plane. Proceedings of the 33rd Canadian Conference on Computational
    Geometry. CCCG: Canadian Conference on Computational Geometry.'
  mla: Dvorak, Martin, and Sara Nicholson. “Massively Winning Configurations in the
    Convex Grabbing Game on the Plane.” <i>Proceedings of the 33rd Canadian Conference
    on Computational Geometry</i>.
  short: M. Dvorak, S. Nicholson, in:, Proceedings of the 33rd Canadian Conference
    on Computational Geometry, n.d.
conference:
  end_date: 2021-08-12
  location: Halifax, NS, Canada
  name: 'CCCG: Canadian Conference on Computational Geometry'
  start_date: 2021-08-10
date_created: 2021-06-22T15:57:11Z
date_published: 2021-06-29T00:00:00Z
date_updated: 2021-08-12T10:57:39Z
day: '29'
ddc:
- '516'
department:
- _id: GradSch
- _id: VlKo
external_id:
  arxiv:
  - '2106.11247'
file:
- access_level: open_access
  checksum: 45accb1de9b7e0e4bb2fbfe5fd3e6239
  content_type: application/pdf
  creator: mdvorak
  date_created: 2021-06-28T20:23:13Z
  date_updated: 2021-06-28T20:23:13Z
  file_id: '9616'
  file_name: Convex-Grabbing-Game_CCCG_proc_version.pdf
  file_size: 381306
  relation: main_file
  success: 1
- access_level: open_access
  checksum: 9199cf18c65658553487458cc24d0ab2
  content_type: application/pdf
  creator: kschuh
  date_created: 2021-08-12T10:57:21Z
  date_updated: 2021-08-12T10:57:21Z
  file_id: '9902'
  file_name: Convex-Grabbing-Game_FULL-VERSION.pdf
  file_size: 403645
  relation: main_file
  success: 1
file_date_updated: 2021-08-12T10:57:21Z
has_accepted_license: '1'
keyword:
- convex grabbing game
- graph grabbing game
- combinatorial game
- convex geometry
language:
- iso: eng
month: '06'
oa: 1
oa_version: Submitted Version
publication: Proceedings of the 33rd Canadian Conference on Computational Geometry
publication_status: accepted
quality_controlled: '1'
status: public
title: Massively winning configurations in the convex grabbing game on the plane
tmp:
  image: /image/cc_by_nd.png
  legal_code_url: https://creativecommons.org/licenses/by-nd/4.0/legalcode
  name: Creative Commons Attribution-NoDerivatives 4.0 International (CC BY-ND 4.0)
  short: CC BY-ND (4.0)
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
year: '2021'
...
---
_id: '10045'
abstract:
- lang: eng
  text: "Given a fixed finite metric space (V,μ), the {\\em minimum 0-extension problem},
    denoted as 0-Ext[μ], is equivalent to the following optimization problem: minimize
    function of the form minx∈Vn∑ifi(xi)+∑ijcijμ(xi,xj) where cij,cvi are given nonnegative
    costs and fi:V→R are functions given by fi(xi)=∑v∈Vcviμ(xi,v). The computational
    complexity of 0-Ext[μ] has been recently established by Karzanov and by Hirai:
    if metric μ is {\\em orientable modular} then 0-Ext[μ] can be solved in polynomial
    time, otherwise 0-Ext[μ] is NP-hard. To prove the tractability part, Hirai developed
    a theory of discrete convex functions on orientable modular graphs generalizing
    several known classes of functions in discrete convex analysis, such as L♮-convex
    functions. We consider a more general version of the problem in which unary functions
    fi(xi) can additionally have terms of the form cuv;iμ(xi,{u,v}) for {u,v}∈F, where
    set F⊆(V2) is fixed. We extend the complexity classification above by providing
    an explicit condition on (μ,F) for the problem to be tractable. In order to prove
    the tractability part, we generalize Hirai's theory and define a larger class
    of discrete convex functions. It covers, in particular, another well-known class
    of functions, namely submodular functions on an integer lattice. Finally, we improve
    the complexity of Hirai's algorithm for solving 0-Ext on orientable modular graphs.\r\n"
article_number: '2109.10203'
article_processing_charge: No
arxiv: 1
author:
- first_name: Martin
  full_name: Dvorak, Martin
  id: 40ED02A8-C8B4-11E9-A9C0-453BE6697425
  last_name: Dvorak
  orcid: 0000-0001-5293-214X
- first_name: Vladimir
  full_name: Kolmogorov, Vladimir
  id: 3D50B0BA-F248-11E8-B48F-1D18A9856A87
  last_name: Kolmogorov
citation:
  ama: Dvorak M, Kolmogorov V. Generalized minimum 0-extension problem and discrete
    convexity. <i>arXiv</i>. doi:<a href="https://doi.org/10.48550/arXiv.2109.10203">10.48550/arXiv.2109.10203</a>
  apa: Dvorak, M., &#38; Kolmogorov, V. (n.d.). Generalized minimum 0-extension problem
    and discrete convexity. <i>arXiv</i>. <a href="https://doi.org/10.48550/arXiv.2109.10203">https://doi.org/10.48550/arXiv.2109.10203</a>
  chicago: Dvorak, Martin, and Vladimir Kolmogorov. “Generalized Minimum 0-Extension
    Problem and Discrete Convexity.” <i>ArXiv</i>, n.d. <a href="https://doi.org/10.48550/arXiv.2109.10203">https://doi.org/10.48550/arXiv.2109.10203</a>.
  ieee: M. Dvorak and V. Kolmogorov, “Generalized minimum 0-extension problem and
    discrete convexity,” <i>arXiv</i>. .
  ista: Dvorak M, Kolmogorov V. Generalized minimum 0-extension problem and discrete
    convexity. arXiv, 2109.10203.
  mla: Dvorak, Martin, and Vladimir Kolmogorov. “Generalized Minimum 0-Extension Problem
    and Discrete Convexity.” <i>ArXiv</i>, 2109.10203, doi:<a href="https://doi.org/10.48550/arXiv.2109.10203">10.48550/arXiv.2109.10203</a>.
  short: M. Dvorak, V. Kolmogorov, ArXiv (n.d.).
date_created: 2021-09-27T10:48:23Z
date_published: 2021-09-21T00:00:00Z
date_updated: 2023-05-03T10:40:16Z
day: '21'
ddc:
- '004'
department:
- _id: GradSch
- _id: VlKo
doi: 10.48550/arXiv.2109.10203
external_id:
  arxiv:
  - '2109.10203'
file:
- access_level: open_access
  checksum: e7e83065f7bc18b9c188bf93b5ca5db6
  content_type: application/pdf
  creator: mdvorak
  date_created: 2021-09-27T10:54:51Z
  date_updated: 2021-09-27T10:54:51Z
  file_id: '10046'
  file_name: Generalized-0-Ext.pdf
  file_size: 603672
  relation: main_file
  success: 1
file_date_updated: 2021-09-27T10:54:51Z
has_accepted_license: '1'
keyword:
- minimum 0-extension problem
- metric labeling problem
- discrete metric spaces
- metric extensions
- computational complexity
- valued constraint satisfaction problems
- discrete convex analysis
- L-convex functions
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: ' https://doi.org/10.48550/arXiv.2109.10203'
month: '09'
oa: 1
oa_version: Preprint
publication: arXiv
publication_status: submitted
status: public
title: Generalized minimum 0-extension problem and discrete convexity
type: preprint
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2021'
...