2013 | OriginalPaper | Buchkapitel
Superposition for Bounded Domains
verfasst von : Thomas Hillenbrand, Christoph Weidenbach
Erschienen in: Automated Reasoning and Mathematics
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
Reasoning about bounded domains in resolution calculi is often painful. For explicit and small domains and formulas with a few variables, grounding can be a successful approach. This approach was in particular shown to be effective by Bill McCune. For larger domains or larger formula sets with many variables, there is not much known. In particular, despite general decidability, superposition implementations that can meanwhile deal with large formula sets typically will not necessarily terminate. We start from the observation that lifting can be done more economically here: A variable does not stand anymore for every ground term, but just for the finitely many domain representatives. Thanks to this observation, the inference rules of superposition can drastically be restricted, and redundancy becomes effective. We present one calculus configuration which constitutes a decision procedure for satisfiability modulo the cardinality bound, and hence decides the Bernays-Schönfinkel class as a simple consequence. Finally, our approach also applies to bounded sorts in combination with arbitrary other, potentially infinite sorts in the framework of soft sorts. This frequent combination – which we recently explored in a combination of
Spass
and Isabelle – is an important motivation of our study.