问题给定两个具有a，b和c布尔值的布尔函数f1(a,b)和f2(a,b,c)，我想知道是否存在c的值，从而对于et b f1(a,b)=f2(a,b,c)的任何组合。
例如，如果f1(a,b)=a AND b和f2(a,b,c)=a AND b AND c，当f1=f2时，我们可以参见那个c=1。但是，如果f1(a,b)=a OR b和f2(a,b,c)=a AND b AND c，则f1=f2的c值不成立。
失败的方法
我尝试使用在nuXmv中实现的普通模型进行模型检查，以通过CTL规范（例如EF ( AG ( (a & b) = (a & b & c)))）回答此问题，但失败了。显然，它适用于规范AG ( c=true -> (a & b = a & b & c))，但需要具有2 ^ n规范（n是两个函数之间的变量数之差）。您认为解决此问题的最佳方法/工具/方法是什么。
感谢您指向正确的方向。
问题给定两个布尔函数f1（a，b）和f2（a，b，c）以及a，b和c布尔值，我想知道是否存在c的值，使得对于a的任何组合等b f1（a，b）= f2（a，b，c）对于...