Heuristics for resolution-based set-theoretic proofs

Abstract

A formal specification language like Z permits the specifier to construct proofs which collaborate the aptness of the specification. This process may be facilitated by establishing a partnership between the specifier and a suitable automated reasoner. However, Z specifications are essentially set-theoretic proofs pose demanding challenges to automated reasoners. Taking the OTTER theorem-prover to be representative of resolution-based automated reasoners, we propose a number of heuristics intended to cut down the search space for proofs involving typical set-theoretic structures.