2026-07-24T18:10:37Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:23371 2025-10-27T10:17:25Z ddc:004 open_access

Complexity of Cubical Cofibration Logics I: coNP-Complete Examples Rose, Robert Licata, Daniel R. cubical sets internal language intuitionistic logic dependent type theory homotopy type theory decision procedures 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Robert Rose and Daniel R. Licata 2025 Is Part Of LIPIcs, Volume 336, 30th International Conference on Types for Proofs and Programs (TYPES 2024) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.TYPES.2024.9 urn:nbn:de:0030-drops-233711 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2024.9 eng https://creativecommons.org/licenses/by/4.0/legalcode