Skip to main content
SpringerLink
Log in

Inst-Gen – A Modular Approach to Instantiation-Based Automated Reasoning

  • Chapter
Programming Logics

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 7797))

Abstract

Inst-Gen is an instantiation-based reasoning method for first-order logic introduced in [18]. One of the distinctive features of Inst-Gen is a modular combination of first-order reasoning with efficient ground reasoning. Thus, Inst-Gen provides a framework for utilising efficient off-the-shelf propositional SAT and SMT solvers as part of general first-order reasoning. In this paper we present a unified view on the developments of the Inst-Gen method: (i) completeness proofs; (ii) abstract and concrete criteria for redundancy elimination, including dismatching constraints and global subsumption; (iii) implementation details and evaluation.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 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 

  2. Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University press, Cambridge (1998)

    Book  MATH  Google Scholar 

  3. 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 

  4. 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 

  5. 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 

  6. 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 

  7. 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 

  8. 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 

  9. Brand, D.: Proving theorems with the modification method. SIAM J. Comput. 4(4), 412–430 (1975)

    Article  MathSciNet  MATH  Google Scholar 

  10. 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 

  11. 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 

  12. 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 

  13. 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 

  14. 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 

  15. 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 

  16. 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 

  17. 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 

  18. 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 

  19. 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 

  20. 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 

  21. Graf, P.: Term Indexing. LNCS, vol. 1053. Springer, Heidelberg (1996)

    MATH  Google Scholar 

  22. 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 

  23. 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 

  24. 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 

  25. 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 

  26. 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 

  27. 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 

  28. 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 

  29. 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 

  30. Korovin, K.: iProver v0.2. In: Sutcliffe, G. (ed.) The CADE-21 ATP System Competition (CASC-21) (2007), see also [31]

    Google Scholar 

  31. 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 

  32. 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 

  33. 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 

  34. 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 

  35. 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 

  36. 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 

  37. McCune, W.: OTTER 3.0 reference manual and guide. Technical Report ANL-94/6, Argonne National Laboratory (1994)

    Google Scholar 

  38. 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 

  39. Navarro Pérez, J.A.: Encoding and Solving Problems in Effectively Propositional Logic. PhD thesis, University of Manchester (2007)

    Google Scholar 

  40. 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 

  41. 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 

  42. 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 

  43. Plaisted, D., Zhu, Y.: Ordered semantic hyper-linking. J. Autom. Reasoning 25(3), 167–217 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  44. 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 

  45. 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 

  46. Riazanov, A., Voronkov, A.: The design and implementation of VAMPIRE. AI Communications 15(2-3), 91–110 (2002)

    MATH  Google Scholar 

  47. Schulz, S.: E - a brainiac theorem prover. AI Commun. 15(2-3), 111–126 (2002)

    MATH  Google Scholar 

  48. 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 

  49. 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 

  50. 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 

  51. Sutcliffe, G.: CASC-23 proceedings of the CADE-23 ATP system competition (2011), http://www.cs.miami.edu/~tptp/CASC/23/Proceedings.pdf

Download references

Author information

Authors and Affiliations

  1. School of Computer Science, The University of Manchester, UK

    Konstantin Korovin

Authors
  1. Konstantin Korovin
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. University of Manchester, Oxford Road, M13 9PL, Manchester, UK

    Andrei Voronkov

  2. Max-Planck-Institut für Informatik, Campus E1 4, 66123, Saarbrücken, Germany

    Christoph Weidenbach

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Korovin, K. (2013). Inst-Gen – A Modular Approach to Instantiation-Based Automated Reasoning. In: Voronkov, A., Weidenbach, C. (eds) Programming Logics. Lecture Notes in Computer Science, vol 7797. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-37651-1_10

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-37651-1_10

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-37650-4

  • Online ISBN: 978-3-642-37651-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation