53 Search Results for "Kaliszyk, Cezary"

Volume

LIPIcs, Volume 193

12th International Conference on Interactive Theorem Proving (ITP 2021)

ITP 2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)

Editors: Liron Cohen and Cezary Kaliszyk

Document
DOI: 10.4230/LIPIcs.CSL.2026.18
A Modular Framework for Proof-Search via Formalised Modal Completeness in HOL Light

Authors: Antonella Bilotta, Marco Maggesi, and Cosimo Perini Brogi

Published in: LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Abstract
We extend the existing HOL Light Library for Modal Systems (HOLMS) to support a modular implementation of modal reasoning within the HOL Light proof assistant. We deeply embed axiomatic calculi and relational semantics for seven normal modal logics (K, T, B, K4, S4, S5, GL) and formalise modal adequacy theorems for these systems. We then leverage those formalisations to implement a mechanism for automated reasoning via proof-search in the associated labelled sequent calculi, which we shallowly embed in HOL Light’s goal-stack mechanism. This way, we equip the general-purpose proof assistant with (semi)decision procedures for these logics that, in case of failure to construct a proof for the input formula, return a certified countermodel within the appropriate class for the logic under consideration. On the methodological side, we propose a precise measure of the modularity of our approach by systematically adopting Christopher Strachey’s distinction between ad hoc and parametric polymorphism throughout the library.
Cite as

Antonella Bilotta, Marco Maggesi, and Cosimo Perini Brogi. A Modular Framework for Proof-Search via Formalised Modal Completeness in HOL Light. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 18:1-18:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{bilotta_et_al:LIPIcs.CSL.2026.18,
  author =	{Bilotta, Antonella and Maggesi, Marco and Perini Brogi, Cosimo},
  title =	{{A Modular Framework for Proof-Search via Formalised Modal Completeness in HOL Light}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{18:1--18:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.18},
  URN =		{urn:nbn:de:0030-drops-254427},
  doi =		{10.4230/LIPIcs.CSL.2026.18},
  annote =	{Keywords: Modal logic, HOL Light, Labelled sequent calculi, Logical verification, Interactive theorem proving, Automated proof-search}
}
Document
DOI: 10.4230/LIPIcs.AFT.2025.25
The Exchange Problem

Authors: Mohit Garg and Suneel Sarswat

Published in: LIPIcs, Volume 354, 7th Conference on Advances in Financial Technologies (AFT 2025)

Abstract
Auctions are widely used in exchanges to match buy and sell requests. Once the buyers and sellers place their requests, the exchange determines how these requests are to be matched. The two most popular objectives used while determining the matching are maximizing volume with dynamic pricing and maximizing volume at a uniform price. In this work, we study the algorithmic complexity of the problems arising from these matching tasks. For dynamic-price matching, we establish a lower bound of Ω(n log n) on the running time, thereby proving that the currently best-known O(n log n) algorithm is time-optimal. In contrast, for uniform-price matching, we present a linear-time algorithm, improving upon previous methods that require O(n log n) time to match n requests.
Cite as

Mohit Garg and Suneel Sarswat. The Exchange Problem. In 7th Conference on Advances in Financial Technologies (AFT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 354, pp. 25:1-25:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{garg_et_al:LIPIcs.AFT.2025.25,
  author =	{Garg, Mohit and Sarswat, Suneel},
  title =	{{The Exchange Problem}},
  booktitle =	{7th Conference on Advances in Financial Technologies (AFT 2025)},
  pages =	{25:1--25:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-400-0},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{354},
  editor =	{Avarikioti, Zeta and Christin, Nicolas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.AFT.2025.25},
  URN =		{urn:nbn:de:0030-drops-247449},
  doi =		{10.4230/LIPIcs.AFT.2025.25},
  annote =	{Keywords: Exchanges, Double Auctions, Matching Algorithms, Element Distinctness, Time Complexity}
}
Document
DOI: 10.4230/LIPIcs.ITP.2025.7
A Verified Cost Model for Call-By-Push-Value

Authors: Zhuo Zoey Chen, Johannes Åman Pohjola, and Christine Rizkallah

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

Abstract
The call-by-push-value λ-calculus allows for syntactically specifying the order of evaluation as part of the term language. Hence, it serves as a unifying language for embedding various evaluation strategies including call-by-value and call-by-name. Given the impact of call-by-push-value, it is remarkable that its adequacy as a model for computational complexity theory has not yet been studied. In this paper, we show that the call-by-push-value λ-calculus is reasonable for both time and space complexity. A reasonable cost model can encode other reasonable cost models with polynomial overhead in time and constant factor overhead in space. We achieve this by encoding call-by-push-value λ-calculus into Turing machines, following a simulation strategy by Forster et al.; for the converse direction, we prove that Levy’s encoding of the call-by-value λ-calculus has reasonable complexity bounds. The main results have been formalised in the HOL4 theorem prover.
Cite as

Zhuo Zoey Chen, Johannes Åman Pohjola, and Christine Rizkallah. A Verified Cost Model for Call-By-Push-Value. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 7:1-7:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{chen_et_al:LIPIcs.ITP.2025.7,
  author =	{Chen, Zhuo Zoey and \r{A}man Pohjola, Johannes and Rizkallah, Christine},
  title =	{{A Verified Cost Model for Call-By-Push-Value}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{7:1--7: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.7},
  URN =		{urn:nbn:de:0030-drops-246067},
  doi =		{10.4230/LIPIcs.ITP.2025.7},
  annote =	{Keywords: lambda calculus, formalizations of computational models, computability theory, HOL, call-by-push-value reduction, time and space complexity, abstract machines}
}
Document
DOI: 10.4230/LIPIcs.ITP.2025.36
Verifying Datalog Reasoning with Lean

Authors: Johannes Tantow, Lukas Gerlach, Stephan Mennicke, and Markus Krötzsch

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

Abstract
Datalog is an essential logical rule language with many applications, and modern rule engines compute logical consequences for Datalog with high performance and scalability. While Datalog is rather simple and, in principle, explainable by design, such sophisticated implementations and optimizations are hard to verify. We therefore propose a certificate-based approach to validate results of Datalog reasoners in a formally verified checker for Datalog proofs. Using the proof assistant Lean, we implement such a checker and verify its correctness against direct formalizations of the Datalog semantics. We propose two JSON encodings for Datalog proofs: one using the widely supported Datalog proof trees, and one using directed acyclic graphs for succinctness. To evaluate the practical feasibility and performance of our approach, we validate proofs that we obtain by converting derivation traces of an existing Datalog reasoner into our tool-independent format.
Cite as

Johannes Tantow, Lukas Gerlach, Stephan Mennicke, and Markus Krötzsch. Verifying Datalog Reasoning with Lean. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 36:1-36:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{tantow_et_al:LIPIcs.ITP.2025.36,
  author =	{Tantow, Johannes and Gerlach, Lukas and Mennicke, Stephan and Kr\"{o}tzsch, Markus},
  title =	{{Verifying Datalog Reasoning with Lean}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{36:1--36: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.36},
  URN =		{urn:nbn:de:0030-drops-246342},
  doi =		{10.4230/LIPIcs.ITP.2025.36},
  annote =	{Keywords: Certifying Algorithms, Datalog, Formal Verification}
}
Document
Short Paper
DOI: 10.4230/LIPIcs.ITP.2025.38
Sledgehammering Without ATPs (Short Paper)

Authors: Martin Desharnais and Jasmin Blanchette

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

Abstract
We describe an alternative architecture for "hammers," inspired by Magnushammer, in which proofs are found by the proof assistant’s built-in automation instead of by external automatic theorem provers (ATPs). We implemented this approach in Isabelle’s Sledgehammer and evaluated it. The new ATP-free approach nicely complements the traditional Sledgehammer. The two approaches in combination solve more goals than the traditional ATP-based approach alone.
Cite as

Martin Desharnais and Jasmin Blanchette. Sledgehammering Without ATPs (Short Paper). In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 38:1-38:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{desharnais_et_al:LIPIcs.ITP.2025.38,
  author =	{Desharnais, Martin and Blanchette, Jasmin},
  title =	{{Sledgehammering Without ATPs}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{38:1--38:8},
  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.38},
  URN =		{urn:nbn:de:0030-drops-246366},
  doi =		{10.4230/LIPIcs.ITP.2025.38},
  annote =	{Keywords: Interactive theorem proving, proof assistants, proof automation}
}
Document
DOI: 10.4230/LIPIcs.ITP.2025.30
Nondeterministic Asynchronous Dataflow in Isabelle/HOL

Authors: Rafael Castro Gonçalves Silva, Laouen Fernet, and Dmitriy Traytel

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

Abstract
We formalize nondeterministic asynchronous dataflow networks in Isabelle/HOL. Dataflow networks are comprised of operators that are capable of communicating with the network, performing silent computations, and making nondeterministic choices. We represent operators using a shallow embedding as codatatypes. Using this representation, we define standard asynchronous dataflow primitives, including sequential and parallel composition and a feedback operator. These primitives adhere to a number of laws from the literature, which we prove by coinduction using weak bisimilarity as our equality. Albeit coinductive and nondeterministic, our model is executable via code extraction to Haskell.
Cite as

Rafael Castro Gonçalves Silva, Laouen Fernet, and Dmitriy Traytel. Nondeterministic Asynchronous Dataflow in Isabelle/HOL. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 30:1-30:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{silva_et_al:LIPIcs.ITP.2025.30,
  author =	{Silva, Rafael Castro Gon\c{c}alves and Fernet, Laouen and Traytel, Dmitriy},
  title =	{{Nondeterministic Asynchronous Dataflow in Isabelle/HOL}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{30:1--30: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.30},
  URN =		{urn:nbn:de:0030-drops-246280},
  doi =		{10.4230/LIPIcs.ITP.2025.30},
  annote =	{Keywords: dataflow, verification, coinduction, Isabelle/HOL}
}
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.14
Canonical for Automated Theorem Proving in Lean

Authors: Chase Norman and Jeremy Avigad

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

Abstract
Canonical is a solver for type inhabitation in dependent type theory, that is, the problem of producing a term of a given type. We present a Lean tactic which invokes Canonical to generate proof terms and synthesize programs. The tactic supports higher-order and dependently-typed goals, structural recursion over indexed inductive types, and definitional equality. Canonical finds proofs for 84% of Natural Number Game problems in 51 seconds total.
Cite as

Chase Norman and Jeremy Avigad. Canonical for Automated Theorem Proving in Lean. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 14:1-14:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{norman_et_al:LIPIcs.ITP.2025.14,
  author =	{Norman, Chase and Avigad, Jeremy},
  title =	{{Canonical for Automated Theorem Proving in Lean}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{14:1--14: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.14},
  URN =		{urn:nbn:de:0030-drops-246128},
  doi =		{10.4230/LIPIcs.ITP.2025.14},
  annote =	{Keywords: Automated Reasoning, Interactive Theorem Proving, Dependent Type Theory, Inhabitation, Unification, Program Synthesis, Formal Methods}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2025.7
Combining Generalization Algorithms in Regular Collapse-Free Theories

Authors: Mauricio Ayala-Rincón, David M. Cerna, Temur Kutsia, and Christophe Ringeissen

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

Abstract
We look at the generalization problem modulo some equational theories. This problem is dual to the unification problem: given two input terms, we want to find a common term whose respective two instances are equivalent to the original terms modulo the theory. There exist algorithms for finding generalizations over various equational theories. We focus on modular construction of equational generalization algorithms for the union of signature-disjoint theories. Specifically, we consider the class of regular and collapse-free theories, showing how to combine existing generalization algorithms to produce specific solutions in these cases. Additionally, we identify a class of theories that admit a generalization algorithm based on the application of axioms to resolve the problem. To define this class, we rely on the notion of syntactic theories, a concept originally introduced to develop unification procedures similar to the one known for syntactic unification. We demonstrate that syntactic theories are also helpful in developing generalization procedures similar to those used for syntactic generalization.
Cite as

Mauricio Ayala-Rincón, David M. Cerna, Temur Kutsia, and Christophe Ringeissen. Combining Generalization Algorithms in Regular Collapse-Free Theories. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 7:1-7:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{ayalarincon_et_al:LIPIcs.FSCD.2025.7,
  author =	{Ayala-Rinc\'{o}n, Mauricio and Cerna, David M. and Kutsia, Temur and Ringeissen, Christophe},
  title =	{{Combining Generalization Algorithms in Regular Collapse-Free Theories}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{7:1--7:18},
  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.7},
  URN =		{urn:nbn:de:0030-drops-236228},
  doi =		{10.4230/LIPIcs.FSCD.2025.7},
  annote =	{Keywords: Generalization, Anti-unification, Equational theories, Combination}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2025.27
What Does It Take to Certify a Conversion Checker?

Authors: Meven Lennon-Bertrand

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

Abstract
We report on a detailed exploration of the properties of conversion (definitional equality) in dependent type theory, with the goal of certifying decision procedures for it. While in that context the property of normalisation has attracted the most light, we instead emphasize the importance of injectivity properties, showing that they alone are both crucial and sufficient to certify most desirable properties of conversion checkers. We also explore the certification of a fully untyped conversion checker, with respect to a typed specification, and show that the story is mostly unchanged, although the exact injectivity properties needed are subtly different.
Cite as

Meven Lennon-Bertrand. What Does It Take to Certify a Conversion Checker?. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 27:1-27:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{lennonbertrand:LIPIcs.FSCD.2025.27,
  author =	{Lennon-Bertrand, Meven},
  title =	{{What Does It Take to Certify a Conversion Checker?}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{27:1--27:23},
  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.27},
  URN =		{urn:nbn:de:0030-drops-236428},
  doi =		{10.4230/LIPIcs.FSCD.2025.27},
  annote =	{Keywords: Dependent types, Bidirectional typing, Certified software}
}
Document
DOI: 10.4230/LIPIcs.CSL.2025.40
Completeness of First-Order Bi-Intuitionistic Logic

Authors: Dominik Kirst and Ian Shillito

Published in: LIPIcs, Volume 326, 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)

Abstract
We provide a succinct and verified completeness proof for first-order bi-intuitionistic logic, relative to constant domain Kripke semantics. By doing so, we make up for the almost-50-year-old substantial mistakes in Rauszer’s foundational work, detected but unresolved by Shillito two years ago. Moreover, an even earlier but historically neglected proof by Klemke has been found to contain at least local errors by Olkhovikov and Badia, that remained unfixed due to the technical complexity of Klemke’s argument. To resolve this unclear situation once and for all, we give a succinct completeness proof, based on and dualising a standard proof for constant domain intuitionistic logic, and verify our constructions using the Coq proof assistant to guarantee correctness.
Cite as

Dominik Kirst and Ian Shillito. Completeness of First-Order Bi-Intuitionistic Logic. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 40:1-40:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{kirst_et_al:LIPIcs.CSL.2025.40,
  author =	{Kirst, Dominik and Shillito, Ian},
  title =	{{Completeness of First-Order Bi-Intuitionistic Logic}},
  booktitle =	{33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
  pages =	{40:1--40:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-362-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{326},
  editor =	{Endrullis, J\"{o}rg and Schmitz, Sylvain},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2025.40},
  URN =		{urn:nbn:de:0030-drops-227979},
  doi =		{10.4230/LIPIcs.CSL.2025.40},
  annote =	{Keywords: bi-intuitionistic logic, first-order logic, completeness, Coq proof assistant}
}
Document
DOI: 10.4230/LIPIcs.ITP.2024.29
Conway Normal Form: Bridging Approaches for Comprehensive Formalization of Surreal Numbers

Authors: Karol Pąk and Cezary Kaliszyk

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

Abstract
The proper class of Conway’s surreal numbers forms a rich totally ordered algebraically closed field with many arithmetic and algebraic properties close to those of real numbers, the ordinals, and infinitesimal numbers. In this paper, we formalize the construction of Conway’s numbers in Mizar using two approaches and propose a bridge between them, aiming to combine their advantages for efficient formalization. By replacing transfinite induction-recursion with transfinite induction, we streamline their construction. Additionally, we introduce a method to merge proofs from both approaches using global choice, facilitating formal proof. We demonstrate that surreal numbers form a field, including the square root, and that they encompass subsets such as reals, ordinals, and powers of ω. We combined Conway’s work with Ehrlich’s generalization to formally prove Conway’s Normal Form, paving the way for many formal developments in surreal number theory.
Cite as

Karol Pąk and Cezary Kaliszyk. Conway Normal Form: Bridging Approaches for Comprehensive Formalization of Surreal Numbers. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 29:1-29:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{pak_et_al:LIPIcs.ITP.2024.29,
  author =	{P\k{a}k, Karol and Kaliszyk, Cezary},
  title =	{{Conway Normal Form: Bridging Approaches for Comprehensive Formalization of Surreal Numbers}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{29:1--29:18},
  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.29},
  URN =		{urn:nbn:de:0030-drops-207573},
  doi =		{10.4230/LIPIcs.ITP.2024.29},
  annote =	{Keywords: Surreal numbers, Conway normal form, Mizar}
}
Document
DOI: 10.4230/LIPIcs.ITP.2023.19
MizAR 60 for Mizar 50

Authors: Jan Jakubův, Karel Chvalovský, Zarathustra Goertzel, Cezary Kaliszyk, Mirek Olšák, Bartosz Piotrowski, Stephan Schulz, Martin Suda, and Josef Urban

Published in: LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023)

Abstract
As a present to Mizar on its 50th anniversary, we develop an AI/TP system that automatically proves about 60% of the Mizar theorems in the hammer setting. We also automatically prove 75% of the Mizar theorems when the automated provers are helped by using only the premises used in the human-written Mizar proofs. We describe the methods and large-scale experiments leading to these results. This includes in particular the E and Vampire provers, their ENIGMA and Deepire learning modifications, a number of learning-based premise selection methods, and the incremental loop that interleaves growing a corpus of millions of ATP proofs with training increasingly strong AI/TP systems on them. We also present a selection of Mizar problems that were proved automatically.
Cite as

Jan Jakubův, Karel Chvalovský, Zarathustra Goertzel, Cezary Kaliszyk, Mirek Olšák, Bartosz Piotrowski, Stephan Schulz, Martin Suda, and Josef Urban. MizAR 60 for Mizar 50. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 19:1-19:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{jakubuv_et_al:LIPIcs.ITP.2023.19,
  author =	{Jakub\r{u}v, Jan and Chvalovsk\'{y}, Karel and Goertzel, Zarathustra and Kaliszyk, Cezary and Ol\v{s}\'{a}k, Mirek and Piotrowski, Bartosz and Schulz, Stephan and Suda, Martin and Urban, Josef},
  title =	{{MizAR 60 for Mizar 50}},
  booktitle =	{14th International Conference on Interactive Theorem Proving (ITP 2023)},
  pages =	{19:1--19:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-284-6},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{268},
  editor =	{Naumowicz, Adam and Thiemann, Ren\'{e}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.19},
  URN =		{urn:nbn:de:0030-drops-183942},
  doi =		{10.4230/LIPIcs.ITP.2023.19},
  annote =	{Keywords: Mizar, ENIGMA, Automated Reasoning, Machine Learning}
}
Document
DOI: 10.4230/OASIcs.FMBC.2022.4
Proofgold: Blockchain for Formal Methods

Authors: Chad E. Brown, Cezary Kaliszyk, Thibault Gauthier, and Josef Urban

Published in: OASIcs, Volume 105, 4th International Workshop on Formal Methods for Blockchains (FMBC 2022)

Abstract
Proofgold is a peer to peer cryptocurrency making use of formal logic. Users can publish theories and then develop a theory by publishing documents with definitions, conjectures and proofs. The blockchain records the theories and their state of development (e.g., which theorems have been proven and when). Two of the main theories are a form of classical set theory (for formalizing mathematics) and an intuitionistic theory of higher-order abstract syntax (for reasoning about syntax with binders). We have also significantly modified the open source Proofgold Core client software to create a faster, more stable and more efficient client, Proofgold Lava. Two important changes are the cryptography code and the database code, and we discuss these improvements. We also discuss how the Proofgold network can be used to support large formalization efforts.
Cite as

Chad E. Brown, Cezary Kaliszyk, Thibault Gauthier, and Josef Urban. Proofgold: Blockchain for Formal Methods. In 4th International Workshop on Formal Methods for Blockchains (FMBC 2022). Open Access Series in Informatics (OASIcs), Volume 105, pp. 4:1-4:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{brown_et_al:OASIcs.FMBC.2022.4,
  author =	{Brown, Chad E. and Kaliszyk, Cezary and Gauthier, Thibault and Urban, Josef},
  title =	{{Proofgold: Blockchain for Formal Methods}},
  booktitle =	{4th International Workshop on Formal Methods for Blockchains (FMBC 2022)},
  pages =	{4:1--4:15},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-250-1},
  ISSN =	{2190-6807},
  year =	{2022},
  volume =	{105},
  editor =	{Dargaye, Zaynah and Schneidewind, Clara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2022.4},
  URN =		{urn:nbn:de:0030-drops-171851},
  doi =		{10.4230/OASIcs.FMBC.2022.4},
  annote =	{Keywords: Formal logic, Blockchain, Proofgold}
}
  • Refine by Type
  • 52 Document/PDF
  • 11 Document/HTML
  • 1 Volume

  • Refine by Publication Year
  • 1 2026
  • 10 2025
  • 1 2024
  • 1 2023
  • 3 2022
  • Show More...

  • Refine by Author
  • 9 Kaliszyk, Cezary
  • 4 Pąk, Karol
  • 3 Traytel, Dmitriy
  • 3 Urban, Josef
  • 2 Ayala-Rincón, Mauricio
  • Show More...

  • Refine by Series/Journal
  • 51 LIPIcs
  • 1 OASIcs

  • Refine by Classification
  • 15 Theory of computation → Logic and verification
  • 11 Theory of computation → Automated reasoning
  • 9 Theory of computation → Type theory
  • 5 Computing methodologies → Theorem proving algorithms
  • 5 Security and privacy → Logic and verification
  • Show More...

  • Refine by Keyword
  • 8 Coq
  • 5 Isabelle/HOL
  • 4 Formal Verification
  • 3 Mizar
  • 2 Automated Reasoning
  • 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