65 Search Results for "Kutsia, Temur"

Volume

LIPIcs, Volume 309

15th International Conference on Interactive Theorem Proving (ITP 2024)

ITP 2024, September 9-14, 2024, Tbilisi, Georgia

Editors: Yves Bertot, Temur Kutsia, and Michael Norrish

Document
DOI: 10.4230/LIPIcs.ITP.2025.8
Abstract, Compositional Consistency: Isabelle/HOL Locales for Completeness à la Fitting

Authors: Asta Halkjær From and Anders Schlichtkrull

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

Abstract
Smullyan and Fitting have used abstract consistency properties to great effect in unifying meta-theoretical results in logic. In this paper, we generalize these developments with the help of Isabelle/HOL. We use locales to decompose abstract consistency into general parts, and provide the textbook variants as special cases. Users can assemble their own consistency property for a given logic. The compositionality alleviates the absence of dependent types in Isabelle/HOL. We use our development to mechanize completeness of calculi for three logics: (1) first-order logic where we only instantiate universal quantifiers with already occurring terms, (2) second-order logic over general models, and (3) a recently developed strong hybrid logic with propositional quantification.
Cite as

Asta Halkjær From and Anders Schlichtkrull. Abstract, Compositional Consistency: Isabelle/HOL Locales for Completeness à la Fitting. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 8:1-8:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{from_et_al:LIPIcs.ITP.2025.8,
  author =	{From, Asta Halkj{\ae}r and Schlichtkrull, Anders},
  title =	{{Abstract, Compositional Consistency: Isabelle/HOL Locales for Completeness \`{a} la Fitting}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{8:1--8: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.8},
  URN =		{urn:nbn:de:0030-drops-246406},
  doi =		{10.4230/LIPIcs.ITP.2025.8},
  annote =	{Keywords: Logic, completeness, abstract consistency property, Isabelle/HOL, locales}
}
Document
DOI: 10.4230/LIPIcs.ITP.2025.24
Formally Verifying a Vertical Cell Decomposition Algorithm

Authors: Yves Bertot and Thomas Portet

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

Abstract
The broad context of this work is the application of formal methods to geometry and robotics. We describe an algorithm to decompose a working area containing obstacles into a collection of safe cells and the formal proof that this algorithm is correct. We expect such an algorithm will be useful to compute safe trajectories. To our knowledge, this is one of the first formalization of such an algorithm to decompose a working space into elementary cells that are suitable for later applications, with the proof of correctness that guarantees that large parts of the working space are safe. Techniques to perform this proof go from algebraic reasoning on coordinates and determinants to sorting. The main difficulty comes from the possible existence of degenerate cases, which are treated in a principled way.
Cite as

Yves Bertot and Thomas Portet. Formally Verifying a Vertical Cell Decomposition Algorithm. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 24:1-24:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bertot_et_al:LIPIcs.ITP.2025.24,
  author =	{Bertot, Yves and Portet, Thomas},
  title =	{{Formally Verifying a Vertical Cell Decomposition Algorithm}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{24:1--24:18},
  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.24},
  URN =		{urn:nbn:de:0030-drops-246222},
  doi =		{10.4230/LIPIcs.ITP.2025.24},
  annote =	{Keywords: Formal Verification, Motion planning, algorithmic geometry}
}
Document
DOI: 10.4230/LIPIcs.ITP.2025.18
Formalising New Mathematics in Isabelle: Diagonal Ramsey

Authors: Lawrence C. Paulson

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

Abstract
The formalisation of mathematics is becoming routine, but its value to research mathematicians remains unproven. There are few examples of using proof assistants to verify new work. This paper reports the formalisation - inspired by a Lean one by Bhavik Mehta - of a major new result [Marcelo Campos et al., 2023] about Ramsey numbers. One unexpected finding was a heavy role for computer algebra techniques.
Cite as

Lawrence C. Paulson. Formalising New Mathematics in Isabelle: Diagonal Ramsey. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 18:1-18:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{paulson:LIPIcs.ITP.2025.18,
  author =	{Paulson, Lawrence C.},
  title =	{{Formalising New Mathematics in Isabelle: Diagonal Ramsey}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{18:1--18:18},
  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.18},
  URN =		{urn:nbn:de:0030-drops-246163},
  doi =		{10.4230/LIPIcs.ITP.2025.18},
  annote =	{Keywords: Isabelle, formalisation of mathematics, Ramsey’s theorem, computer algebra}
}
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.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.CONCUR.2025.10
Abstract Subtyping for Asynchronous Multiparty Sessions

Authors: Laura Bocchi, Andy King, Maurizio Murgia, and Simon Thompson

Published in: LIPIcs, Volume 348, 36th International Conference on Concurrency Theory (CONCUR 2025)

Abstract
Session subtyping answers the question of whether a program in a communicating system can be safely substituted for another, when their communication behaviour is described by session types. Asynchronous session subtyping is undecidable, even for two participants, hence the interest in sound, but incomplete, subtyping algorithms. Asynchronous multiparty subtyping can be formulated by decomposing session types into single input and output types which preclude, respectively, external and internal choice. This paper shows how abstract interpretation can sit atop this approach and how it leads to an algorithm that can prove subtyping for intricate communication patterns.
Cite as

Laura Bocchi, Andy King, Maurizio Murgia, and Simon Thompson. Abstract Subtyping for Asynchronous Multiparty Sessions. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 10:1-10:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bocchi_et_al:LIPIcs.CONCUR.2025.10,
  author =	{Bocchi, Laura and King, Andy and Murgia, Maurizio and Thompson, Simon},
  title =	{{Abstract Subtyping for Asynchronous Multiparty Sessions}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{10:1--10:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-389-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{348},
  editor =	{Bouyer, Patricia and van de Pol, Jaco},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.10},
  URN =		{urn:nbn:de:0030-drops-239605},
  doi =		{10.4230/LIPIcs.CONCUR.2025.10},
  annote =	{Keywords: asynchrony, session subtyping, automata, abstract interpretation}
}
Document
DOI: 10.4230/LIPIcs.CP.2025.8
Breaking Symmetries with Involutions

Authors: Michael Codish and Mikoláš Janota

Published in: LIPIcs, Volume 340, 31st International Conference on Principles and Practice of Constraint Programming (CP 2025)

Abstract
Symmetry breaking for graphs and other combinatorial objects is notoriously hard. On the one hand, complete symmetry breaks are exponential in size. On the other hand, current, state-of-the-art, partial symmetry breaks are often considered too weak to be of practical use. Recently, the concept of graph patterns has been introduced and provides a concise representation for (large) sets of non-canonical graphs, i.e. graphs that are not lex-leaders and can be excluded from search. In particular, four (specific) graph patterns apply to identify about 3/4 of the set of all non-canonical graphs. Taking this approach further, we discover that graph patterns that derive from permutations that are involutions play an important role in the construction of symmetry breaks for graphs. We take advantage of this to guide the construction of partial and complete symmetry-breaking constraints based on graph patterns. The resulting constraints are small in size and strong in the number of symmetries they break.
Cite as

Michael Codish and Mikoláš Janota. Breaking Symmetries with Involutions. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 8:1-8:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{codish_et_al:LIPIcs.CP.2025.8,
  author =	{Codish, Michael and Janota, Mikol\'{a}\v{s}},
  title =	{{Breaking Symmetries with Involutions}},
  booktitle =	{31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
  pages =	{8:1--8:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-380-5},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{340},
  editor =	{de la Banda, Maria Garcia},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.8},
  URN =		{urn:nbn:de:0030-drops-238699},
  doi =		{10.4230/LIPIcs.CP.2025.8},
  annote =	{Keywords: graph symmetry, patterns, permutation, Ramsey graphs, greedy, CEGAR}
}
Document
DOI: 10.4230/LIPIcs.SAT.2025.15
RustSAT: A Library for SAT Solving in Rust

Authors: Christoph Jabs

Published in: LIPIcs, Volume 341, 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)

Abstract
State-of-the-art Boolean satisfiability (SAT) solvers constitute a practical and competitive approach for solving various real-world problems. To encourage their widespread adoption, the relatively high barrier of entry following from the low level syntax of SAT and the expert knowledge required to achieve tight integration with SAT solvers should be further reduced. We present RustSAT, a library with the aim of making SAT solving technology readily available in the Rust programming language. RustSAT provides functionality for helping with generating (Max)SAT instances, writing them to, or reading them from files. Furthermore, RustSAT includes interfaces to various state-of-the-art SAT solvers available with a unified Rust API. Lastly, RustSAT implements several encodings for higher level constraints (at-most-one, cardinality, and pseudo-Boolean), which are also available via a C and Python API.
Cite as

Christoph Jabs. RustSAT: A Library for SAT Solving in Rust. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 15:1-15:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{jabs:LIPIcs.SAT.2025.15,
  author =	{Jabs, Christoph},
  title =	{{RustSAT: A Library for SAT Solving in Rust}},
  booktitle =	{28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
  pages =	{15:1--15:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-381-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{341},
  editor =	{Berg, Jeremias and Nordstr\"{o}m, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.15},
  URN =		{urn:nbn:de:0030-drops-237498},
  doi =		{10.4230/LIPIcs.SAT.2025.15},
  annote =	{Keywords: Rust, library, SAT solvers, constraint encodings}
}
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.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
Complete Volume
DOI: 10.4230/LIPIcs.ITP.2024
LIPIcs, Volume 309, ITP 2024, Complete Volume

Authors: Yves Bertot, Temur Kutsia, and Michael Norrish

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

Abstract
LIPIcs, Volume 309, ITP 2024, Complete Volume
Cite as

15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 1-714, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@Proceedings{bertot_et_al:LIPIcs.ITP.2024,
  title =	{{LIPIcs, Volume 309, ITP 2024, Complete Volume}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{1--714},
  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},
  URN =		{urn:nbn:de:0030-drops-207277},
  doi =		{10.4230/LIPIcs.ITP.2024},
  annote =	{Keywords: LIPIcs, Volume 309, ITP 2024, Complete Volume}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.ITP.2024.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Yves Bertot, Temur Kutsia, and Michael Norrish

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

Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as

15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 0:i-0:xii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{bertot_et_al:LIPIcs.ITP.2024.0,
  author =	{Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{0:i--0:xii},
  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.0},
  URN =		{urn:nbn:de:0030-drops-207287},
  doi =		{10.4230/LIPIcs.ITP.2024.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.ITP.2024.1
Alpha-Beta Pruning Verified (Invited Talk)

Authors: Tobias Nipkow

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

Abstract
Alpha-beta pruning is an efficient search strategy for two-player game trees. It was invented in the late 1950s and is at the heart of most implementations of combinatorial game playing programs. We have formalized and verified a number of variations of alpha-beta pruning, in particular fail-hard and fail-soft, and valuations into linear orders, distributive lattices and domains with negative values.
Cite as

Tobias Nipkow. Alpha-Beta Pruning Verified (Invited Talk). In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 1:1-1:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{nipkow:LIPIcs.ITP.2024.1,
  author =	{Nipkow, Tobias},
  title =	{{Alpha-Beta Pruning Verified}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{1:1--1:4},
  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.1},
  URN =		{urn:nbn:de:0030-drops-207294},
  doi =		{10.4230/LIPIcs.ITP.2024.1},
  annote =	{Keywords: Verification, Algorithmic Game Theory, Isabelle}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.ITP.2024.2
Translating Libraries of Definitions and Theorems Between Proof Systems (Invited Talk)

Authors: Frédéric Blanqui

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

Abstract
There exist many proof systems, interactive or automated. However, most of them are not interoperable, which leads to an important work duplication. This is unfortunate as it slows down the formalization of more advanced mathematical results, and the democratization of proof systems in education, industry and research. This state of affairs is not just a matter of file formats. Each proof system has its own axioms and deduction rules, and those axioms and deduction rules can sometimes be incompatible. To translate a proof from one system to the other, and be able to handle so many different systems, it is important to find out a logical framework in which a logical feature used in two different systems is represented by the same construction. Research on proof system interoperability started about 30 years ago, and received some increased attention with the formalization of Hales proof of Kepler conjecture in the years 2000, because parts of this proof were initially formalized in different systems. Then, it received some new interest in the years 2010 with the increasing use of automated theorem provers in proof assistants. At about the same time appeared a new logical framework, Dedukti, which extends Edinburgh’s logical framework LF by allowing the identification of types modulo some equational theory. It has been shown that various proof systems can be nicely encoded in Dedukti, and various tools have been developed to actually represent the proofs of those systems and translate them to other systems. In this talk, I will review some of these works and tools, and present recent efforts to translate entire libraries of definitions and theorems.
Cite as

Frédéric Blanqui. Translating Libraries of Definitions and Theorems Between Proof Systems (Invited Talk). In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, p. 2:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{blanqui:LIPIcs.ITP.2024.2,
  author =	{Blanqui, Fr\'{e}d\'{e}ric},
  title =	{{Translating Libraries of Definitions and Theorems Between Proof Systems}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{2:1--2:1},
  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.2},
  URN =		{urn:nbn:de:0030-drops-207307},
  doi =		{10.4230/LIPIcs.ITP.2024.2},
  annote =	{Keywords: Logical frameworks, proof systems interoperability, type theory}
}
  • Refine by Type
  • 64 Document/PDF
  • 10 Document/HTML
  • 1 Volume

  • Refine by Publication Year
  • 10 2025
  • 44 2024
  • 2 2020
  • 1 2019
  • 2 2018
  • Show More...

  • Refine by Author
  • 14 Kutsia, Temur
  • 4 Cerna, David M.
  • 4 Levy, Jordi
  • 4 Villaret, Mateu
  • 3 Affeldt, Reynald
  • Show More...

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

  • Refine by Classification
  • 23 Theory of computation → Logic and verification
  • 13 Theory of computation → Type theory
  • 8 Theory of computation → Higher order logic
  • 7 Theory of computation → Automated reasoning
  • 6 Theory of computation → Interactive proof systems
  • Show More...

  • Refine by Keyword
  • 6 Coq
  • 5 Isabelle/HOL
  • 4 Isabelle
  • 4 Lean
  • 3 Anti-unification
  • 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