6 Search Results for "Kovács, Benjamin"

Document
Short Paper
DOI: 10.4230/LIPIcs.COSIT.2024.17
A Logic of East and West for Intervals (Short Paper)

Authors: Zekai Li, Amin Farjudian, and Heshan Du

Published in: LIPIcs, Volume 315, 16th International Conference on Spatial Information Theory (COSIT 2024)

Abstract
This paper proposes a logic of east and west for intervals (LEWI), which extends the logic of east and west for points. For intervals in 1D Euclidean space, the logic LEWI formalises the qualitative direction relations "east", "west", "definitely east", "definitely west", "partially east", "partially west", etc. To cope with imprecision in geometry representations, the logic LEWI is parameterized by a margin of error σ ∈ ℝ_{> 0} and a level of indeterminacy in directions τ ∈ ℕ_{> 1}. For every τ, we provide an axiomatisation of the logic LEWI, and prove that it is sound and complete with respect to 1D Euclidean space.
Cite as

Zekai Li, Amin Farjudian, and Heshan Du. A Logic of East and West for Intervals (Short Paper). In 16th International Conference on Spatial Information Theory (COSIT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 315, pp. 17:1-17:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{li_et_al:LIPIcs.COSIT.2024.17,
  author =	{Li, Zekai and Farjudian, Amin and Du, Heshan},
  title =	{{A Logic of East and West for Intervals}},
  booktitle =	{16th International Conference on Spatial Information Theory (COSIT 2024)},
  pages =	{17:1--17:8},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-330-0},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{315},
  editor =	{Adams, Benjamin and Griffin, Amy L. and Scheider, Simon and McKenzie, Grant},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.COSIT.2024.17},
  URN =		{urn:nbn:de:0030-drops-208320},
  doi =		{10.4230/LIPIcs.COSIT.2024.17},
  annote =	{Keywords: Qualitative Spatial Logic, Soundness, Completeness}
}
Document
DOI: 10.4230/LIPIcs.ITP.2024.10
Duper: A Proof-Producing Superposition Theorem Prover for Dependent Type Theory

Authors: Joshua Clune, Yicheng Qian, Alexander Bentkamp, and Jeremy Avigad

Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)

Abstract
We present Duper, a proof-producing theorem prover for Lean based on the superposition calculus. Duper can be called directly as a terminal tactic in interactive Lean proofs, but is also designed with proof reconstruction for a future Lean hammer in mind. In this paper, we describe Duper’s underlying approach to proof search and proof reconstruction with a particular emphasis on the challenges of working in a dependent type theory. We also compare Duper’s performance to Metis' on pre-existing benchmarks to give evidence that Duper is performant enough to be useful for proof reconstruction in a hammer.
Cite as

Joshua Clune, Yicheng Qian, Alexander Bentkamp, and Jeremy Avigad. Duper: A Proof-Producing Superposition Theorem Prover for Dependent Type Theory. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 10:1-10:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{clune_et_al:LIPIcs.ITP.2024.10,
  author =	{Clune, Joshua and Qian, Yicheng and Bentkamp, Alexander and Avigad, Jeremy},
  title =	{{Duper: A Proof-Producing Superposition Theorem Prover for Dependent Type Theory}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{10:1--10:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-337-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{309},
  editor =	{Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.10},
  URN =		{urn:nbn:de:0030-drops-207381},
  doi =		{10.4230/LIPIcs.ITP.2024.10},
  annote =	{Keywords: proof search, automatic theorem proving, interactive theorem proving, Lean, dependent type theory}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2024.13
The Power of Counting Steps in Quantitative Games

Authors: Sougata Bose, Rasmus Ibsen-Jensen, David Purser, Patrick Totzke, and Pierre Vandenhove

Published in: LIPIcs, Volume 311, 35th International Conference on Concurrency Theory (CONCUR 2024)

Abstract
We study deterministic games of infinite duration played on graphs and focus on the strategy complexity of quantitative objectives. Such games are known to admit optimal memoryless strategies over finite graphs, but require infinite-memory strategies in general over infinite graphs. We provide new lower and upper bounds for the strategy complexity of mean-payoff and total-payoff objectives over infinite graphs, focusing on whether step-counter strategies (sometimes called Markov strategies) suffice to implement winning strategies. In particular, we show that over finitely branching arenas, three variants of limsup mean-payoff and total-payoff objectives admit winning strategies that are based either on a step counter or on a step counter and an additional bit of memory. Conversely, we show that for certain liminf total-payoff objectives, strategies resorting to a step counter and finite memory are not sufficient. For step-counter strategies, this settles the case of all classical quantitative objectives up to the second level of the Borel hierarchy.
Cite as

Sougata Bose, Rasmus Ibsen-Jensen, David Purser, Patrick Totzke, and Pierre Vandenhove. The Power of Counting Steps in Quantitative Games. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 13:1-13:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{bose_et_al:LIPIcs.CONCUR.2024.13,
  author =	{Bose, Sougata and Ibsen-Jensen, Rasmus and Purser, David and Totzke, Patrick and Vandenhove, Pierre},
  title =	{{The Power of Counting Steps in Quantitative Games}},
  booktitle =	{35th International Conference on Concurrency Theory (CONCUR 2024)},
  pages =	{13:1--13:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-339-3},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{311},
  editor =	{Majumdar, Rupak and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.13},
  URN =		{urn:nbn:de:0030-drops-207852},
  doi =		{10.4230/LIPIcs.CONCUR.2024.13},
  annote =	{Keywords: Games on graphs, Markov strategies, quantitative objectives, infinite-state systems}
}
Document
DOI: 10.4230/LIPIcs.SAT.2024.28
Strategy Extraction by Interpolation

Authors: Friedrich Slivovsky

Published in: LIPIcs, Volume 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)

Abstract
In applications, QBF solvers are often required to generate strategies. This typically involves a process known as strategy extraction, where a Boolean circuit encoding a strategy is computed from a proof. It has previously been observed that Craig interpolation in propositional logic can be seen as a special case of QBF strategy extraction. In this paper we explore this connection further and show that, conversely, any strategy for a false QBF corresponds to a sequence of interpolants in its complete (Herbrand) expansion. Inspired by this correspondence, we present a new strategy extraction algorithm for the expansion-based proof system Exp+Res. Its asymptotic running time matches the best known bound of O(mn) for a proof with m lines and n universally quantified variables. We report on experiments comparing this algorithm with a strategy extraction algorithm based on combining partial strategies, as well as with round-based strategy extraction.
Cite as

Friedrich Slivovsky. Strategy Extraction by Interpolation. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 28:1-28:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{slivovsky:LIPIcs.SAT.2024.28,
  author =	{Slivovsky, Friedrich},
  title =	{{Strategy Extraction by Interpolation}},
  booktitle =	{27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)},
  pages =	{28:1--28:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-334-8},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{305},
  editor =	{Chakraborty, Supratik and Jiang, Jie-Hong Roland},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.28},
  URN =		{urn:nbn:de:0030-drops-205509},
  doi =		{10.4230/LIPIcs.SAT.2024.28},
  annote =	{Keywords: QBF, Expansion, Strategy Extraction, Interpolation}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2024.10
Second-Order Generalised Algebraic Theories: Signatures and First-Order Semantics

Authors: Ambrus Kaposi and Szumi Xie

Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)

Abstract
Programming languages can be defined from the concrete to the abstract by abstract syntax trees, well-scoped syntax, well-typed (intrinsic) syntax, algebraic syntax (well-typed syntax quotiented by conversion). Another aspect is the representation of binding structure for which nominal approaches, De Bruijn indices/levels and higher order abstract syntax (HOAS) are available. In HOAS, binders are given by the function space of an internal language of presheaves. In this paper, we show how to combine the algebraic approach with the HOAS approach: following Uemura, we define languages as second-order generalised algebraic theories (SOGATs). Through a series of examples we show that non-substructural languages can be naturally defined as SOGATs. We give a formal definition of SOGAT signatures (using the syntax of a particular SOGAT) and define two translations from SOGAT signatures to GAT signatures (signatures for quotient inductive-inductive types), based on parallel and single substitutions, respectively.
Cite as

Ambrus Kaposi and Szumi Xie. Second-Order Generalised Algebraic Theories: Signatures and First-Order Semantics. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 10:1-10:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{kaposi_et_al:LIPIcs.FSCD.2024.10,
  author =	{Kaposi, Ambrus and Xie, Szumi},
  title =	{{Second-Order Generalised Algebraic Theories: Signatures and First-Order Semantics}},
  booktitle =	{9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
  pages =	{10:1--10:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-323-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{299},
  editor =	{Rehof, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.10},
  URN =		{urn:nbn:de:0030-drops-203396},
  doi =		{10.4230/LIPIcs.FSCD.2024.10},
  annote =	{Keywords: Type theory, universal algebra, inductive types, quotient inductive types, higher-order abstract syntax, logical framework}
}
Document
DOI: 10.4230/LIPIcs.CP.2021.36
Utilizing Constraint Optimization for Industrial Machine Workload Balancing

Authors: Benjamin Kovács, Pierre Tassel, Wolfgang Kohlenbrein, Philipp Schrott-Kostwein, and Martin Gebser

Published in: LIPIcs, Volume 210, 27th International Conference on Principles and Practice of Constraint Programming (CP 2021)

Abstract
Efficient production scheduling is an important application area of constraint-based optimization techniques. Problem domains like flow- and job-shop scheduling have been extensive study targets, and solving approaches range from complete and local search to machine learning methods. In this paper, we devise and compare constraint-based optimization techniques for scheduling specialized manufacturing processes in the build-to-print business. The goal is to allocate production equipment such that customer orders are completed in time as good as possible, while respecting machine capacities and minimizing extra shifts required to resolve bottlenecks. To this end, we furnish several approaches for scheduling pending production tasks to one or more workdays for performing them. First, we propose a greedy custom algorithm that allows for quickly screening the effects of altering resource demands and availabilities. Moreover, we take advantage of such greedy solutions to parameterize and warm-start the optimization performed by integer linear programming (ILP) and constraint programming (CP) solvers on corresponding problem formulations. Our empirical evaluation is based on production data by Kostwein Holding GmbH, a worldwide supplier in the build-to-print business, and thus demonstrates the industrial applicability of our scheduling methods. We also present a user-friendly web interface for feeding the underlying solvers with customer order and equipment data, graphically displaying computed schedules, and facilitating the investigation of changed resource demands and availabilities, e.g., due to updating orders or including extra shifts.
Cite as

Benjamin Kovács, Pierre Tassel, Wolfgang Kohlenbrein, Philipp Schrott-Kostwein, and Martin Gebser. Utilizing Constraint Optimization for Industrial Machine Workload Balancing. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 36:1-36:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{kovacs_et_al:LIPIcs.CP.2021.36,
  author =	{Kov\'{a}cs, Benjamin and Tassel, Pierre and Kohlenbrein, Wolfgang and Schrott-Kostwein, Philipp and Gebser, Martin},
  title =	{{Utilizing Constraint Optimization for Industrial Machine Workload Balancing}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{36:1--36:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.36},
  URN =		{urn:nbn:de:0030-drops-153276},
  doi =		{10.4230/LIPIcs.CP.2021.36},
  annote =	{Keywords: application, production planning, production scheduling, linear programming, constraint programming, greedy algorithm, benchmarking}
}
  • Refine by Author
  • 1 Avigad, Jeremy
  • 1 Bentkamp, Alexander
  • 1 Bose, Sougata
  • 1 Clune, Joshua
  • 1 Du, Heshan
  • Show More...

  • Refine by Classification
  • 3 Theory of computation → Automated reasoning
  • 2 Theory of computation → Type theory
  • 1 Applied computing → Command and control
  • 1 Theory of computation → Automata over infinite objects
  • 1 Theory of computation → Higher order logic
  • Show More...

  • Refine by Keyword
  • 1 Completeness
  • 1 Expansion
  • 1 Games on graphs
  • 1 Interpolation
  • 1 Lean
  • Show More...

  • Refine by Type
  • 6 document

  • Refine by Publication Year
  • 5 2024
  • 1 2021

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 Imprint Privacy Contact