构造性和综合性的可约性理论:Myhill的同构定理和Coq中多表和真值表可约性的Post问题 这是论文“一种构造性和综合性的可约性理论:Myhill的同构定理和Coq中多表和真值表可约性的Post问题”的Coq机械化。 如何编译代码 您需要安装The Coq Proof Assistant, version 8.12 , , 软件包和软件包。 之后,您可以输入make 。 如何安装Coq 安装Coq和所需库的最简单方法是通过opam (版本2 )。 opam switch create coq-reducibility 4.07.1+flambda eval $(opam env) opam repo add coq-released https://coq.inria.fr/opam/released opam install coq.8.12.1 coq-equations.1.