6 Search Results for "Ringeissen, Christophe"

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
DOI: 10.4230/LIPIcs.FSCD.2025.18
Knowledge Problems vs Unification and Matching: Dichotomy Results

Authors: Serdar Erbatur, Andrew M. Marshall, Paliath Narendran, and Christophe Ringeissen

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

Abstract
The research area of cryptographic protocol analysis contains a number of innovative algorithms and procedures for checking various security properties of protocols. Most of these procedures focus on solving one of several "knowledge problems" that model intruder knowledge. Solving these problems can demonstrate the ability of the intruder to obtain some forbidden information of the protocol, such as secret keys. Two important examples of these problems are the deduction problem and the static equivalence problem. Deduction is concerned with the ability to derive a term from a set of terms (or knowledge) obtained from the observation of a protocol instance. Static equivalence, on the other hand, is concerned with distinguishing between two runs of a protocol based on two sets of knowledge. These two knowledge problems at first inspection appear to be very close to the older automated reasoning problems of matching and unification. However, this first impression is wrong, and there have been a few results that have shown theories where one problem, such as unification, is undecidable but another problem, such as deduction, is decidable. These existing dichotomy results were, however, incomplete, and not all cases had been examined, thus leaving the possibility of some connection between the problems for those unexamined cases. In this paper, we consider the missing dichotomy cases. For each of the remaining cases, we demonstrate a theory that separates the two problems. In addition, once the dichotomy results are completed, it leaves open the question of the existence of non-trivial classes of theories for which all four of the problems are decidable. One example for which this is true is the well-known class of subterm convergent term rewrite systems. In this paper, we develop another example, a class of restrictive permutative theories for which all problems are likewise decidable.
Cite as

Serdar Erbatur, Andrew M. Marshall, Paliath Narendran, and Christophe Ringeissen. Knowledge Problems vs Unification and Matching: Dichotomy Results. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 18:1-18:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{erbatur_et_al:LIPIcs.FSCD.2025.18,
  author =	{Erbatur, Serdar and Marshall, Andrew M. and Narendran, Paliath and Ringeissen, Christophe},
  title =	{{Knowledge Problems vs Unification and Matching: Dichotomy Results}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{18:1--18:17},
  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.18},
  URN =		{urn:nbn:de:0030-drops-236331},
  doi =		{10.4230/LIPIcs.FSCD.2025.18},
  annote =	{Keywords: Knowledge Problems, Unification, Matching, Decidability}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2023.30
Knowledge Problems in Security Protocols: Going Beyond Subterm Convergent Theories

Authors: Saraid Dwyer Satterfield, Serdar Erbatur, Andrew M. Marshall, and Christophe Ringeissen

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

Abstract
We introduce a new form of restricted term rewrite system, the graph-embedded term rewrite system. These systems, and thus the name, are inspired by the graph minor relation and are more flexible extensions of the well-known homeomorphic-embedded property of term rewrite systems. As a motivating application area, we consider the symbolic analysis of security protocols, and more precisely the two knowledge problems defined by the deduction problem and the static equivalence problem. In this field restricted term rewrite systems, such as subterm convergent ones, have proven useful since the knowledge problems are decidable for such systems. However, many of the same decision procedures still work for examples of systems which are "beyond subterm convergent". However, the applicability of the corresponding decision procedures to these examples must often be proven on an individual basis. This is due to the problem that they don't fit into an existing syntactic definition for which the procedures are known to work. Here we show that many of these systems belong to a particular subclass of graph-embedded convergent systems, called contracting convergent systems. On the one hand, we show that the knowledge problems are decidable for the subclass of contracting convergent systems. On the other hand, we show that the knowledge problems are undecidable for the class of graph-embedded systems.
Cite as

Saraid Dwyer Satterfield, Serdar Erbatur, Andrew M. Marshall, and Christophe Ringeissen. Knowledge Problems in Security Protocols: Going Beyond Subterm Convergent Theories. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 30:1-30:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{dwyersatterfield_et_al:LIPIcs.FSCD.2023.30,
  author =	{Dwyer Satterfield, Saraid and Erbatur, Serdar and Marshall, Andrew M. and Ringeissen, Christophe},
  title =	{{Knowledge Problems in Security Protocols: Going Beyond Subterm Convergent Theories}},
  booktitle =	{8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
  pages =	{30:1--30:19},
  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.30},
  URN =		{urn:nbn:de:0030-drops-180148},
  doi =		{10.4230/LIPIcs.FSCD.2023.30},
  annote =	{Keywords: Term rewriting, security protocols, verification}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2022.6
Combined Hierarchical Matching: the Regular Case

Authors: Serdar Erbatur, Andrew M. Marshall, and Christophe Ringeissen

Published in: LIPIcs, Volume 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)

Abstract
Matching algorithms are often central sub-routines in many areas of automated reasoning. They are used in areas such as functional programming, rule-based programming, automated theorem proving, and the symbolic analysis of security protocols. Matching is related to unification but provides a somewhat simplified problem. Thus, in some cases, we can obtain a matching algorithm even if the unification problem is undecidable. In this paper we consider a hierarchical approach to constructing matching algorithms. The hierarchical method has been successful for developing unification algorithms for theories defined over a constructor sub-theory. We show how the approach can be extended to matching problems which allows for the development, in a modular way, of hierarchical matching algorithms. Here we focus on regular theories, where both sides of each equational axiom have the same set of variables. We show that the combination of two hierarchical matching algorithms leads to a hierarchical matching algorithm for the union of regular theories sharing only a common constructor sub-theory.
Cite as

Serdar Erbatur, Andrew M. Marshall, and Christophe Ringeissen. Combined Hierarchical Matching: the Regular Case. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 6:1-6:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{erbatur_et_al:LIPIcs.FSCD.2022.6,
  author =	{Erbatur, Serdar and Marshall, Andrew M. and Ringeissen, Christophe},
  title =	{{Combined Hierarchical Matching: the Regular Case}},
  booktitle =	{7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
  pages =	{6:1--6:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-233-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{228},
  editor =	{Felty, Amy P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.6},
  URN =		{urn:nbn:de:0030-drops-162879},
  doi =		{10.4230/LIPIcs.FSCD.2022.6},
  annote =	{Keywords: Matching, combination problem, equational theories}
}
Document
DOI: 10.4230/LIPIcs.RTA.2013.303
Automatic Decidability: A Schematic Calculus for Theories with Counting Operators

Authors: Elena Tushkanova, Christophe Ringeissen, Alain Giorgetti, and Olga Kouchnarenko

Published in: LIPIcs, Volume 21, 24th International Conference on Rewriting Techniques and Applications (RTA 2013)

Abstract
Many verification problems can be reduced to a satisfiability problem modulo theories. For building satisfiability procedures the rewriting-based approach uses a general calculus for equational reasoning named paramodulation. Schematic paramodulation, in turn, provides means to reason on the derivations computed by paramodulation. Until now, schematic paramodulation was only studied for standard paramodulation. We present a schematic paramodulation calculus modulo a fragment of arithmetics, namely the theory of Integer Offsets. This new schematic calculus is used to prove the decidability of the satisfiability problem for some theories equipped with counting operators. We illustrate our theoretical contribution on theories representing extensions of classical data structures, e.g., lists and records. An implementation within the rewriting-based Maude system constitutes a practical contribution. It enables automatic decidability proofs for theories of practical use.
Cite as

Elena Tushkanova, Christophe Ringeissen, Alain Giorgetti, and Olga Kouchnarenko. Automatic Decidability: A Schematic Calculus for Theories with Counting Operators. In 24th International Conference on Rewriting Techniques and Applications (RTA 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 21, pp. 303-318, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{tushkanova_et_al:LIPIcs.RTA.2013.303,
  author =	{Tushkanova, Elena and Ringeissen, Christophe and Giorgetti, Alain and Kouchnarenko, Olga},
  title =	{{Automatic Decidability: A Schematic Calculus for Theories with Counting Operators}},
  booktitle =	{24th International Conference on Rewriting Techniques and Applications (RTA 2013)},
  pages =	{303--318},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-53-8},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{21},
  editor =	{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.RTA.2013.303},
  URN =		{urn:nbn:de:0030-drops-40696},
  doi =		{10.4230/LIPIcs.RTA.2013.303},
  annote =	{Keywords: decision procedures, superposition, schematic saturation}
}
  • Refine by Type
  • 6 Document/PDF
  • 3 Document/HTML

  • Refine by Publication Year
  • 3 2025
  • 1 2023
  • 1 2022
  • 1 2013

  • Refine by Author
  • 5 Ringeissen, Christophe
  • 3 Erbatur, Serdar
  • 3 Marshall, Andrew M.
  • 1 Ayala-Rincón, Mauricio
  • 1 Baader, Franz
  • Show More...

  • Refine by Series/Journal
  • 6 LIPIcs

  • Refine by Classification
  • 5 Theory of computation → Equational logic and rewriting
  • 3 Theory of computation → Automated reasoning
  • 1 Computing methodologies → Symbolic and algebraic manipulation
  • 1 Theory of computation → Description logics

  • Refine by Keyword
  • 2 Equational theories
  • 2 Matching
  • 1 Anti-unification
  • 1 Combination
  • 1 Decidability
  • 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