7 Search Results for "Galmiche, Didier"

Document
DOI: 10.4230/LIPIcs.CSL.2026.16
On the Entailment Problem in Dynamic Separation Logic with Inductive Definitions

Authors: Nicolas Peltier

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

Abstract
Separation Logic (SL) is a well-established framework for reasoning about programs that manipulate dynamic memory. To express and verify properties of custom recursive data structures, SL is extended with spatial predicates defined by user-specified inductive rules. Many verification problems reduce to deciding entailments between formulas involving these predicates. While the general entailment problem is undecidable, a broad class of inductive rules - known as PCE (Progressing, Connected, and Established) - has been identified for which entailment is decidable. In this work, we extend the study of the entailment problem to Dynamic Separation Logic (DSL), an extension of SL that includes dynamic modalities for reasoning about actions on the heap and store. We show that entailment in DSL remains decidable for PCE rules by proving that dynamic modalities can be automatically eliminated.
Cite as

Nicolas Peltier. On the Entailment Problem in Dynamic Separation Logic with Inductive Definitions. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 16:1-16:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{peltier:LIPIcs.CSL.2026.16,
  author =	{Peltier, Nicolas},
  title =	{{On the Entailment Problem in Dynamic Separation Logic with Inductive Definitions}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{16:1--16:20},
  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.16},
  URN =		{urn:nbn:de:0030-drops-254402},
  doi =		{10.4230/LIPIcs.CSL.2026.16},
  annote =	{Keywords: Separation logic, Dynamic logic, Entailment problem}
}
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.CP.2025.15
Symmetric Core Learning for Pseudo-Boolean Optimization by Implicit Hitting Sets

Authors: Hannes Ihalainen, Jeremias Berg, Matti Järvisalo, and Bart Bogaerts

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

Abstract
We propose symmetric core learning (SCL) as a novel approach to making the implicit hitting set approach (IHS) to constraint optimization more symmetry-aware. SCL has the potential of significantly reducing the number of iterations and, in particular, the number of calls to an NP decision solver for extracting individual unsatisfiable cores. As the technique is focused on generating symmetric cores to the hitting set component of IHS, SCL is generally applicable in IHS-style search for essentially any constraint optimization paradigm. In this work, we focus in particular on integrating SCL to IHS for pseudo-Boolean optimization (PBO), as earlier proposed static symmetry breaking through lex-leader constraints generated before search turns out to often degrade the performance of the IHS approach to PBO. In contrast, we show that SCL can improve the runtime performance of a state-of-the-art IHS approach to PBO and generally does not impose significant overhead in terms of runtime performance.
Cite as

Hannes Ihalainen, Jeremias Berg, Matti Järvisalo, and Bart Bogaerts. Symmetric Core Learning for Pseudo-Boolean Optimization by Implicit Hitting Sets. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 15:1-15:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{ihalainen_et_al:LIPIcs.CP.2025.15,
  author =	{Ihalainen, Hannes and Berg, Jeremias and J\"{a}rvisalo, Matti and Bogaerts, Bart},
  title =	{{Symmetric Core Learning for Pseudo-Boolean Optimization by Implicit Hitting Sets}},
  booktitle =	{31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
  pages =	{15:1--15:26},
  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.15},
  URN =		{urn:nbn:de:0030-drops-238767},
  doi =		{10.4230/LIPIcs.CP.2025.15},
  annote =	{Keywords: Implicit hitting sets, symmetries, unsatisfiable cores, pseudo-Boolean optimization}
}
Document
DOI: 10.4230/LIPIcs.SAT.2025.11
Better Extension Variables in DQBF via Independence

Authors: Leroy Chew and Tomáš Peitl

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

Abstract
We show that extension variables in (D)QBF can be generalised by conditioning on universal assignments. The benefit of this is that the dependency sets of such conditioned extension variables can be made smaller to allow easier refutations. This simple modification instantly solves many challenges in p-simulating the QBF expansion rule, which cannot be p-simulated in proof systems that have strategy extraction [Leroy Chew and Judith Clymo, 2020]. Simulating expansion is even more crucial in DQBF, where other methods are incomplete. In this paper we provide an overview of the strength of this new independent extension rule. We find that a new version of Extended Frege called IndExtFrege + ∀red can p-simulate a multitude of difficult QBF and DQBF techniques, even techniques that are difficult to approach with eFrege + ∀red. We show five p-simulations, that IndExtFrege + ∀red p-simulates QRAT, DQBF-IR-calc, IR(𝒟^rrs)-calc, Fork-Resolution and DQRAT which together underpin most DQBF solving and preprocessing techniques. The p-simulations work despite these systems using complicated rules and our new extension rule being relatively simple. Moreover, unlike recent p-simulations by eFrege + ∀red we can simulate the proof rules line by line, which allows us to mix QBF rules more easily with other inference steps.
Cite as

Leroy Chew and Tomáš Peitl. Better Extension Variables in DQBF via Independence. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 11:1-11:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{chew_et_al:LIPIcs.SAT.2025.11,
  author =	{Chew, Leroy and Peitl, Tom\'{a}\v{s}},
  title =	{{Better Extension Variables in DQBF via Independence}},
  booktitle =	{28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
  pages =	{11:1--11:24},
  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.11},
  URN =		{urn:nbn:de:0030-drops-237453},
  doi =		{10.4230/LIPIcs.SAT.2025.11},
  annote =	{Keywords: DQBF, QBF, Proof Systems, Dependency Schemes, RAT, Extended Frege, Skolem functions}
}
Document
DOI: 10.4230/LIPIcs.CSL.2025.42
Unifying Sequent Systems for Gödel-Löb Provability Logic via Syntactic Transformations

Authors: Tim S. Lyon

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

Abstract
We demonstrate the inter-translatability of proofs between the most prominent sequent-based formalisms for Gödel-Löb provability logic. In particular, we consider Sambin and Valentini’s sequent system GL_{seq}, Shamkanov’s non-wellfounded and cyclic sequent systems GL_∞ and GL_{circ}, Poggiolesi’s tree-hypersequent system CSGL, and Negri’s labeled sequent system G3GL. Shamkanov provided proof-theoretic correspondences between GL_{seq}, GL_∞, and GL_{circ}, and Goré and Ramanayake showed how to transform proofs between CSGL and G3GL, however, the exact nature of proof transformations between the former three systems and the latter two systems has remained an open problem. We solve this open problem by showing how to restructure tree-hypersequent proofs into an end-active form and introduce a novel linearization technique that transforms such proofs into linear nested sequent proofs. As a result, we obtain a new proof-theoretic tool for extracting linear nested sequent systems from tree-hypersequent systems, which yields the first cut-free linear nested sequent calculus LNGL for Gödel-Löb provability logic. We show how to transform proofs in LNGL into a certain normal form, where proofs repeat in stages of modal and local rule applications, and which are translatable into GL_{seq} and G3GL proofs. These new syntactic transformations, together with those mentioned above, establish full proof-theoretic correspondences between GL_{seq}, GL_∞, GL_{circ}, CSGL, G3GL, and LNGL while also giving (to the best of the author’s knowledge) the first constructive proof mappings between structural (viz. labeled, tree-hypersequent, and linear nested sequent) systems and a cyclic sequent system.
Cite as

Tim S. Lyon. Unifying Sequent Systems for Gödel-Löb Provability Logic via Syntactic Transformations. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 42:1-42:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{lyon:LIPIcs.CSL.2025.42,
  author =	{Lyon, Tim S.},
  title =	{{Unifying Sequent Systems for G\"{o}del-L\"{o}b Provability Logic via Syntactic Transformations}},
  booktitle =	{33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
  pages =	{42:1--42:23},
  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.42},
  URN =		{urn:nbn:de:0030-drops-227992},
  doi =		{10.4230/LIPIcs.CSL.2025.42},
  annote =	{Keywords: Cyclic proof, G\"{o}del-L\"{o}b logic, Labeled sequent, Linear nested sequent, Modal logic, Non-wellfounded proof, Proof theory, Proof transformation, Tree-hypersequent}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2023.31
Labelled Tableaux for Linear Time Bunched Implication Logic

Authors: Didier Galmiche and Daniel Méry

Published in: LIPIcs, Volume 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)

Abstract
In this paper, we define the logic of Linear Temporal Bunched Implications (LTBI), a temporal extension of the Bunched Implications logic BI that deals with resource evolution over time, by combining the BI separation connectives and the LTL temporal connectives. We first present the syntax and semantics of LTBI and illustrate its expressiveness with a significant example. Then we introduce a tableau calculus with labels and constraints, called TLTBI, and prove its soundness w.r.t. the Kripke-style semantics of LTBI. Finally we discuss and analyze the issues that make the completeness of the calculus not trivial in the general case of unbounded timelines and explain how to solve the issues in the more restricted case of bounded timelines.
Cite as

Didier Galmiche and Daniel Méry. Labelled Tableaux for Linear Time Bunched Implication Logic. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 31:1-31:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{galmiche_et_al:LIPIcs.FSCD.2023.31,
  author =	{Galmiche, Didier and M\'{e}ry, Daniel},
  title =	{{Labelled Tableaux for Linear Time Bunched Implication Logic}},
  booktitle =	{8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
  pages =	{31:1--31:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-277-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{260},
  editor =	{Gaboardi, Marco and van Raamsdonk, Femke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.31},
  URN =		{urn:nbn:de:0030-drops-180159},
  doi =		{10.4230/LIPIcs.FSCD.2023.31},
  annote =	{Keywords: Temporal Logic, Bunched Implication Logic, Labelled Deduction, Tableaux}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2021.13
Beth Semantics and Labelled Deduction for Intuitionistic Sentential Calculus with Identity

Authors: Didier Galmiche, Marta Gawek, and Daniel Méry

Published in: LIPIcs, Volume 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)

Abstract
In this paper we consider the intuitionistic sentential calculus with Suszko’s identity (ISCI). After recalling the basic concepts of the logic and its associated Hilbert proof system, we introduce a new sound and complete class of models for ISCI which can be viewed as algebraic counterparts (and extensions) of sheaf-theoretic topological models of intuitionistic logic. We use this new class of models, called Beth semantics for ISCI, to derive a first labelled sequent calculus and show its adequacy w.r.t. the standard Hilbert axiomatization of ISCI. This labelled proof system, like all other current proof systems for ISCI that we know of, does not enjoy the subformula property, which is problematic for achieving termination. We therefore introduce a second labelled sequent calculus in which the standard rules for identity are replaced with new special rules and show that this second calculus admits cut-elimination. Finally, using a key regularity property of the forcing relation in Beth models, we show that the eigenvariable condition can be dropped, thus leading to the termination and decidability results.
Cite as

Didier Galmiche, Marta Gawek, and Daniel Méry. Beth Semantics and Labelled Deduction for Intuitionistic Sentential Calculus with Identity. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 13:1-13:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{galmiche_et_al:LIPIcs.FSCD.2021.13,
  author =	{Galmiche, Didier and Gawek, Marta and M\'{e}ry, Daniel},
  title =	{{Beth Semantics and Labelled Deduction for Intuitionistic Sentential Calculus with Identity}},
  booktitle =	{6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
  pages =	{13:1--13:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-191-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{195},
  editor =	{Kobayashi, Naoki},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.13},
  URN =		{urn:nbn:de:0030-drops-142516},
  doi =		{10.4230/LIPIcs.FSCD.2021.13},
  annote =	{Keywords: Algebraic Semantics, Beth Models, Labelled Deduction, Intuitionistic Logic}
}
  • Refine by Type
  • 7 Document/PDF
  • 5 Document/HTML

  • Refine by Publication Year
  • 1 2026
  • 4 2025
  • 1 2023
  • 1 2021

  • Refine by Author
  • 2 Galmiche, Didier
  • 2 Méry, Daniel
  • 1 Berg, Jeremias
  • 1 Blanchette, Jasmin
  • 1 Bogaerts, Bart
  • Show More...

  • Refine by Series/Journal
  • 7 LIPIcs

  • Refine by Classification
  • 2 Theory of computation → Automated reasoning
  • 2 Theory of computation → Logic and verification
  • 2 Theory of computation → Proof theory
  • 1 Computing methodologies → Theorem proving algorithms
  • 1 Mathematics of computing → Combinatorial optimization
  • Show More...

  • Refine by Keyword
  • 2 Labelled Deduction
  • 1 Algebraic Semantics
  • 1 Beth Models
  • 1 Bunched Implication Logic
  • 1 Cyclic proof
  • 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