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 2 articles )
Showing results 1 to 2 of 2.
- Horbach, Matthias: Predicate completion for non-Horn clause sets (2011)
- Horbach, Matthias: System description: SPASS-FD (2011)