Skip to main content
SpringerLink
Log in

An Abstraction-Refinement Framework for Reasoning with Large Theories

  • Conference paper
  • First Online:
Automated Reasoning (IJCAR 2018)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 10900))

Included in the following conference series:

Abstract

In this paper we present an approach to reasoning with large theories which is based on the abstraction-refinement framework. The proposed approach consists of the following approximations: the over-approximation, the under-approximation and their combination. We present several concrete abstractions based on subsumption, signature grouping and argument filtering. We implemented our approach in a theorem prover for first-order logic iProver and evaluated over the TPTP library.

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 EPUB and 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

Notes

  1. 1.

    Preliminary version of this work was presented at the IWIL workshop [13].

  2. 2.

    iProver is available at: http://www.cs.man.ac.uk/~korovink/iprover/.

References

  1. Alberti, F., Bruttomesso, R., Ghilardi, S., Ranise, S., Sharygina, N.: An extension of lazy abstraction with interpolation for programs with arrays. Formal Methods Syst. Des. 45(1), 63–109 (2014)

    Article  Google Scholar 

  2. Benzmüller, C., Steen, A., Wisniewski, M.: Leo-III version 1.1 (system description). In: Eiter, T., Sands, D., Sutcliffe, G., Voronkov, A. (eds.) IWIL@LPAR 2017. Kalpa Publications in Computing, vol.1, pp. 11–26. EasyChair (2017)

    Google Scholar 

  3. Blanchette, J.C., Böhme, S., Paulson, L.C.: Extending sledgehammer with SMT solvers. J. Autom. Reason. 51(1), 109–128 (2013)

    Article  MathSciNet  Google Scholar 

  4. Blanchette, J.C., Böhme, S., Popescu, A., Smallbone, N.: Encoding monomorphic and polymorphic types. Log. Methods Comput. Sci. 12(4:13), 1–52 (2016)

    MathSciNet  MATH  Google Scholar 

  5. Bonacina, M.P., Lynch, C., de Moura, L.M.: On deciding satisfiability by theorem proving with speculative inferences. J. Autom. Reason. 47(2), 161–189 (2011)

    Article  MathSciNet  Google Scholar 

  6. Brown, C.E.: Reducing higher-order theorem proving to a sequence of SAT problems. J. Autom. Reason. 51(1), 57–77 (2013)

    Article  MathSciNet  Google Scholar 

  7. Bryant, R.E., Kroening, D., Ouaknine, J., Seshia, S.A., Strichman, O., Brady, B.: Deciding bit-vector arithmetic with abstraction. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 358–372. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-71209-1_28

    Chapter  Google Scholar 

  8. Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Trans. Program. Lang. Syst. 16(5), 1512–1542 (1994)

    Article  Google Scholar 

  9. Conchon, S., Goel, A., Krstic, S., Majumdar, R., Roux, M.: Far-cubicle - a new reachability algorithm for cubicle. In: Stewart, D., Weissenbacher, G. (eds.) FMCAD 2017, pp. 172–175. IEEE (2017)

    Google Scholar 

  10. Gauthier, T., Kaliszyk, C.: Sharing HOL4 and HOL light proof knowledge. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) LPAR 2015. LNCS, vol. 9450, pp. 372–386. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-48899-7_26

    Chapter  MATH  Google Scholar 

  11. Ge, Y., de Moura, L.: Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 306–320. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02658-4_25

    Chapter  Google Scholar 

  12. Glimm, B., Kazakov, Y., Liebig, T., Tran, T., Vialard, V.: Abstraction refinement for ontology materialization. In: Bienvenu, M., Ortiz, M., Rosati, R., Simkus, M. (eds.) Informal Proceedings of the 27th International Workshop on Description Logics. CEUR Workshop Proceedings, vol. 1193, pp. 185–196. CEUR-WS.org (2014)

    Google Scholar 

  13. Hernandez, J.C.L., Korovin, K.: Towards an abstraction-refinement framework for reasoning with large theories. In: Eiter, T., Sands, D., Sutcliffe, G., Voronkov, A. (eds.) IWIL@LPAR 2017. Kalpa Publications in Computing, vol. 1. EasyChair (2017)

    Google Scholar 

  14. Hoder, K., Reger, G., Suda, M., Voronkov, A.: Selecting the selection. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS (LNAI), vol. 9706, pp. 313–329. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-40229-1_22

    Chapter  Google Scholar 

  15. Hoder, K., Voronkov, A.: Sine qua non for large theory reasoning. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol. 6803, pp. 299–314. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22438-6_23

    Chapter  Google Scholar 

  16. Irving, G., Szegedy, C., Alemi, A.A., Eén, N., Chollet, F., Urban, J.: DeepMath - deep sequence models for premise selection. In: Lee, D.D., Sugiyama, M., von Luxburg, U., Guyon, I., Garnett, R. (eds.) NIPS 2016, pp. 2235–2243 (2016)

    Google Scholar 

  17. Kaliszyk, C., Urban, J.: HOL(y)Hammer: online ATP service for HOL light. Math. Comput. Sci. 9(1), 5–22 (2015)

    Article  Google Scholar 

  18. Korovin, K.: iProver - an instantiation-based theorem prover for first-order logic (system description). In: Proceedings of the IJCAR 2008, pp. 292–298 (2008)

    Google Scholar 

  19. Korovin, K.: Inst-Gen – a modular approach to instantiation-based automated reasoning. In: Voronkov, A., Weidenbach, C. (eds.) Programming Logics. LNCS, vol. 7797, pp. 239–270. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-37651-1_10

    Chapter  Google Scholar 

  20. Kovács, L., Voronkov, A.: First-order theorem proving and Vampire. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 1–35. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39799-8_1

    Chapter  Google Scholar 

  21. Kumar, R., Myreen, M.O., Norrish, M., Owens, S.: CakeML: a verified implementation of ML. In: POPL 2014, pp. 179–192 (2014)

    Google Scholar 

  22. Lynch, C.: Unsound theorem proving. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol. 3210, pp. 473–487. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30124-0_36

    Chapter  Google Scholar 

  23. Plaisted, D.A.: Theorem proving with abstraction. Artif. Intell. 16(1), 47–108 (1981)

    Article  MathSciNet  Google Scholar 

  24. Reger, G., Bjørner, N., Suda, M., Voronkov, A.: AVATAR modulo theories. In: Benzmüller, C., Sutcliffe, G., Rojas, R. (eds.) GCAI 2016. EPiC Series in Computing, vol. 41, pp. 39–52. EasyChair (2016)

    Google Scholar 

  25. Reynolds, A., Tinelli, C., de Moura, L.M.: Finding conflicting instances of quantified formulas in SMT. In: FMCAD 2014, pp. 195–202. IEEE (2014)

    Google Scholar 

  26. Riazanov, A., Voronkov, A.: Splitting without backtracking. In: Nebel, B. (ed.) Proceedings of the IJCAI 2001, pp. 611–617. Morgan Kaufmann (2001)

    Google Scholar 

  27. Schulz, S.: System description: E 1.8. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR 2013. LNCS, vol. 8312, pp. 735–743. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-45221-5_49

    Chapter  Google Scholar 

  28. Slind, K., Norrish, M.: A brief overview of HOL4. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 28–32. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-71067-7_6

    Chapter  Google Scholar 

  29. Sutcliffe, G.: The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0. J. Autom. Reason. 59(4), 483–502 (2017)

    Article  MathSciNet  Google Scholar 

  30. Sutcliffe, G., Puzis, Y.: SRASS - a semantic relevance axiom selection system. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 295–310. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73595-3_20

    Chapter  Google Scholar 

  31. Teucke, A., Weidenbach, C.: First-order logic theorem proving and model building via approximation and instantiation. In: Lutz, C., Ranise, S. (eds.) FroCoS 2015. LNCS (LNAI), vol. 9322, pp. 85–100. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-24246-0_6

    Chapter  Google Scholar 

  32. Urban, J.: MaLARea: a metasystem for automated reasoning in large theories. In: CEUR Workshop Proceedings, vol. 257, pp. 45–58 (2007)

    Google Scholar 

  33. Urban, J., Sutcliffe, G., Pudlák, P., Vyskočil, J.: MaLARea SG1 - machine learner for automated reasoning with semantic guidance. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 441–456. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-71070-7_37

    Chapter  MATH  Google Scholar 

Download references

Acknowledgements

We would like to thank anonymous reviewers for many helpful suggestions.

Author information

Authors and Affiliations

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

    Julio Cesar Lopez Hernandez & Konstantin Korovin

Authors
  1. Julio Cesar Lopez Hernandez
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Konstantin Korovin
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Konstantin Korovin .

Editor information

Editors and Affiliations

  1. Université de Lorraine, Vandoeuvre-lès-Nancy, France

    Didier Galmiche

  2. Baden-Wuerttemberg Cooperative State University, Stuttgart, Germany

    Stephan Schulz

  3. University of Trento, Trento, Italy

    Roberto Sebastiani

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG, part of Springer Nature

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Lopez Hernandez, J.C., Korovin, K. (2018). An Abstraction-Refinement Framework for Reasoning with Large Theories. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds) Automated Reasoning. IJCAR 2018. Lecture Notes in Computer Science(), vol 10900. Springer, Cham. https://doi.org/10.1007/978-3-319-94205-6_43

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-94205-6_43

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-94204-9

  • Online ISBN: 978-3-319-94205-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation