In this paper we report on our first experiences using the relational analysis provided by the Alloy tool with the theorem prover KIV in the context of specifications of freely generated data types. The presented approach aims at improving KIV's performance on first-order theories. In theorem proving practice a significant amount of time is spent on unsuccessful proof attempts. An automatic method that exhibits counter examples for unprovable theorems would offer an extremely valuable support for a proof engineer by saving his time and effort. In practice, such counterexamples tend to be small, so usually there is no need to search for big instances. The paper defines a translation from KIV's recursive definitions to Alloy, discusses its correctness and gives some examples. © 2008 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
Dunets, A., Schellhorn, G., & Reif, W. (2008). Bounded relational analysis of free data types. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4966 LNCS, pp. 99–115). https://doi.org/10.1007/978-3-540-79124-9_8
Mendeley helps you to discover research relevant for your work.