When working in a proof assistant, automation is key to discharging routine proof goals such as equations between algebraic expressions. Homotopy type theory allows the user to reason about higher structures, such as topological spaces, using higher inductive types (HITs) and univalence. Cubical type theory provides computational support for HITs and univalence. A difficulty when working in cubical type theory is dealing with the complex combinatorics of higher structures, an infinite-dimensional generalisation of equational reasoning. To solve these higher-dimensional equations consists in constructing cubes with specified boundaries. We develop a simplified cubical language in which we isolate and study two automation problems: contortion solving, where we attempt to "contort" a cube to fit a given boundary, and the more general Kan solving, where we search for solutions that involve pasting multiple cubes together. Both problems are difficult in the general case-Kan solving is even undecidable-so we focus on heuristics that perform well on practical examples. Our language encompasses different variations of cubical type theory which differ in their "contortion theory", i.e., the class of contortions they support. We provide a solver for the contortion problem for the most complex contortion theories currently being researched, the Dedekind and De Morgan contortions, by utilizing a reformulation of contortions in terms of poset maps. We solve Kan problems using constraint satisfaction programming, which is applicable independently of the underlying contortion theory. We have implemented our algorithms in an experimental Haskell solver that can be used to automatically solve many goals a user of cubical type theory might face. We illustrate this with a case study establishing the Eckmann-Hilton theorem using our solver, as well as various benchmarks.

翻译：在使用证明助手时，自动化对于完成常规证明目标（如代数表达式之间的等式）至关重要。同伦类型论允许用户通过高阶归纳类型（HITs）和幺半等价性来推理高阶结构（如拓扑空间）。立方类型论为HITs和幺半等价性提供了计算支持。使用立方类型论时的一个难点是处理高阶结构的复杂组合性质，这是等式推理的无限维推广。解决这些高维等式需要构造具有指定边界的立方体。我们开发了一种简化的立方语言，在其中分离并研究了两个自动化问题：扭结求解（试图将立方体“扭结”以匹配给定边界）和更一般的Kan求解（寻找涉及将多个立方体粘合在一起的解）。这两个问题在一般情况下都很困难——Kan求解甚至不可判定——因此我们专注于在实际例子中表现良好的启发式方法。我们的语言涵盖了立方类型论的不同变体，这些变体在“扭结理论”（即它们支持的扭结类别）上有所不同。我们通过将扭结重新表述为偏序集映射，为当前正在研究的最复杂扭结理论（戴德金扭结和德摩根扭结）提供了扭结问题的求解器。我们使用约束满足编程解决Kan问题，该方法独立于底层的扭结理论。我们已在实验性的Haskell求解器中实现了算法，可用于自动解决立方类型论用户可能面临的许多目标。我们通过一个案例研究（使用我们的求解器建立埃克曼-希尔顿定理）以及各种基准测试来展示其效果。