Anzeige
Erschienen in:
2011 | OriginalPaper | Buchkapitel
System Description: SPASS-FD
verfasst von : Matthias Horbach
Erschienen in: Automated Deduction – CADE-23
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.
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.