2007 | OriginalPaper | Buchkapitel
Constraints for Argument Filterings
verfasst von : Harald Zankl, Nao Hirokawa, Aart Middeldorp
Erschienen in: SOFSEM 2007: Theory and Practice of Computer Science
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
The dependency pair method is a powerful method for automatically proving termination of rewrite systems. When used with traditional simplification orders like LPO and KBO, argument filterings play a key role. In this paper we propose an encoding of argument filterings in propositional logic. By incorporating propositional encodings of simplification orders, the search for suitable argument filterings is turned into a satisfiability problem. Preliminary experimental results show that our logic-based approach is significantly faster than existing implementations.