System description: SPASS-FD. Using a constrained superposition calculus and a disunification procedure, it is possible to employ superposition-based first-order reasoners for reasoning not only about all models of a first-order theory, but also about all models over a specific finite domain and often as well about the perfect models of the theory (or the unique minimal model in case of a Horn theory). Both of these problems are second-order problems.par In this paper, I describe the tool Spass-FD, an extension of the first-order prover Spass that equips Spass with disunification as well as with fixed domain and minimal model theorem proving capabilities.
References in zbMATH (referenced in 1 article )
Showing result 1 of 1.