Search Results

Documents authored by Donato, Pablo

Artifact
Software
DOI: 10.4230/artifacts.22486
flowers-metatheory

Authors: Pablo Donato

Abstract
Cite as

Pablo Donato. flowers-metatheory (Software, Mechanized Theory). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-22486,
   title = {{flowers-metatheory}}, 
   author = {Donato, Pablo},
   note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:290076a847ca95e93c17fb66659086d7f68be014;origin=https://github.com/Champitoad/flowers-metatheory;visit=swh:1:snp:4e8e9db020ad62996ea53e2f7aa11a1293700d6c;anchor=swh:1:rev:9fad86b89037ce4aca7ffefc9a964a39ee3e473d}{\texttt{swh:1:dir:290076a847ca95e93c17fb66659086d7f68be014}} (visited on 2024-11-28)},
   url = {https://github.com/Champitoad/flowers-metatheory},
   doi = {10.4230/artifacts.22486},
}
Document
DOI: 10.4230/LIPIcs.FSCD.2024.5
The Flower Calculus

Authors: Pablo Donato

Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)

Abstract
We introduce the flower calculus, a deep inference proof system for intuitionistic first-order logic inspired by Peirce’s existential graphs. It works as a rewriting system over inductive objects called "flowers", that enjoy both a graphical interpretation as topological diagrams, and a textual presentation as nested sequents akin to coherent formulas. Importantly, the calculus dispenses completely with the traditional notion of symbolic connective, operating solely on nested flowers containing atomic predicates. We prove both the soundness of the full calculus and the completeness of an analytic fragment with respect to Kripke semantics. This provides to our knowledge the first analyticity result for a proof system based on existential graphs, adapting semantic cut-elimination techniques to a deep inference setting. Furthermore, the kernel of rules targetted by completeness is fully invertible, a desirable property for both automated and interactive proof search.
Cite as

Pablo Donato. The Flower Calculus. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 5:1-5:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{donato:LIPIcs.FSCD.2024.5,
  author =	{Donato, Pablo},
  title =	{{The Flower Calculus}},
  booktitle =	{9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
  pages =	{5:1--5:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-323-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{299},
  editor =	{Rehof, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.5},
  URN =		{urn:nbn:de:0030-drops-203343},
  doi =		{10.4230/LIPIcs.FSCD.2024.5},
  annote =	{Keywords: deep inference, graphical calculi, existential graphs, intuitionistic logic, Kripke semantics, cut-elimination}
}
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
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact