Document Open Access Logo

Complexity of Cubical Cofibration Logics I: coNP-Complete Examples

Authors Robert Rose , Daniel R. Licata

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.TYPES.2024.9.pdf
  • Filesize: 0.75 MB
  • 21 pages
HTML5 Logo HTML (experimental)
LIPIcs.TYPES.2024.9.html

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
Keywords
  • cubical sets
  • internal language
  • intuitionistic logic
  • dependent type theory
  • homotopy type theory
  • decision procedures

Metrics

Abstract

We provide a comprehensive classification of the cofibration entailment problem, COFENT, for the cofibration logics of various cubical type theories in use today. The problem COFENT arose from the need of cubical proof assistants to automate reasoning about cubical complexes included in an n-dimensional hypercube. Intuitively, it asks: given logical descriptions of two such complexes, is one a subcomplex of the other? We show that the common variants of COFENT are coNP-complete.

Cite As Get BibTex

Robert Rose and Daniel R. Licata. Complexity of Cubical Cofibration Logics I: coNP-Complete Examples. In 30th International Conference on Types for Proofs and Programs (TYPES 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 336, pp. 9:1-9:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.TYPES.2024.9

Author Details

Robert Rose
  • Dept. of Mathematics & Computer Science, Wesleyan University, Middletown, CT, USA
Daniel R. Licata
  • Dept. of Mathematics & Computer Science, Wesleyan University, Middletown, CT, USA

Funding

This material is based upon work supported by the Air Force Office of Scientific Research under Grant No.FA9550-21-0009 (Tristan Nguyen, program manager). Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author and do not necessarily reflect the views of the Air Force Office of Scientific Research.
  • Rose, Robert: US Air Force Research Lab, FA-95502110009 and FA-95501510053
  • Licata, Daniel R.: US Air Force Research Lab, FA-95502110009 and FA-95501510053

References

  1. Carlo Angiuli, Guillaume Brunerie, Thierry Coquand, Robert Harper, Kuen-Bang Hou (Favonia), and Daniel R. Licata. Syntax and models of cartesian cubical type theory. Mathematical Structures in Computer Science, 31(4):424-468, 2021. URL: https://doi.org/10.1017/S0960129521000347.
  2. Ulrik Buchholtz and Edward Morehouse. Varieties of cubical sets. Lecture Notes in Computer Science, pages 77-92, 2017. URL: https://doi.org/10.1007/978-3-319-57418-9_5.
  3. Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. Cubical type theory: a constructive interpretation of the univalence axiom, 2016. URL: https://arxiv.org/abs/1611.02108.
  4. Leonid Libkin. Elements of Finite Model Theory. Springer Publishing Company, Incorporated, 1st edition, 2010. Google Scholar
  5. Saunders Mac Lane and Ieke Moerdijk. Sheaves in Geometry and Logic: A First Introduction to Topos Theory. Springer New York, New York, NY, 1994. Google Scholar
  6. Emily Riehl and Michael Shulman. A type theory for synthetic ∞-categories, 2017. URL: https://arxiv.org/abs/1705.07442.
  7. Matthew Z. Weaver and Daniel R. Licata. A constructive model of directed univalence in bicubical sets. In Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '20, pages 915-928, New York, NY, USA, 2020. Association for Computing Machinery. URL: https://doi.org/10.1145/3373718.3394794.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact