Heuristics for resolution-based set-theoretic proofs

Abstract

A formal specification language like Z permits the specifier to construct proofs which corroborate the aptness of the spec­ification. This process may be facilitated by establishing a partnership between the specifier and a suitable automated reasoner. However, Z specifications are essentially set-theoretic and 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.