我当时正在为Python编写一个抽象代数库，当我意识到很多繁琐的工作只是构造循环来对应带有量词的逻辑表达式。然后我意识到，虽然在Python中实现逻辑量化的函数可能很难，但在Haskell或其他语言中会更容易。
现在我有了量词，只要属性只涉及一个要被量化的变量，并且只有当你要量化的关系有三个变量时，克服这些障碍似乎是困难的部分。
例如，语句∀x ∃y (x < y)会导致问题，但∀x (x = 2) ∃y (y < 3)没有问题。
是否有任何现有的Haskell库实现这样的值级逻辑量词?它很难搜索，因为每当我沿着"逻辑量词Haskell"搜索时，我都会得到许多关于类型量词的信息，这不是我想要的。
我唯一能找到的是一个forAll在测试。QuickCheck，它没有"存在"。
您可以编写这种表达式并使用SMT求解器生成反例。Haskell对smt求解器有很好的、自然的绑定(例如https://hackage.haskell.org/package/sbv)，它允许您编写普通的表达式，并在这个特殊的规则下对它们求值。