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.
@InProceedings{rose_et_al:LIPIcs.TYPES.2024.9, author = {Rose, Robert and Licata, Daniel R.}, title = {{Complexity of Cubical Cofibration Logics I: coNP-Complete Examples}}, booktitle = {30th International Conference on Types for Proofs and Programs (TYPES 2024)}, pages = {9:1--9:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-376-8}, ISSN = {1868-8969}, year = {2025}, volume = {336}, editor = {M{\o}gelberg, Rasmus Ejlers and van den Berg, Benno}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2024.9}, URN = {urn:nbn:de:0030-drops-233711}, doi = {10.4230/LIPIcs.TYPES.2024.9}, annote = {Keywords: cubical sets, internal language, intuitionistic logic, dependent type theory, homotopy type theory, decision procedures} }
Feedback for Dagstuhl Publishing