Akbarpour, B., Paulson, L.C.: Extending a Resolution Prover for Inequalities on Elementary Functions. In: Dershowitz, N., Voronkov, A. (eds.) LPAR 2007. LNCS (LNAI), vol. 4790, pp. 47–61. Springer, Heidelberg (2007)
Chapter
Google Scholar
Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University press, Cambridge (1998)
Book
MATH
Google Scholar
Bachmair, L., Ganzinger, H.: Resolution theorem proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. I, ch. 2, pp. 19–99. Elsevier Science (2001)
Google Scholar
Baumgartner, P.: Logical Engineering with Instance-Based Methods. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 404–409. Springer, Heidelberg (2007)
Chapter
Google Scholar
Baumgartner, P., Fuchs, A., de Nivelle, H., Tinelli, C.: Computing finite models by reduction to function-free clause logic. J. Applied Logic 7(1), 58–74 (2009)
Article
MathSciNet
MATH
Google Scholar
Baumgartner, P., Fuchs, A., Tinelli, C.: Implementing the model evolution calculus. International Journal on Artificial Intelligence Tools 15(1), 21–52 (2006)
Article
MATH
Google Scholar
Baumgartner, P., Schmidt, R.A.: Blocking and Other Enhancements for Bottom-Up Model Generation Methods. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 125–139. Springer, Heidelberg (2006)
Chapter
Google Scholar
Baumgartner, P., Tinelli, C.: The Model Evolution Calculus. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol. 2741, pp. 350–364. Springer, Heidelberg (2003)
Chapter
Google Scholar
Brand, D.: Proving theorems with the modification method. SIAM J. Comput. 4(4), 412–430 (1975)
Article
MathSciNet
MATH
Google Scholar
Caferra, R., Zabel, N.: A method for simultaneous search for refutations and models by equational constraint solving. Journal of Symbolic Computation 13(6), 613–641 (1992)
Article
MathSciNet
MATH
Google Scholar
Claessen, K., Sorensson, N.: New techniques that improve mace-style finite model finding. In: Baumgartner, P., Fermueller, C. (eds.) Proceedings of the CADE-19 Workshop: Model Computation - Principles, Algorithms, Applications (MODEL 2003) (2003)
Google Scholar
de Moura, L., Bjørner, N.S.: Deciding Effectively Propositional Logic Using DPLL and Substitution Sets. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 410–425. Springer, Heidelberg (2008)
Chapter
Google Scholar
Denzinger, J., Kronenburg, M., Schulz, S.: DISCOUNT - A distributed and learning equational prover. Journal of Automated Reasoning 18(2), 189–198 (1997)
Article
Google Scholar
Eén, N., Biere, A.: Effective Preprocessing in SAT Through Variable and Clause Elimination. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 61–75. Springer, Heidelberg (2005)
Chapter
Google Scholar
Eén, N., Sörensson, N.: An Extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004)
Chapter
Google Scholar
Eiter, T., Faber, W., Traxler, P.: Testing Strong Equivalence of Datalog Programs - Implementation and Examples. In: Baral, C., Greco, G., Leone, N., Terracina, G. (eds.) LPNMR 2005. LNCS (LNAI), vol. 3662, pp. 437–441. Springer, Heidelberg (2005)
Chapter
Google Scholar
Emmer, M., Khasidashvili, Z., Korovin, K., Voronkov, A.: Encoding industrial hardware verification problems into effectively propositional logic. In: Bloem, R., Sharygina, N. (eds.) The 10th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2010), pp. 137–144. IEEE (2010)
Google Scholar
Ganzinger, H., Korovin, K.: New directions in instantiation-based theorem proving. In: Proc. 18th IEEE Symposium on LICS, pp. 55–64. IEEE (2003)
Google Scholar
Ganzinger, H., Korovin, K.: Integrating Equational Reasoning into Instantiation-Based Theorem Proving. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol. 3210, pp. 71–84. Springer, Heidelberg (2004)
Chapter
Google Scholar
Ganzinger, H., Korovin, K.: Theory Instantiation. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol. 4246, pp. 497–511. Springer, Heidelberg (2006)
Chapter
Google Scholar
Graf, P.: Term Indexing. LNCS, vol. 1053. Springer, Heidelberg (1996)
MATH
Google Scholar
Heule, M., Järvisalo, M., Biere, A.: Clause Elimination Procedures for CNF Formulas. In: Fermüller, C.G., Voronkov, A. (eds.) LPAR-17. LNCS, vol. 6397, pp. 357–371. Springer, Heidelberg (2010)
Chapter
Google Scholar
Hoder, K., Kovács, L., Voronkov, A.: Interpolation and Symbol Elimination in Vampire. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS, vol. 6173, pp. 188–195. Springer, Heidelberg (2010)
Chapter
Google Scholar
Hooker, J.N., Rago, G., Chandru, V., Shrivastava, A.: Partial instantiation methods for inference in first order logic. Journal of Automated Reasoning 28, 371–396 (2002)
Article
MathSciNet
MATH
Google Scholar
Hustadt, U., Motik, B., Sattler, U.: Reducing SHIQ-description logic to disjunctive datalog programs. In: The Ninth International Conference on Principles of Knowledge Representation and Reasoning, pp. 152–162. AAAI Press (2004)
Google Scholar
Hustadt, U., Schmidt, R.: MSPASS: Modal Reasoning by Translation and First-Order Resolution. In: Dyckhoff, R. (ed.) TABLEAUX 2000. LNCS, vol. 1847, pp. 67–71. Springer, Heidelberg (2000)
Chapter
Google Scholar
Kapur, D., Narendran, P., Rosenkrantz, D., Zhang, H.: Sufficient-completeness, ground-reducibility and their complexity. Acta Informatica 28(4), 311–350 (1991)
Article
MathSciNet
MATH
Google Scholar
Khasidashvili, Z., Kinanah, M., Voronkov, A.: Verifying equivalence of memories using a first order logic theorem prover. In: The 9th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2009), pp. 128–135. IEEE (2009)
Google Scholar
Kirchner, C., Kirchner, H., Rusinowitch, M.: Deduction with symbolic constraints. Revue Francaise d’Intelligence Artificielle 4(3), 9–52 (1990); Special issue on automated deduction
Google Scholar
Korovin, K.: iProver v0.2. In: Sutcliffe, G. (ed.) The CADE-21 ATP System Competition (CASC-21) (2007), see also [31]
Google Scholar
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)
Chapter
Google Scholar
Korovin, K., Sticksel, C.: iProver-Eq: An Instantiation-Based Theorem Prover with Equality. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS, vol. 6173, pp. 196–202. Springer, Heidelberg (2010)
Chapter
Google Scholar
Korovin, K., Sticksel, C.: Labelled Unit Superposition Calculi for Instantiation-Based Reasoning. In: Fermüller, C.G., Voronkov, A. (eds.) LPAR-17. LNCS, vol. 6397, pp. 459–473. Springer, Heidelberg (2010)
Chapter
Google Scholar
Lassez, J.-L., Marriott, K.: Explicit representation of terms defined by counter examples. Journal of Automated Reasoning 3(3), 301–317 (1987)
Article
MathSciNet
MATH
Google Scholar
Lee, S.-J., Plaisted, D.: Eliminating duplication with the Hyper-linking strategy. Journal of Automated Reasoning 9, 25–42 (1992)
Article
MathSciNet
MATH
Google Scholar
Lynch, C., McGregor, R.E.: Combining Instance Generation and Resolution. In: Ghilardi, S., Sebastiani, R. (eds.) FroCoS 2009. LNCS, vol. 5749, pp. 304–318. Springer, Heidelberg (2009)
Chapter
Google Scholar
McCune, W.: OTTER 3.0 reference manual and guide. Technical Report ANL-94/6, Argonne National Laboratory (1994)
Google Scholar
Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. I, pp. 371–443. Elsevier (2001)
Google Scholar
Navarro Pérez, J.A.: Encoding and Solving Problems in Effectively Propositional Logic. PhD thesis, University of Manchester (2007)
Google Scholar
Navarro-Pérez, J.A., Voronkov, A.: Encodings of Bounded LTL Model Checking in Effectively Propositional Logic. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 346–361. Springer, Heidelberg (2007)
Chapter
Google Scholar
Navarro, J.A., Voronkov, A.: Proof Systems for Effectively Propositional Logic. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 426–440. Springer, Heidelberg (2008)
Chapter
Google Scholar
Pichler, R.: Explicit versus implicit representations of subsets of the Herbrand universe. Theor. Comput. Sci. 290(1), 1021–1056 (2003)
Article
MathSciNet
MATH
Google Scholar
Plaisted, D., Zhu, Y.: Ordered semantic hyper-linking. J. Autom. Reasoning 25(3), 167–217 (2000)
Article
MathSciNet
MATH
Google Scholar
Ramakrishnan, I.V., Sekar, R.C., Voronkov, A.: Term indexing. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 1853–1964. Elsevier and MIT Press (2001)
Google Scholar
Riazanov, A., Voronkov, A.: Splitting without backtracking. In: Proc. of the 17 International Joint Conference on Artificial Intelligence (IJCAI 2001), pp. 611–617. Morgan Kaufmann (2001)
Google Scholar
Riazanov, A., Voronkov, A.: The design and implementation of VAMPIRE. AI Communications 15(2-3), 91–110 (2002)
MATH
Google Scholar
Schulz, S.: E - a brainiac theorem prover. AI Commun. 15(2-3), 111–126 (2002)
MATH
Google Scholar
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. ENTCS. Elsevier Science (2004)
Google Scholar
Suda, M., Weidenbach, C., Wischnewski, P.: On the saturation of YAGO. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS, vol. 6173, pp. 441–456. Springer, Heidelberg (2010)
Chapter
Google Scholar
Sutcliffe, G.: The TPTP Problem Library and Associated Infrastructure: The FOF and CNF Parts, v3.5.0. Journal of Automated Reasoning 43(4), 337–362 (2009)
Article
MathSciNet
MATH
Google Scholar
Sutcliffe, G.: CASC-23 proceedings of the CADE-23 ATP system competition (2011),
http://www.cs.miami.edu/~tptp/CASC/23/Proceedings.pdf