Turning decision procedures into disprovers.

A class of many-sorted polyadic set algebras is introduced. These generalise structure and model in a way that is relevant in regards to the Entscheidungsproblem and to automated reasoning. A downward Löwenheim-Skolem property is shown in that each satisfiable finite conjunction of purely relational first-order prenex sentences has a finite generalised model. This property does, together with a construction related to doubling the size of a finite structure, provide several strict generalisations of the strategy of finite model search for disproving. (© 2009 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim) [ABSTRACT FROM AUTHOR]