Abstract
The equality logic with uninterpreted functions (EUF) has been proposed for processor verification. A procedure for proving satisfiability of formulas in this logic is introduced. Since it is based on the DPLL method, the procedure can adopt its heuristics. Therefore the procedure can be used as a basis for efficient implementations of satisfiability checkers for EUF. A part of the introduced method is a technique for reducing the size of formulas, which can also be used as a preprocessing step in other approaches for checking satisfiability of EUF formulas.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Ackermann, W.: Solvable cases of the decision problem. Studies in Logic and the Foundations of Mathematics. North-Holland, Amsterdam (1954)
Barrett, C.W., Dill, D., Levitt, J.: Validity checking for combinations of theories with equality. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol. 1166, pp. 187–201. Springer, Heidelberg (1996)
Bryant, R., Velev, M.: Boolean satisfiability with transitivity constraints. ACM Transactions on Computational Logic 3(4), 604–627 (2002)
Burch, J., Dill, D.: Automated verification of pipelined microprocesoor control. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 68–80. Springer, Heidelberg (1994)
Davis, M., Logemann, G., Loveland, D.: A machine program for theorem proving. Communications of the Association for Computing Machinery 7, 394–397 (1962)
Goel, A., Sajid, K., Zhou, H., Aziz, A., Singhal, V.: BDD based procedures for a theory of equality with uninterpreted functions. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, pp. 244–255. Springer, Heidelberg (1998)
Groote, J., van de Pol, J.: Equational binary decision diagrams. In: Parigot, M., Voronkov, A. (eds.) LPAR 2000. LNCS (LNAI), vol. 1955, pp. 161–178. Springer, Heidelberg (2000)
Nieuwenhuis, R., Oliveras, A.: Congruence closure with integer offsets. In: Y. Vardi, M., Voronkov, A. (eds.) LPAR 2003. LNCS (LNAI), vol. 2850, pp. 78–90. Springer, Heidelberg (2003)
Pnueli, A., Rodeh, Y., Shtrichman, O., Siegel, M.: Deciding equality formulas by small domains instantiations. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 455–469. Springer, Heidelberg (1999)
Rodeh, Y., Shtrichman, O.: Finite instantiations in equivalence logic with uninterpreted functions. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 144–154. Springer, Heidelberg (2001)
Shostak, R.: An algorithm for reasoning about equality. Communications of the ACM 21 (1978)
Tseitin, G.: On the complexity of derivation in propositional calculus, Consultant Bureau, New York-London. Studies in Constructive Mathematics and Mathematical Logic, Part 2, pp. 115–125 (1968)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Tveretina, O. (2004). A Decision Procedure for Equality Logic with Uninterpreted Functions. In: Buchberger, B., Campbell, J. (eds) Artificial Intelligence and Symbolic Computation. AISC 2004. Lecture Notes in Computer Science(), vol 3249. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30210-0_7
Download citation
DOI: https://doi.org/10.1007/978-3-540-30210-0_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-23212-4
Online ISBN: 978-3-540-30210-0
eBook Packages: Springer Book Archive