8 Search Results for "Ganzinger, Harald"

Document
DOI: 10.4230/LIPIcs.STACS.2026.37
Random Models and Guarded Logic

Authors: Oskar Fiuk

Published in: LIPIcs, Volume 364, 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)

Abstract
Building on ideas of Gurevich and Shelah for the Gödel Class, we present a new probabilistic proof of the finite model property for the Guarded Fragment of First-Order Logic. Our proof is conceptually simple and yields the optimal doubly-exponential upper bound on the size of minimal models. We precisely analyse the obtained bound, up to constant factors in the exponents, and construct sentences that enforce models of tightly matching size. The probabilistic approach adapts naturally to the Triguarded Fragment, an extension of the Guarded Fragment that also subsumes the Two-Variable Fragment. Finally, we derandomise the probabilistic proof by providing an explicit model construction which replaces randomness with deterministic hash functions.
Cite as

Oskar Fiuk. Random Models and Guarded Logic. In 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 364, pp. 37:1-37:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{fiuk:LIPIcs.STACS.2026.37,
  author =	{Fiuk, Oskar},
  title =	{{Random Models and Guarded Logic}},
  booktitle =	{43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)},
  pages =	{37:1--37:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-412-3},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{364},
  editor =	{Mahajan, Meena and Manea, Florin and McIver, Annabelle 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.2026.37},
  URN =		{urn:nbn:de:0030-drops-255269},
  doi =		{10.4230/LIPIcs.STACS.2026.37},
  annote =	{Keywords: guarded fragment, finite model property, probabilistic method}
}
Document
DOI: 10.4230/LIPIcs.ITP.2025.11
Animating MRBNFs: Truly Modular Binding-Aware Datatypes in Isabelle/HOL

Authors: Jan van Brügge, Andrei Popescu, and Dmitriy Traytel

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

Abstract
Nominal Isabelle provides powerful tools for meta-theoretic reasoning about syntax of logics or programming languages, in which variables are bound. It has been instrumental to major verification successes, such as Gödel’s incompleteness theorems. However, the existing tooling is not compositional. In particular, it does not support nested recursion, linear binding patterns, or infinitely branching syntax. These limitations are fundamental in the way nominal datatypes and functions on them are constructed within Nominal Isabelle. Taking advantage of recent theoretical advancements that overcome these limitations through a modular approach using the concept of map-restricted bounded natural functor (MRBNF), we develop and implement a new definitional package for binding-aware datatypes in Isabelle/HOL, called MrBNF. We describe the journey from the user specification to the end-product types, constants and theorems the tool generates. We validate MrBNF in two formalization case studies that so far were out of reach of nominal approaches: (1) Mazza’s isomorphism between the finitary and the infinitary affine λ-calculus, and (2) the POPLmark 2B challenge, which involves non-free binders for linear pattern matching.
Cite as

Jan van Brügge, Andrei Popescu, and Dmitriy Traytel. Animating MRBNFs: Truly Modular Binding-Aware Datatypes in Isabelle/HOL. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 11:1-11:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{vanbrugge_et_al:LIPIcs.ITP.2025.11,
  author =	{van Br\"{u}gge, Jan and Popescu, Andrei and Traytel, Dmitriy},
  title =	{{Animating MRBNFs: Truly Modular Binding-Aware Datatypes in Isabelle/HOL}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{11:1--11:20},
  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.11},
  URN =		{urn:nbn:de:0030-drops-246091},
  doi =		{10.4230/LIPIcs.ITP.2025.11},
  annote =	{Keywords: syntax with bindings, datatypes, inductive predicates, Isabelle/HOL}
}
Document
DOI: 10.4230/LIPIcs.ITP.2025.22
Formalizing Splitting in Isabelle/HOL

Authors: Ghilain Bergeron, Florent Krasnopol, and Sophie Tourret

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

Abstract
We describe the formalization in Isabelle/HOL of a framework for splitting, a theorem proving technique that extends saturation-based calculi with branching abilities. The framework preserves the completeness of the original calculus. We focus here on the simplest splitting model and provide an extension of the ordered resolution calculus with a variant of splitting called Lightweight AVATAR.
Cite as

Ghilain Bergeron, Florent Krasnopol, and Sophie Tourret. Formalizing Splitting in Isabelle/HOL. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 22:1-22:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bergeron_et_al:LIPIcs.ITP.2025.22,
  author =	{Bergeron, Ghilain and Krasnopol, Florent and Tourret, Sophie},
  title =	{{Formalizing Splitting in Isabelle/HOL}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{22:1--22:19},
  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.22},
  URN =		{urn:nbn:de:0030-drops-246208},
  doi =		{10.4230/LIPIcs.ITP.2025.22},
  annote =	{Keywords: Isabelle/HOL, saturation-based calculi, splitting}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2025.8
The Unification Type of an Equational Theory May Depend on the Instantiation Preorder

Authors: Franz Baader and Oliver Fernández Gil

Published in: LIPIcs, Volume 337, 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)

Abstract
The unification type of an equational theory is defined using a preorder on substitutions, called the instantiation preorder, whose scope is either restricted to the variables occurring in the unification problem, or unrestricted such that all variables are considered. It has been known for more than three decades that the unification type of an equational theory may vary, depending on which instantiation preorder is used. More precisely, it was shown in 1991 that the theory ACUI of an associative, commutative, and idempotent binary function symbol with a unit is unitary w.r.t. the restricted instantiation preorder, but not unitary w.r.t. the unrestricted one. In 2016 this result was strengthened by showing that the unrestricted type of this theory also cannot be finitary. Here, we considerably improve on this result by proving that ACUI is infinitary w.r.t. the unrestricted instantiation preorder, thus precluding type zero. We also show that, w.r.t. this preorder, the unification type of ACU (where idempotency is removed from the axioms) and of AC (where additionally the unit is removed) is infinitary, though it is respectively unitary and finitary in the restricted case. In the other direction, we prove (using the example of unification in the description logic EL) that the unification type may actually improve from type zero to infinitary when switching from the restricted instantiation preorder to the unrestricted one. In addition, we establish some general results on the relationship between the two instantiation preorders.
Cite as

Franz Baader and Oliver Fernández Gil. The Unification Type of an Equational Theory May Depend on the Instantiation Preorder. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 8:1-8:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{baader_et_al:LIPIcs.FSCD.2025.8,
  author =	{Baader, Franz and Fern\'{a}ndez Gil, Oliver},
  title =	{{The Unification Type of an Equational Theory May Depend on the Instantiation Preorder}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{8:1--8:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-374-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{337},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.8},
  URN =		{urn:nbn:de:0030-drops-236230},
  doi =		{10.4230/LIPIcs.FSCD.2025.8},
  annote =	{Keywords: Unification type, Instantiation preorder, Equational theories, Modal and Description Logics}
}
Document
DOI: 10.4230/DagSemRep.401
Applied Deductive Verification (Dagstuhl Seminar 03451)

Authors: David Basin, Harald Ganzinger, John R. Harrison, and Amir Pnueli

Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)

Abstract
Cite as

David Basin, Harald Ganzinger, John R. Harrison, and Amir Pnueli. Applied Deductive Verification (Dagstuhl Seminar 03451). Dagstuhl Seminar Report 401, pp. 1-6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2003)

Copy BibTex To Clipboard

@TechReport{basin_et_al:DagSemRep.401,
  author =	{Basin, David and Ganzinger, Harald and Harrison, John R. and Pnueli, Amir},
  title =	{{Applied Deductive Verification (Dagstuhl Seminar 03451)}},
  pages =	{1--6},
  ISSN =	{1619-0203},
  year =	{2003},
  type = 	{Dagstuhl Seminar Report},
  number =	{401},
  institution =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemRep.401},
  URN =		{urn:nbn:de:0030-drops-152813},
  doi =		{10.4230/DagSemRep.401},
}
Document
DOI: 10.4230/DagSemRep.300
Deduction (Dagstuhl Seminar 01101)

Authors: Ulrich Furbach, Harald Ganzinger, Ryuzo Hasegawa, and Deepak Kapur

Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)

Abstract
Cite as

Ulrich Furbach, Harald Ganzinger, Ryuzo Hasegawa, and Deepak Kapur. Deduction (Dagstuhl Seminar 01101). Dagstuhl Seminar Report 300, pp. 1-27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2001)

Copy BibTex To Clipboard

@TechReport{furbach_et_al:DagSemRep.300,
  author =	{Furbach, Ulrich and Ganzinger, Harald and Hasegawa, Ryuzo and Kapur, Deepak},
  title =	{{Deduction (Dagstuhl Seminar 01101)}},
  pages =	{1--27},
  ISSN =	{1619-0203},
  year =	{2001},
  type = 	{Dagstuhl Seminar Report},
  number =	{300},
  institution =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemRep.300},
  URN =		{urn:nbn:de:0030-drops-151843},
  doi =		{10.4230/DagSemRep.300},
}
Document
DOI: 10.4230/DagSemRep.232
Deduction (Dagstuhl Seminar 99091)

Authors: Ulrich Furbach, Harald Ganzinger, Ryuzo Hasegawa, and Deepak Kapur

Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)

Abstract
Cite as

Ulrich Furbach, Harald Ganzinger, Ryuzo Hasegawa, and Deepak Kapur. Deduction (Dagstuhl Seminar 99091). Dagstuhl Seminar Report 232, pp. 1-24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2000)

Copy BibTex To Clipboard

@TechReport{furbach_et_al:DagSemRep.232,
  author =	{Furbach, Ulrich and Ganzinger, Harald and Hasegawa, Ryuzo and Kapur, Deepak},
  title =	{{Deduction (Dagstuhl Seminar 99091)}},
  pages =	{1--24},
  ISSN =	{1619-0203},
  year =	{2000},
  type = 	{Dagstuhl Seminar Report},
  number =	{232},
  institution =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemRep.232},
  URN =		{urn:nbn:de:0030-drops-151182},
  doi =		{10.4230/DagSemRep.232},
}
Document
DOI: 10.4230/DagSemRep.24
Theorem Proving and Logic Programming with Constraints (Dagstuhl Seminar 9143)

Authors: Hubert Comon, Harald Ganzinger, Claude Kirchner, Hélène Kirchner, Jean-Louis Lassez, and Gert Smolka

Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)

Abstract
Cite as

Hubert Comon, Harald Ganzinger, Claude Kirchner, Hélène Kirchner, Jean-Louis Lassez, and Gert Smolka. Theorem Proving and Logic Programming with Constraints (Dagstuhl Seminar 9143). Dagstuhl Seminar Report 24, pp. 1-24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (1992)

Copy BibTex To Clipboard

@TechReport{comon_et_al:DagSemRep.24,
  author =	{Comon, Hubert and Ganzinger, Harald and Kirchner, Claude and Kirchner, H\'{e}l\`{e}ne and Lassez, Jean-Louis and Smolka, Gert},
  title =	{{Theorem Proving and Logic Programming with Constraints (Dagstuhl Seminar 9143)}},
  pages =	{1--24},
  ISSN =	{1619-0203},
  year =	{1992},
  type = 	{Dagstuhl Seminar Report},
  number =	{24},
  institution =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemRep.24},
  URN =		{urn:nbn:de:0030-drops-149127},
  doi =		{10.4230/DagSemRep.24},
}
  • Refine by Type
  • 8 Document/PDF
  • 4 Document/HTML

  • Refine by Publication Year
  • 1 2026
  • 3 2025
  • 1 2003
  • 1 2001
  • 1 2000
  • Show More...

  • Refine by Author
  • 4 Ganzinger, Harald
  • 2 Furbach, Ulrich
  • 2 Hasegawa, Ryuzo
  • 2 Kapur, Deepak
  • 1 Baader, Franz
  • Show More...

  • Refine by Series/Journal
  • 4 LIPIcs
  • 4 DagSemRep

  • Refine by Classification
  • 1 Computing methodologies → Theorem proving algorithms
  • 1 Security and privacy → Logic and verification
  • 1 Theory of computation → Automated reasoning
  • 1 Theory of computation → Description logics
  • 1 Theory of computation → Equational logic and rewriting
  • Show More...

  • Refine by Keyword
  • 2 Isabelle/HOL
  • 1 Equational theories
  • 1 Instantiation preorder
  • 1 Modal and Description Logics
  • 1 Unification type
  • 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