To Ackermann-ize or Not to Ackermann-ize? On Efficiently Handling Uninterpreted Function Symbols in ::::SMT::::(::::EUF:::: È::::T::::)

Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Alessandro Santuari, Roberto Sebastiani. To Ackermann-ize or Not to Ackermann-ize? On Efficiently Handling Uninterpreted Function Symbols in ::::SMT::::(::::EUF:::: È::::T::::). In Miki Hermann, Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning, 13th International Conference, LPAR 2006, Phnom Penh, Cambodia, November 13-17, 2006, Proceedings. Volume 4246 of Lecture Notes in Computer Science, pages 557-571, Springer, 2006. [doi]

Abstract

Abstract is missing.