Abstract
This paper describes feature vector indexing, a new, non-perfect indexing method for clause subsumption. It is suitable for both forward (i.e., finding a subsuming clause in a set) and backward (finding all subsumed clauses in a set) subsumption. Moreover, it is easy to implement, but still yields excellent performance in practice. As an added benefit, by restricting the selection of features used in the index, our technique immediately adapts to indexing modulo arbitrary AC theories with only minor loss of efficiency. Alternatively, the feature selection can be restricted to result in set subsumption. Feature vector indexing has been implemented in our equational theorem prover E, and has enabled us to integrate new simplification techniques making heavy use of subsumption. We experimentally compare the performance of the prover for a number of strategies using feature vector indexing and conventional sequential subsumption.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
de Moura, L., Bjørner, N.S.: Engineering DPLL(T) + Saturation. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 475–490. Springer, Heidelberg (2008)
Denzinger, J., Kronenburg, M., Schulz, S.: DISCOUNT: A Distributed and Learning Equational Prover. Journal of Automated Reasoning 18(2), 189–198 (1997); Special Issue on the CADE 13 ATP System Competition
Graf, P.: Term Indexing. LNCS, vol. 1053. Springer, Heidelberg (1996)
Graf, P., Fehrer, D.: Term Indexing. In: Bibel, W., Schmitt, P.H. (eds.) Automated Deduction — A Basis for Applications. Applied Logic Series, vol. 9(2), ch. 5, pp. 125–147. Kluwer Academic Publishers (1998)
Jaynes, E.T.: Probability Theory: The Logic of Science. Cambridge University Press (2003)
Kapur, D., Narendran, P.: NP-Completeness of the Set Unification and Matching Problems. In: Siekmann, J.H. (ed.) CADE 1986. LNCS, vol. 230, pp. 489–495. Springer, Heidelberg (1986)
Korovin, K.: iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 292–298. Springer, Heidelberg (2008)
Löchner, B., Hillenbrand, T.: A Phytography of Waldmeister. Journal of AI Communications 15(2/3), 127–133 (2002)
McCune, W.W.: EQP 0.9 Users’ Guide (1999), http://www.cs.unm.edu/~mccune/eqp/Manual.txt (accessed December 11, 2012)
McCune, W.W.: Experiments with Discrimination-Tree Indexing and Path Indexing for Term Retrieval. Journal of Automated Reasoning 9(2), 147–167 (1992)
McCune, W.W.: 33 Basic Test Problems: A Practical Evaluation of Some Paramodulation Strategies. In: Veroff, R. (ed.) Automated Reasoning and its Applications: Essays in Honor of Larry Wos, ch. 5, pp. 71–114. MIT Press (1997)
Motik, B., Sattler, U.: A Comparison of Reasoning Techniques for Querying Large Description Logic ABoxes. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol. 4246, pp. 227–241. Springer, Heidelberg (2006)
University of Miami Center for Computational Science. Pegasus - Introduction (2007-2011), http://ccs.miami.edu/?page_id=3749 (accessed December 09, 2012)
Riazanov, A., Voronkov, A.: The Design and Implementation of VAMPIRE. Journal of AI Communications 15(2/3), 91–110 (2002)
Riazanov, A., Voronkov, A.: Efficient Instance Retrieval with Standard and Relational Path Indexing. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol. 2741, pp. 380–396. Springer, Heidelberg (2003)
Schulz, S.: Information-Based Selection of Abstraction Levels. In: Russel, I., Kolen, J. (eds.) Proc. of the 14th FLAIRS, Key West, pp. 402–406. AAAI Press (2001)
Schulz, S.: E – A Brainiac Theorem Prover. Journal of AI Communications 15(2/3), 111–126 (2002)
Schulz, S.: Simple and Efficient Clause Subsumption with Feature Vector Indexing. In: Sutcliffe, G., Schulz, S., Tammet, T. (eds.) Proc. of the IJCAR-2004 Workshop on Empirically Successful First-Order Theorem Proving, Cork, Ireland (2004)
Schulz, S.: System Description: E 0.81. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol. 3097, pp. 223–228. Springer, Heidelberg (2004)
Schulz, S.: Empirically Sucessful Topics in Automated Deduction (2008), http://www.eprover.org/EVENTS/es_series.html
Schulz, S.: Fingerprint Indexing for Paramodulation and Rewriting. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 477–483. Springer, Heidelberg (2012)
Sekar, R., Ramakrishnan, I.V., Voronkov, A.: Term Indexing. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. II, ch. 26, pp. 1853–1961. Elsevier Science and MIT Press (2001)
Shannon, C.E., Weaver, W.: The Mathematical Theory of Communication. University of Illinois Press (1949)
Sleator, D.D., Tarjan, R.E.: Self-Adjusting Binary Search Trees. Journal of the ACM 32(3), 652–686 (1985)
Stickel, M.E.: SNARK - SRI’s New Automated Reasoning Kit (2008), http://www.ai.sri.com/~stickel/snark.html (accessed October 04, 2009)
Tammet, T.: Towards Efficient Subsumption. In: Kirchner, C., Kirchner, H. (eds.) CADE 1998. LNCS (LNAI), vol. 1421, pp. 427–441. Springer, Heidelberg (1998)
Voronkov, A.: The Anatomy of Vampire: Implementing Bottom-Up Procedures with Code Trees. Journal of Automated Reasoning 15(2), 238–265 (1995)
Weidenbach, C.: SPASS: Combining Superposition, Sorts and Splitting. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. II, ch. 27, pp. 1965–2013. Elsevier Science and MIT Press (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Schulz, S. (2013). Simple and Efficient Clause Subsumption with Feature Vector Indexing. In: Bonacina, M.P., Stickel, M.E. (eds) Automated Reasoning and Mathematics. Lecture Notes in Computer Science(), vol 7788. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-36675-8_3
Download citation
DOI: https://doi.org/10.1007/978-3-642-36675-8_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-36674-1
Online ISBN: 978-3-642-36675-8
eBook Packages: Computer ScienceComputer Science (R0)