我在用着 SBV （用Z3后端）在Haskell中创建一些理论证明。我想检查是否forall x 和 y 给定约束（如 x + y = y + x，哪里 + 是一个“加号运算符”，而不是加法）其他一些条款是有效的。我想定义关于的公理 + 表达式（如关联性，身份等），然后检查进一步的等式，如检查是否 a + (b + c) == (a + c) + b 是正式的 a， b 和 c。
我试图通过以下方式实现它：
main = do
let x = forall "x"
let y = forall "y"
out <- prove $ (x .== x)
print "end"
但似乎我们无法使用 .== 运算符符号值。这是缺少的功能还是错误的用法？我们能够以某种方式使用SBV吗？
通过使用未经解释的排序和功能，这种推理确实是可能的。然而，需要注意的是，对这种结构的推理通常需要量化的公理，而SMT求解器通常不能很好地用量词推理。
话虽如此，这就是我将如何使用SBV。
首先，一些样板代码来获得未解释的类型 T：
{-# LANGUAGE DeriveDataTypeable #-}
import Data.Generics
import Data.SBV
-- Uninterpreted type T
data T = TBase () deriving (Eq, Ord, Data, Typeable, Read, Show)
instance SymWord T
instance HasKind T
type ST = SBV T
完成此操作后，您将可以访问未解释的类型 T 和它的象征性对应物 ST。我们来宣布 plus 和 zero，再次只是具有正确类型的未解释的常量：
-- Uninterpreted addition
plus :: ST -> ST -> ST
plus = uninterpret "plus"
-- Uninterpreted zero
zero :: ST
zero = uninterpret "zero"
到目前为止，我们告诉SBV的是，存在一种类型 T和一个功能 plus和一个常数 zero;显然没有被解释。也就是说，除了具有给定类型的事实之外，SMT求解器不做任何假设。
让我们首先尝试证明这一点 0+x = x：
bad = prove $ \x -> zero `plus` x .== x
如果你试试这个，你会得到以下回复：
*Main> bad
Falsifiable. Counter-example:
s0 = T!val!0 :: T
SMT求解器告诉你的是该属性不成立，这是一个不成立的值。价值 T!val!0 是一个 Z3 具体反应;其他求解者可以返回其他东西。它本质上是该类型居民的内部标识符 T;除此之外我们对此一无所知。当然，这并不是非常有用，因为你真的不知道它为它做了什么关联 plus 和 zero，但这是可以预料的。
为了证明这个属性，让我们再告诉SMT求解器两件事。首先，那 plus 是可交换的。第二，那 zero 添加在右边没有做任何事情。这些是通过 addAxiom 调用。不幸的是，你必须用SMTLib语法编写公理，因为SBV（至少尚未）支持使用Haskell编写的公理。另请注意，我们切换到使用 Symbolic monad在这里：
good = prove $ do
addAxiom "plus-zero-axioms"
[ "(assert (forall ((x T) (y T)) (= (plus x y) (plus y x))))"
, "(assert (forall ((x T)) (= (plus x zero) x)))"
]
x <- free "x"
return $ zero `plus` x .== x
注意我们如何告诉解算器 x+y = y+x 和 x+0 = x，并要求它证明 0+x = x。以这种方式编写公理看起来非常难看，因为你必须使用SMTLib语法，但那是当前的事态。现在我们有：
*Main> good
Q.E.D.
量化的公理和未解释的类型/函数不是通过SBV接口使用的最简单的东西，但是你可以通过这种方式获得一些里程数。如果你在公理中大量使用量词，求解器就不太可能回答你的问题;并可能会作出回应 unknown。这一切都取决于你使用的求解器，以及要证明的属性有多难。
您对API的使用并不完全正确。证明数学等式的最简单方法是使用简单的函数。例如，关于无界整数的关联性可以这样表达：
prove $ \x y z -> x + (y + z) .== (x + y) + (z :: SInteger)
如果你需要一个更具编程性的界面（有时你会），那么你可以使用 Symbolic monad，因此：
plusAssoc = prove $ do x <- sInteger "x"
y <- sInteger "y"
z <- sInteger "z"
return $ x + (y + z) .== (x + y) + z
我建议浏览hackage站点中提供的许多示例以熟悉API： https://hackage.haskell.org/package/sbv