Search Results

Documents authored by Ivanov, Ievgen


Document
Generalized Newman’s Lemma for Discrete and Continuous Systems

Authors: Ievgen Ivanov

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


Abstract
We propose a generalization of Newman’s lemma which gives a criterion of confluence for a wide class of not-necessarily-terminating abstract rewriting systems. We show that ordinary Newman’s lemma for terminating systems can be considered as a corollary of this criterion. We describe a formalization of the proposed generalized Newman’s lemma in Isabelle proof assistant using HOL logic.

Cite as

Ievgen Ivanov. Generalized Newman’s Lemma for Discrete and Continuous Systems. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 9:1-9:17, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{ivanov:LIPIcs.FSCD.2023.9,
  author =	{Ivanov, Ievgen},
  title =	{{Generalized Newman’s Lemma for Discrete and Continuous Systems}},
  booktitle =	{8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
  pages =	{9:1--9: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.9},
  URN =		{urn:nbn:de:0030-drops-179936},
  doi =		{10.4230/LIPIcs.FSCD.2023.9},
  annote =	{Keywords: abstract rewriting system, confluence, discrete-continuous systems, proof assistant, formal proof}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail