Automated Higher-order Reasoning in Quantales

erschienen 2009 in R. Berghammer, A. M. Jaoua, B. Möller (eds.): Relations and Kleene algebra in computer science. PhD Programme (RelMiCS 11/AKA 6)
Technical Report, Computer Science and Engineering Department, University of Qatar, 2009, pp.38-42.

Abstract:
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.

Downloads:

• QA-09-11  -  (QA-09-11.pdf, 0 KB)