15 Search Results for "Baumgartner, Peter"

Document
DOI: 10.4230/LIPIcs.SEA.2026.5
BuffCut: Prioritized Buffered Streaming Graph Partitioning

Authors: Linus Baumgärtner, Adil Chhabra, Marcelo Fonseca Faraj, and Christian Schulz

Published in: LIPIcs, Volume 371, 24th International Symposium on Experimental Algorithms (SEA 2026)

Abstract
Streaming graph partitioners enable resource-efficient and massively scalable partitioning, but one-pass assignment heuristics are highly sensitive to stream order and often yield substantially higher edge cuts than in-memory methods. We present BuffCut, a buffered streaming partitioner that narrows this quality gap, particularly when stream ordering is adversarial, by combining prioritized buffering with batch-wise multilevel assignment. BuffCut maintains a bounded priority buffer to delay poorly informed decisions and regulate the order in which nodes are considered for assignment. It incrementally constructs high-locality batches of configurable size by iteratively inserting the highest-priority nodes from the buffer into the batch, effectively recovering locality structure from the stream. Each batch is then assigned via a multilevel partitioning algorithm. Experiments on diverse real-world and synthetic graphs show that BuffCut consistently outperforms state-of-the-art buffered streaming methods. Compared to the strongest prioritized buffering baseline, BuffCut achieves 20.8% fewer edge cuts while running 2.9× faster and using 11.3× less memory. Against the next-best batched method, it reduces edge cut by 15.8% with only modest overheads of 1.8× runtime and 1.09× memory.
Cite as

Linus Baumgärtner, Adil Chhabra, Marcelo Fonseca Faraj, and Christian Schulz. BuffCut: Prioritized Buffered Streaming Graph Partitioning. In 24th International Symposium on Experimental Algorithms (SEA 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 371, pp. 5:1-5:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{baumgartner_et_al:LIPIcs.SEA.2026.5,
  author =	{Baumg\"{a}rtner, Linus and Chhabra, Adil and Faraj, Marcelo Fonseca and Schulz, Christian},
  title =	{{BuffCut: Prioritized Buffered Streaming Graph Partitioning}},
  booktitle =	{24th International Symposium on Experimental Algorithms (SEA 2026)},
  pages =	{5:1--5:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-422-2},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{371},
  editor =	{Aum\"{u}ller, Martin and Finocchi, Irene},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SEA.2026.5},
  URN =		{urn:nbn:de:0030-drops-260097},
  doi =		{10.4230/LIPIcs.SEA.2026.5},
  annote =	{Keywords: graph partitioning, streaming, online, buffered, prioritized partitioning}
}
Document
DOI: 10.4230/LIPIcs.SoCG.2026.45
Line Segment Visibility in Simple Polygons: Exact, Robust, Scalable Computation and Applications

Authors: Sándor P. Fekete, Prahlad Narasimhan Kasthurirangan, Phillip Keldenich, Fabian Kollhoff, Chek-Manh Loi, and Michael Perk

Published in: LIPIcs, Volume 367, 42nd International Symposium on Computational Geometry (SoCG 2026)

Abstract
The weak visibility polygon of a line segment s inside a simple polygon P, denoted by V_P(s), is the region of the polygon that is visible from at least one point on s. Given its fundamental nature in computational geometry, several algorithms have been proposed to compute weak visibility polygons efficiently, each with different trade-offs in terms of preprocessing time, query time, and space complexity. Although there are many applications that require computing these polygons such as computer graphics, robot motion planning, and network communication systems, there is a lack of any implementations of these algorithms in the literature - not to mention one that is exact, robust, and scalable. Furthermore, weak segment visibility polygons are used as basic building blocks in several other algorithms, such as in minimum-link path computation. In this work, we present an implementation of an optimal linear-time algorithm for computing the weak visibility polygon of a segment inside a triangulated simple polygon. Our implementation provides exact, robust geometric primitives and optimizations to handle large inputs with more than 18,000,000 vertices. We demonstrate two concrete applications: (1) construction of window partitions, a standard data structure in visibility algorithms, and (2) support for optimal minimum-link path queries between two points in a simple polygon, the latter serving as a direct use case of the former. Experimental results on a variety of polygon families confirm that the end-to-end running time scales linearly with the size of the polygon and is dominated by the cost of computing the triangulation, validating the practicality and scalability of the approach. The implementation is released as open source in the format of a CGAL package to support reproducibility and further research.
Cite as

Sándor P. Fekete, Prahlad Narasimhan Kasthurirangan, Phillip Keldenich, Fabian Kollhoff, Chek-Manh Loi, and Michael Perk. Line Segment Visibility in Simple Polygons: Exact, Robust, Scalable Computation and Applications. In 42nd International Symposium on Computational Geometry (SoCG 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 367, pp. 45:1-45:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{fekete_et_al:LIPIcs.SoCG.2026.45,
  author =	{Fekete, S\'{a}ndor P. and Kasthurirangan, Prahlad Narasimhan and Keldenich, Phillip and Kollhoff, Fabian and Loi, Chek-Manh and Perk, Michael},
  title =	{{Line Segment Visibility in Simple Polygons: Exact, Robust, Scalable Computation and Applications}},
  booktitle =	{42nd International Symposium on Computational Geometry (SoCG 2026)},
  pages =	{45:1--45:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-418-5},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{367},
  editor =	{Ahn, Hee-Kap and Hoffmann, Michael and Nayyeri, Amir},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SoCG.2026.45},
  URN =		{urn:nbn:de:0030-drops-258516},
  doi =		{10.4230/LIPIcs.SoCG.2026.45},
  annote =	{Keywords: Visibility, line segments, link distance, window partition, computation, implementation, robustness, scalability, exactness, CGAL}
}
Document
DOI: 10.4230/LIPIcs.ESA.2025.106
On Estimating the Quantum 𝓁_α Distance

Authors: Yupan Liu and Qisheng Wang

Published in: LIPIcs, Volume 351, 33rd Annual European Symposium on Algorithms (ESA 2025)

Abstract
We study the computational complexity of estimating the quantum 𝓁_α distance T_α(ρ₀,ρ₁), defined via the Schatten α-norm ‖A‖_α := tr(|A|^α)^{1/α}, given poly(n)-size state-preparation circuits of n-qubit quantum states ρ₀ and ρ₁. This quantity serves as a lower bound on the trace distance for α > 1. For any constant α > 1, we develop an efficient rank-independent quantum estimator for T_α(ρ₀,ρ₁) with time complexity poly(n), achieving an exponential speedup over the prior best results of exp(n) due to Wang, Guan, Liu, Zhang, and Ying (IEEE Trans. Inf. Theory 2024). Our improvement leverages efficiently computable uniform polynomial approximations of signed positive power functions within quantum singular value transformation, thereby eliminating the dependence on the rank of the states. Our quantum algorithm reveals a dichotomy in the computational complexity of the Quantum State Distinguishability Problem with Schatten α-norm (QSD_α), which involves deciding whether T_α(ρ₀,ρ₁) is at least 2/5 or at most 1/5. This dichotomy arises between the cases of constant α > 1 and α = 1: - For any 1+Ω(1) ≤ α ≤ O(1), QSD_α is BQP-complete. - For any 1 ≤ α ≤ 1+1/n, QSD_α is QSZK-complete, implying that no efficient quantum estimator for T_α(ρ₀,ρ₁) exists unless BQP = QSZK. The hardness results follow from reductions based on new rank-dependent inequalities for the quantum 𝓁_α distance with 1 ≤ α ≤ ∞, which are of independent interest.
Cite as

Yupan Liu and Qisheng Wang. On Estimating the Quantum 𝓁_α Distance. In 33rd Annual European Symposium on Algorithms (ESA 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 351, pp. 106:1-106:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{liu_et_al:LIPIcs.ESA.2025.106,
  author =	{Liu, Yupan and Wang, Qisheng},
  title =	{{On Estimating the Quantum 𝓁\underline\alpha Distance}},
  booktitle =	{33rd Annual European Symposium on Algorithms (ESA 2025)},
  pages =	{106:1--106:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-395-9},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{351},
  editor =	{Benoit, Anne and Kaplan, Haim and Wild, Sebastian and Herman, Grzegorz},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ESA.2025.106},
  URN =		{urn:nbn:de:0030-drops-245758},
  doi =		{10.4230/LIPIcs.ESA.2025.106},
  annote =	{Keywords: quantum algorithms, quantum state testing, trace distance, Schatten norm}
}
Document
DOI: 10.4230/LIPIcs.ITP.2025.13
Barendregt’s Theory of the λ-Calculus, Refreshed and Formalized

Authors: Adrienne Lancelot, Beniamino Accattoli, and Maxime Vemclefs

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
Barendregt’s book on the untyped λ-calculus refines the inconsistent view of β-divergence as representation of the undefined via the key concept of head reduction. In this paper, we put together recent revisitations of some key theorems laid out in Barendregt’s book, and we formalize them in the Abella proof assistant. Our work provides a compact and refreshed presentation of the core of the book. The formalization faithfully mimics pen-and-paper proofs. Two interesting aspects are the manipulation of contexts for the study of contextual equivalence and a formal alternative to the informal trick at work in Takahashi’s proof of the genericity lemma. As a by-product, we obtain an alternative definition of contextual equivalence that does not mention contexts.
Cite as

Adrienne Lancelot, Beniamino Accattoli, and Maxime Vemclefs. Barendregt’s Theory of the λ-Calculus, Refreshed and Formalized. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 13:1-13:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{lancelot_et_al:LIPIcs.ITP.2025.13,
  author =	{Lancelot, Adrienne and Accattoli, Beniamino and Vemclefs, Maxime},
  title =	{{Barendregt’s Theory of the \lambda-Calculus, Refreshed and Formalized}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{13:1--13:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.13},
  URN =		{urn:nbn:de:0030-drops-246114},
  doi =		{10.4230/LIPIcs.ITP.2025.13},
  annote =	{Keywords: lambda-calculus, head reduction, equational theory}
}
Document
DOI: 10.4230/LIPIcs.ICDT.2025.4
Learning Aggregate Queries Defined by First-Order Logic with Counting

Authors: Steffen van Bergerem and Nicole Schweikardt

Published in: LIPIcs, Volume 328, 28th International Conference on Database Theory (ICDT 2025)

Abstract
In the logical framework introduced by Grohe and Turán (TOCS 2004) for Boolean classification problems, the instances to classify are tuples from a logical structure, and Boolean classifiers are described by parametric models based on logical formulas. This is a specific scenario for supervised passive learning, where classifiers should be learned based on labelled examples. Existing results in this scenario focus on Boolean classification. This paper presents learnability results beyond Boolean classification. We focus on multiclass classification problems where the task is to assign input tuples to arbitrary integers. To represent such integer-valued classifiers, we use aggregate queries specified by an extension of first-order logic with counting terms called FOC₁. Our main result shows the following: given a database of polylogarithmic degree, within quasi-linear time, we can build an index structure that makes it possible to learn FOC₁-definable integer-valued classifiers in time polylogarithmic in the size of the database and polynomial in the number of training examples.
Cite as

Steffen van Bergerem and Nicole Schweikardt. Learning Aggregate Queries Defined by First-Order Logic with Counting. In 28th International Conference on Database Theory (ICDT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 328, pp. 4:1-4:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{vanbergerem_et_al:LIPIcs.ICDT.2025.4,
  author =	{van Bergerem, Steffen and Schweikardt, Nicole},
  title =	{{Learning Aggregate Queries Defined by First-Order Logic with Counting}},
  booktitle =	{28th International Conference on Database Theory (ICDT 2025)},
  pages =	{4:1--4:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-364-5},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{328},
  editor =	{Roy, Sudeepa and Kara, Ahmet},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2025.4},
  URN =		{urn:nbn:de:0030-drops-229457},
  doi =		{10.4230/LIPIcs.ICDT.2025.4},
  annote =	{Keywords: Supervised learning, multiclass classification problems, counting logic}
}
Document
Survey
DOI: 10.4230/TGDK.1.1.4
Knowledge Graph Embeddings: Open Challenges and Opportunities

Authors: Russa Biswas, Lucie-Aimée Kaffee, Michael Cochez, Stefania Dumbrava, Theis E. Jendal, Matteo Lissandrini, Vanessa Lopez, Eneldo Loza Mencía, Heiko Paulheim, Harald Sack, Edlira Kalemi Vakaj, and Gerard de Melo

Published in: TGDK, Volume 1, Issue 1 (2023): Special Issue on Trends in Graph Data and Knowledge. Transactions on Graph Data and Knowledge, Volume 1, Issue 1

Abstract
While Knowledge Graphs (KGs) have long been used as valuable sources of structured knowledge, in recent years, KG embeddings have become a popular way of deriving numeric vector representations from them, for instance, to support knowledge graph completion and similarity search. This study surveys advances as well as open challenges and opportunities in this area. For instance, the most prominent embedding models focus primarily on structural information. However, there has been notable progress in incorporating further aspects, such as semantics, multi-modal, temporal, and multilingual features. Most embedding techniques are assessed using human-curated benchmark datasets for the task of link prediction, neglecting other important real-world KG applications. Many approaches assume a static knowledge graph and are unable to account for dynamic changes. Additionally, KG embeddings may encode data biases and lack interpretability. Overall, this study provides an overview of promising research avenues to learn improved KG embeddings that can address a more diverse range of use cases.
Cite as

Russa Biswas, Lucie-Aimée Kaffee, Michael Cochez, Stefania Dumbrava, Theis E. Jendal, Matteo Lissandrini, Vanessa Lopez, Eneldo Loza Mencía, Heiko Paulheim, Harald Sack, Edlira Kalemi Vakaj, and Gerard de Melo. Knowledge Graph Embeddings: Open Challenges and Opportunities. In Special Issue on Trends in Graph Data and Knowledge. Transactions on Graph Data and Knowledge (TGDK), Volume 1, Issue 1, pp. 4:1-4:32, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@Article{biswas_et_al:TGDK.1.1.4,
  author =	{Biswas, Russa and Kaffee, Lucie-Aim\'{e}e and Cochez, Michael and Dumbrava, Stefania and Jendal, Theis E. and Lissandrini, Matteo and Lopez, Vanessa and Menc{\'\i}a, Eneldo Loza and Paulheim, Heiko and Sack, Harald and Vakaj, Edlira Kalemi and de Melo, Gerard},
  title =	{{Knowledge Graph Embeddings: Open Challenges and Opportunities}},
  journal =	{Transactions on Graph Data and Knowledge},
  pages =	{4:1--4:32},
  year =	{2023},
  volume =	{1},
  number =	{1},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/TGDK.1.1.4},
  URN =		{urn:nbn:de:0030-drops-194783},
  doi =		{10.4230/TGDK.1.1.4},
  annote =	{Keywords: Knowledge Graphs, KG embeddings, Link prediction, KG applications}
}
Document
Position
DOI: 10.4230/TGDK.1.1.5
Knowledge Graphs for the Life Sciences: Recent Developments, Challenges and Opportunities

Authors: Jiaoyan Chen, Hang Dong, Janna Hastings, Ernesto Jiménez-Ruiz, Vanessa López, Pierre Monnin, Catia Pesquita, Petr Škoda, and Valentina Tamma

Published in: TGDK, Volume 1, Issue 1 (2023): Special Issue on Trends in Graph Data and Knowledge. Transactions on Graph Data and Knowledge, Volume 1, Issue 1

Abstract
The term life sciences refers to the disciplines that study living organisms and life processes, and include chemistry, biology, medicine, and a range of other related disciplines. Research efforts in life sciences are heavily data-driven, as they produce and consume vast amounts of scientific data, much of which is intrinsically relational and graph-structured. The volume of data and the complexity of scientific concepts and relations referred to therein promote the application of advanced knowledge-driven technologies for managing and interpreting data, with the ultimate aim to advance scientific discovery. In this survey and position paper, we discuss recent developments and advances in the use of graph-based technologies in life sciences and set out a vision for how these technologies will impact these fields into the future. We focus on three broad topics: the construction and management of Knowledge Graphs (KGs), the use of KGs and associated technologies in the discovery of new knowledge, and the use of KGs in artificial intelligence applications to support explanations (explainable AI). We select a few exemplary use cases for each topic, discuss the challenges and open research questions within these topics, and conclude with a perspective and outlook that summarizes the overarching challenges and their potential solutions as a guide for future research.
Cite as

Jiaoyan Chen, Hang Dong, Janna Hastings, Ernesto Jiménez-Ruiz, Vanessa López, Pierre Monnin, Catia Pesquita, Petr Škoda, and Valentina Tamma. Knowledge Graphs for the Life Sciences: Recent Developments, Challenges and Opportunities. In Special Issue on Trends in Graph Data and Knowledge. Transactions on Graph Data and Knowledge (TGDK), Volume 1, Issue 1, pp. 5:1-5:33, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@Article{chen_et_al:TGDK.1.1.5,
  author =	{Chen, Jiaoyan and Dong, Hang and Hastings, Janna and Jim\'{e}nez-Ruiz, Ernesto and L\'{o}pez, Vanessa and Monnin, Pierre and Pesquita, Catia and \v{S}koda, Petr and Tamma, Valentina},
  title =	{{Knowledge Graphs for the Life Sciences: Recent Developments, Challenges and Opportunities}},
  journal =	{Transactions on Graph Data and Knowledge},
  pages =	{5:1--5:33},
  year =	{2023},
  volume =	{1},
  number =	{1},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/TGDK.1.1.5},
  URN =		{urn:nbn:de:0030-drops-194791},
  doi =		{10.4230/TGDK.1.1.5},
  annote =	{Keywords: Knowledge graphs, Life science, Knowledge discovery, Explainable AI}
}
Document
Survey
DOI: 10.4230/TGDK.1.1.11
How Does Knowledge Evolve in Open Knowledge Graphs?

Authors: Axel Polleres, Romana Pernisch, Angela Bonifati, Daniele Dell'Aglio, Daniil Dobriy, Stefania Dumbrava, Lorena Etcheverry, Nicolas Ferranti, Katja Hose, Ernesto Jiménez-Ruiz, Matteo Lissandrini, Ansgar Scherp, Riccardo Tommasini, and Johannes Wachs

Published in: TGDK, Volume 1, Issue 1 (2023): Special Issue on Trends in Graph Data and Knowledge. Transactions on Graph Data and Knowledge, Volume 1, Issue 1

Abstract
Openly available, collaboratively edited Knowledge Graphs (KGs) are key platforms for the collective management of evolving knowledge. The present work aims t o provide an analysis of the obstacles related to investigating and processing specifically this central aspect of evolution in KGs. To this end, we discuss (i) the dimensions of evolution in KGs, (ii) the observability of evolution in existing, open, collaboratively constructed Knowledge Graphs over time, and (iii) possible metrics to analyse this evolution. We provide an overview of relevant state-of-the-art research, ranging from metrics developed for Knowledge Graphs specifically to potential methods from related fields such as network science. Additionally, we discuss technical approaches - and their current limitations - related to storing, analysing and processing large and evolving KGs in terms of handling typical KG downstream tasks.
Cite as

Axel Polleres, Romana Pernisch, Angela Bonifati, Daniele Dell'Aglio, Daniil Dobriy, Stefania Dumbrava, Lorena Etcheverry, Nicolas Ferranti, Katja Hose, Ernesto Jiménez-Ruiz, Matteo Lissandrini, Ansgar Scherp, Riccardo Tommasini, and Johannes Wachs. How Does Knowledge Evolve in Open Knowledge Graphs?. In Special Issue on Trends in Graph Data and Knowledge. Transactions on Graph Data and Knowledge (TGDK), Volume 1, Issue 1, pp. 11:1-11:59, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@Article{polleres_et_al:TGDK.1.1.11,
  author =	{Polleres, Axel and Pernisch, Romana and Bonifati, Angela and Dell'Aglio, Daniele and Dobriy, Daniil and Dumbrava, Stefania and Etcheverry, Lorena and Ferranti, Nicolas and Hose, Katja and Jim\'{e}nez-Ruiz, Ernesto and Lissandrini, Matteo and Scherp, Ansgar and Tommasini, Riccardo and Wachs, Johannes},
  title =	{{How Does Knowledge Evolve in Open Knowledge Graphs?}},
  journal =	{Transactions on Graph Data and Knowledge},
  pages =	{11:1--11:59},
  year =	{2023},
  volume =	{1},
  number =	{1},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/TGDK.1.1.11},
  URN =		{urn:nbn:de:0030-drops-194855},
  doi =		{10.4230/TGDK.1.1.11},
  annote =	{Keywords: KG evolution, temporal KG, versioned KG, dynamic KG}
}
Document
DOI: 10.4230/LIPIcs.ITP.2022.8
Seventeen Provers Under the Hammer

Authors: Martin Desharnais, Petar Vukmirović, Jasmin Blanchette, and Makarius Wenzel

Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)

Abstract
One of the main success stories of automatic theorem provers has been their integration into proof assistants. Such integrations, or "hammers," increase proof automation and hence user productivity. In this paper, we use Isabelle/HOL’s Sledgehammer tool to find out how useful modern provers are at proving formulas in higher-order logic. Our evaluation follows in the steps of Böhme and Nipkow’s Judgment Day study from 2010, but instead of three provers we use 17, including SMT solvers and higher-order provers. Our work offers an alternative yardstick for comparing modern provers, next to the benchmarks and competitions emerging from the TPTP World and SMT-LIB.
Cite as

Martin Desharnais, Petar Vukmirović, Jasmin Blanchette, and Makarius Wenzel. Seventeen Provers Under the Hammer. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{desharnais_et_al:LIPIcs.ITP.2022.8,
  author =	{Desharnais, Martin and Vukmirovi\'{c}, Petar and Blanchette, Jasmin and Wenzel, Makarius},
  title =	{{Seventeen Provers Under the Hammer}},
  booktitle =	{13th International Conference on Interactive Theorem Proving (ITP 2022)},
  pages =	{8:1--8:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-252-5},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{237},
  editor =	{Andronick, June and de Moura, Leonardo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.8},
  URN =		{urn:nbn:de:0030-drops-167178},
  doi =		{10.4230/LIPIcs.ITP.2022.8},
  annote =	{Keywords: Automatic theorem proving, interactive theorem proving, proof assistants}
}
Document
DOI: 10.4230/DagSemProc.05431.1
05431 Abstracts Collection – Deduction and Applications

Authors: Franz Baader, Peter Baumgartner, Robert Nieuwenhuis, and Andrei Voronkov

Published in: Dagstuhl Seminar Proceedings, Volume 5431, Deduction and Applications (2006)

Abstract
From 23.10.05 to 28.10.05, the Dagstuhl Seminar 05431 ``Deduction and Applications'' was held in the International Conference and Research Center (IBFI), Schloss Dagstuhl. During the seminar, several participants presented their current research, and ongoing work and open problems were discussed. Abstracts of the presentations given during the seminar as well as abstracts of seminar results and ideas are put together in this paper. The first section describes the seminar topics and goals in general. Links to extended abstracts or full papers are provided, if available.
Cite as

Franz Baader, Peter Baumgartner, Robert Nieuwenhuis, and Andrei Voronkov. 05431 Abstracts Collection – Deduction and Applications. In Deduction and Applications. Dagstuhl Seminar Proceedings, Volume 5431, pp. 1-23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{baader_et_al:DagSemProc.05431.1,
  author =	{Baader, Franz and Baumgartner, Peter and Nieuwenhuis, Robert and Voronkov, Andrei},
  title =	{{05431 Abstracts Collection – Deduction and Applications}},
  booktitle =	{Deduction and Applications},
  pages =	{1--23},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{5431},
  editor =	{Franz Baader and Peter Baumgartner and Robert Nieuwenhuis and Andrei Voronkov},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.05431.1},
  URN =		{urn:nbn:de:0030-drops-5625},
  doi =		{10.4230/DagSemProc.05431.1},
  annote =	{Keywords: Formal logic, deduction, artificial intelligence}
}
Document
DOI: 10.4230/DagSemProc.05431.5
Proof Presentation

Authors: Jörg Siekmann

Published in: Dagstuhl Seminar Proceedings, Volume 5431, Deduction and Applications (2006)

Abstract
The talk is based on a book about the human-oriented presentation of a mathematical proof in natural language, in a style as we may find it in a typical mathematical text book. How can a proof be other than human-oriented? What we have in mind is a deduction systems, which is implemented on a computer, that proves – with some human interaction – a mathematical textbook as may be used in an undergraduate course. The proofs generated by these systems today are far from being human-oriented and can in general only be read by an expert in the respective field: proofs between several hundred (for a common mathematical theorem), for more than a thousand steps (for an unusually difficult theorem) and more than ten thousand deduction steps (in a program verification task) are not uncommon. Although these proofs are provably correct, they are typically marred by many problems: to start with, that are usually written in a highly specialised logic such as the resolution calculus, in a matrix format, or even worse, they may be generated by a model checker. Moreover they record every logical step that may be necessary for the minute detail of some term transformation (such as, for example, the rearrangement of brackets) along side those arguments, a mathematician would call important steps or heureka-steps that capture the main idea of the proof. Only these would he be willing to communicate to his fellow mathematicians – provided they have a similar academic background and work in the same mathematical discipline. If not, i.e. if the proof was written say for an undergraduate textbook, the option of an important step may be viewed differently depending on the intended reader. Now, even if we were able to isolate the ten important steps – out of those hundreds of machine generated proof steps – there would still be the startling problem that they are usually written in the "wrong" order. A human reader might say: "they do not have a logical structure"; which is to say that of course they follow a logical pattern (as they are correctly generated by a machine), but, given the convention of the respective field and the way the trained mathematician in this field is used to communicate, they are somewhat strange and ill structured. And finally, there is the problem that proofs are purely formal and recorded in a predicate logic that is very far from the usual presentation that relies on a mixture of natural language arguments interspersed with some formalism. The book (about 800 page) which gives an answer to some of these problems is to appear with Elsevier
Cite as

Jörg Siekmann. Proof Presentation. In Deduction and Applications. Dagstuhl Seminar Proceedings, Volume 5431, pp. 1-7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{siekmann:DagSemProc.05431.5,
  author =	{Siekmann, J\"{o}rg},
  title =	{{Proof Presentation}},
  booktitle =	{Deduction and Applications},
  pages =	{1--7},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{5431},
  editor =	{Franz Baader and Peter Baumgartner and Robert Nieuwenhuis and Andrei Voronkov},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.05431.5},
  URN =		{urn:nbn:de:0030-drops-5611},
  doi =		{10.4230/DagSemProc.05431.5},
  annote =	{Keywords: Artificial intelligence, mathematics, proof presentation}
}
Document
DOI: 10.4230/DagSemProc.05431.2
05431 Executive Summary – Deduction and Applications

Authors: Franz Baader, Peter Baumgartner, Robert Nieuwenhuis, and Andrei Voronkov

Published in: Dagstuhl Seminar Proceedings, Volume 5431, Deduction and Applications (2006)

Abstract
Formal logic provides a mathematical foundation for many areas of computer science. Logical languages are used as specification language within, e.g., program development and verification, hardware design and verification, relational databases, and many subfields of Artificial Intelligence. Automated Deduction is concerned with the design and implementation of algorithms based on logical deduction for solving problems in these areas. The last years have seen considerable improvements concerning both basic automated deduction technology and its (real-world) applications. Accordingly, the goal of the seminar was to bring together researchers from both sides in order to get an overview of the state of the art, and also to get ideas how to advance automated deduction from an application oriented point of view.
Cite as

Franz Baader, Peter Baumgartner, Robert Nieuwenhuis, and Andrei Voronkov. 05431 Executive Summary – Deduction and Applications. In Deduction and Applications. Dagstuhl Seminar Proceedings, Volume 5431, pp. 1-3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{baader_et_al:DagSemProc.05431.2,
  author =	{Baader, Franz and Baumgartner, Peter and Nieuwenhuis, Robert and Voronkov, Andrei},
  title =	{{05431 Executive Summary – Deduction and Applications}},
  booktitle =	{Deduction and Applications},
  pages =	{1--3},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{5431},
  editor =	{Franz Baader and Peter Baumgartner and Robert Nieuwenhuis and Andrei Voronkov},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.05431.2},
  URN =		{urn:nbn:de:0030-drops-5100},
  doi =		{10.4230/DagSemProc.05431.2},
  annote =	{Keywords: Formal logic, deduction, artificial intelligence}
}
Document
DOI: 10.4230/DagSemProc.05431.3
Automatically Generating Loop Invariants Using Quantifier Elimination

Authors: Deepak Kapur

Published in: Dagstuhl Seminar Proceedings, Volume 5431, Deduction and Applications (2006)

Abstract
An approach for automatically generating loop invariants using quantifier-elimination is proposed. An invariant of a loop is hypothesized as a parameterized formula. Parameters in the invariant are discovered by generating constraints on the parameters by ensuring that the formula is indeed preserved by the execution path corresponding to every basic cycle of the loop. The parameterized formula can be successively refined by considering execution paths one by one; heuristics can be developed for determining the order in which the paths are considered. Initialization of program variables as well as the precondition and postcondition of the loop, if available, can also be used to further refine the hypothesized invariant. Constraints on parameters generated in this way are solved for possible values of parameters. If no solution is possible, this means that an invariant of the hypothesized form does not exist for the loop. Otherwise, if the parametric constraints are solvable, then under certain conditions on methods for generating these constraints, the strongest possible invariant of the hypothesized form can be generated from most general solutions of the parametric constraints. The approach is illustrated using the first-order theory of polynomial equations as well as Presburger arithmetic.
Cite as

Deepak Kapur. Automatically Generating Loop Invariants Using Quantifier Elimination. In Deduction and Applications. Dagstuhl Seminar Proceedings, Volume 5431, pp. 1-17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{kapur:DagSemProc.05431.3,
  author =	{Kapur, Deepak},
  title =	{{Automatically Generating Loop Invariants Using Quantifier Elimination}},
  booktitle =	{Deduction and Applications},
  pages =	{1--17},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{5431},
  editor =	{Franz Baader and Peter Baumgartner and Robert Nieuwenhuis and Andrei Voronkov},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.05431.3},
  URN =		{urn:nbn:de:0030-drops-5116},
  doi =		{10.4230/DagSemProc.05431.3},
  annote =	{Keywords: Program verification, loop invariants, inductive assertions, quantifier elimination}
}
Document
DOI: 10.4230/DagSemProc.05431.4
On Algorithms and Complexity for Sets with Cardinality Constraints

Authors: Viktor Kuncak, Martin Rinard, and Bruno Marnette

Published in: Dagstuhl Seminar Proceedings, Volume 5431, Deduction and Applications (2006)

Abstract
Complexity of data structures in modern programs presents a challenge for current analysis and verification tools, forcing them to report false alarms or miss errors. I will describe a new approach for verifying programs with complex data structures. This approach builds on program analysis techniques, as well as decision procedures and theorem provers. The approach is based on specifying interfaces of data structures by writing procedure preconditions and postconditions in terms of abstract sets and relations. Our system then separately verifies that 1) each data structure conforms to its interface, 2) each data structure interface is used correctly, and 3) desired high-level application-specific invariants hold. The system verifies these conditions by combining decision procedures, theorem provers, and static analyses, promising an unprecedented tradeoff between precision and scalability. In the context of this system, we have developed new decision procedures for reasoning about sets and their cardinalities, approaches for extending the applicability of existing decision procedures, and techniques for modular analysis of dynamically created data structure instances.
Cite as

Viktor Kuncak, Martin Rinard, and Bruno Marnette. On Algorithms and Complexity for Sets with Cardinality Constraints. In Deduction and Applications. Dagstuhl Seminar Proceedings, Volume 5431, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{kuncak_et_al:DagSemProc.05431.4,
  author =	{Kuncak, Viktor and Rinard, Martin and Marnette, Bruno},
  title =	{{On Algorithms and Complexity for Sets with Cardinality Constraints}},
  booktitle =	{Deduction and Applications},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{5431},
  editor =	{Franz Baader and Peter Baumgartner and Robert Nieuwenhuis and Andrei Voronkov},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.05431.4},
  URN =		{urn:nbn:de:0030-drops-5125},
  doi =		{10.4230/DagSemProc.05431.4},
  annote =	{Keywords: Static analysis, data structure consistency, program verification, decision procedures}
}
Document
DOI: 10.4230/DagSemProc.05431.6
Proving and Disproving Termination in the Dependency Pair Framework

Authors: Jürgen Giesl, René Thiemann, and Peter Schneider-Kamp

Published in: Dagstuhl Seminar Proceedings, Volume 5431, Deduction and Applications (2006)

Abstract
The dependency pair framework is a new general concept to integrate arbitrary techniques for termination analysis of term rewriting. In this way, the benefits of different techniques can be combined and their modularity and power are increased significantly. Moreover, this framework facilitates the development of new methods for termination analysis. Traditionally, the research on termination focused on methods which prove termination and there were hardly any approaches for disproving termination. We show that with the dependency pair framework, one can combine the search for a proof and for a disproof of termination. In this way, we obtain the first powerful method which can also verify non-termination of term rewrite systems. We implemented and evaluated our contributions in the automated termination prover AProVE. Due to these results, AProVE was the winning tool in the International Competition of Termination Provers 2005, both for proving and for disproving termination of term rewriting.
Cite as

Jürgen Giesl, René Thiemann, and Peter Schneider-Kamp. Proving and Disproving Termination in the Dependency Pair Framework. In Deduction and Applications. Dagstuhl Seminar Proceedings, Volume 5431, p. 1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{giesl_et_al:DagSemProc.05431.6,
  author =	{Giesl, J\"{u}rgen and Thiemann, Ren\'{e} and Schneider-Kamp, Peter},
  title =	{{Proving and Disproving Termination in the Dependency Pair Framework}},
  booktitle =	{Deduction and Applications},
  pages =	{1--1},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{5431},
  editor =	{Franz Baader and Peter Baumgartner and Robert Nieuwenhuis and Andrei Voronkov},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.05431.6},
  URN =		{urn:nbn:de:0030-drops-5091},
  doi =		{10.4230/DagSemProc.05431.6},
  annote =	{Keywords: Termination, non-termination, term rewriting, dependency pairs}
}
  • Refine by Type
  • 15 Document/PDF
  • 8 Document/HTML

  • Refine by Publication Year
  • 2 2026
  • 3 2025
  • 3 2023
  • 1 2022
  • 6 2006

  • Refine by Author
  • 2 Baader, Franz
  • 2 Baumgartner, Peter
  • 2 Dumbrava, Stefania
  • 2 Jiménez-Ruiz, Ernesto
  • 2 Lissandrini, Matteo
  • Show More...

  • Refine by Series/Journal
  • 6 LIPIcs
  • 3 TGDK
  • 6 DagSemProc

  • Refine by Classification
  • 2 Information systems → Graph-based database models
  • 1 Applied computing → Life and medical sciences
  • 1 Computing methodologies → Knowledge representation and reasoning
  • 1 Computing methodologies → Logical and relational learning
  • 1 Computing methodologies → Machine learning approaches
  • Show More...

  • Refine by Keyword
  • 2 Formal logic
  • 2 artificial intelligence
  • 2 deduction
  • 1 Artificial intelligence
  • 1 Automatic theorem proving
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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