We present an approach to bring reasoning in quantales into the realm of
automated theorem proving. We use the TPTP Problem Library for this purpose
which by a recent approach now integrates fully automated higher-order
theorem provers.
In particular, we give an encoding of quantales in the new typed
higher-order
form and show how to prove theorems about quantales fully automatically.
We have done more proof experiments, including idempotent
semirings, Kleene algebras, omega algebras and demonic refinement
algebras. The files concerning these experiments can be found in a
proof
database.