[go: up one dir, main page]
More Web Proxy on the site http://driver.im/ Skip to main content
Springer Nature Link
Log in

SPASS-AR: A First-Order Theorem Prover Based on Approximation-Refinement into the Monadic Shallow Linear Fragment

  • Published:
Journal of Automated Reasoning Aims and scope Submit manuscript

Abstract

We introduce FO-AR, an approximation-refinement approach for first-order theorem proving based on counterexample-guided abstraction refinement. A given first-order clause set N is transformed into an over-approximation \(N^{\prime }\) in a decidable first-order fragment. That means if \(N^{\prime }\) is satisfiable so is N. However, if \(N^{\prime }\) is unsatisfiable, then the approximation provides a lifting terminology for the found refutation which is step-wise transformed into a proof of unsatisfiability for N. If this fails, the cause is analyzed to refine the original clause set such that the found refutation is ruled out for the future and the procedure repeats. The target fragment of the transformation is the monadic shallow linear fragment with straight dismatching constraints, which we prove to be decidable via ordered resolution with selection. We further discuss practical aspects of SPASS-AR, a first-order theorem prover implementing FO-AR. We focus in particularly on effective algorithms for lifting and refinement.

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

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
£29.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (United Kingdom)

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

Explore related subjects

Discover the latest articles, news and stories from top researchers in related subjects.

References

  1. Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. J. Logic Comput. 4(3), 217–247 (1994). Revised version of Max-Planck-Institut für Informatik technical report, MPI-I-91-208, 1991

    Article  MathSciNet  Google Scholar 

  2. Bachmair, L., Ganzinger, H.: Ordered chaining calculi for first-order theories of transitive relations. J. ACM 45(6), 1007–1049 (1998)

    Article  MathSciNet  Google Scholar 

  3. Baeten, J.C.M., Bergstra, J.A., Klop, J.W., Weijland, W.P.: Term-rewriting systems with rule priorities. Theor. Comput. Sci. 67(2 & 3), 283–301 (1989)

    Article  MathSciNet  Google Scholar 

  4. Baumgartner, P., Fuchs, A., Tinelli, C.: Implementing the model evolution calculus. Int. J. Artif. Intell. Tools 15(1), 21–52 (2006). https://doi.org/10.1142/S0218213006002552

    Article  MATH  Google Scholar 

  5. Baumgartner, P., Tinelli, C.: The model evolution calculus. In: Baader, F. (ed.) Automated Deduction—CADE-19, 19th International Conference on Automated Deduction Miami Beach, FL, USA, July 28–August 2, 2003, Proceedings, Lecture Notes in Computer Science, vol. 2741, pp. 350–364. Springer, Berlin (2003). https://doi.org/10.1007/978-3-540-45085-6_32

    Chapter  Google Scholar 

  6. Caferra, R., Leitsch, A., Peltier, N.: Automated Model Building. Applied Logic, vol. 31. Springer, Berlin (2004)

    Book  Google Scholar 

  7. Comon, H., Dauchet, M., Gilleron, R., Löding, C., Jacquemard, F., Lugiez, D., Tison, S., Tommasi, M.: Tree automata techniques and applications. http://www.grappa.univ-lille3.fr/tata (2007). Release October, 12th 2007

  8. Goubault-Larrecq, J.: Deciding \(\cal{H}_1\) by resolution. Inf. Process. Lett. 95(3), 401–408 (2005). https://doi.org/10.1016/j.ipl.2005.04.007

    Article  MathSciNet  MATH  Google Scholar 

  9. Jacquemard, F., Meyer, C., Weidenbach, C.: Unification in extensions of shallow equational theories. In: Nipkow, T. (ed.) Rewriting Techniques and Applications, 9th International Conference, RTA-98, LNCS, vol. 1379, pp. 76–90. Springer, Berlin (1998)

    Chapter  Google Scholar 

  10. Korovin, K.: iprover—an instantiation-based theorem prover for first-order logic (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12–15, 2008, Proceedings, Lecture Notes in Computer Science, vol. 5195, pp. 292–298. Springer, Berlin (2008). https://doi.org/10.1007/978-3-540-71070-7_24

    Chapter  Google Scholar 

  11. Korovin, K.: Inst-Gen—a modular approach to instantiation-based automated reasoning. In: Programming Logics—Essays in Memory of Harald Ganzinger, pp. 239–270 (2013). https://doi.org/10.1007/978-3-642-37651-1_10

    Chapter  Google Scholar 

  12. Kovács, L., Voronkov, A.: First-order theorem proving and vampire. In: Sharygina, N., Veith, H. (eds.) Computer Aided Verification—25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13–19, 2013. Proceedings, Lecture Notes in Computer Science, vol. 8044, pp. 1–35. Springer, Berlin (2013)

    Google Scholar 

  13. Seidl, H., Reuß, A.: Extending H1-clauses with disequalities. Inf. Process. Lett. 111(20), 1007–1013 (2011)

    Article  Google Scholar 

  14. Seidl, H., Reuß, A.: Extending \({\cal{H}}\_1\)-clauses with path disequalities. In: L. Birkedal (ed.) Foundations of Software Science and Computational Structures—15th International Conference, FOSSACS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24–April 1, 2012. Proceedings, Lecture Notes in Computer Science, vol. 7213, pp. 165–179. Springer (2012)

  15. Seidl, H., Verma, K.N.: Cryptographic protocol verification using tractable classes of horn clauses. In: Reps, T., Sagiv, M., Bauer, J. (eds.) Program Analysis and Compilation, Theory and Practice. Lecture Notes in Computer Science, pp. 97–119. Springer, Berlin (2007)

    Chapter  Google Scholar 

  16. Slaney, J.K., Surendonk, T.: Combining finite model generation with theorem proving: problems and prospects. In: Baader, F., Schulz, K.U. (eds.) Frontiers of Combining Systems, First International Workshop FroCoS 1996, Munich, Germany, March 26–29, 1996, Proceedings, Applied Logic Series, vol. 3, pp. 141–155. Kluwer Academic Publishers, Berlin (1996)

    Google Scholar 

  17. Suda, M., Weidenbach, C., Wischnewski, P.: On the saturation of YAGO. In: Automated Reasoning, 5th International Joint Conference, IJCAR 2010, LNAI, vol. 6173, pp. 441–456. Springer, Edinburgh (2010)

    Chapter  Google Scholar 

  18. Sutcliffe, G.: The TPTP problem library and associated infrastructure: the FOF and CNF parts, v3.5.0. J. Autom. Reason. 43(4), 337–362 (2009)

    Article  MathSciNet  Google Scholar 

  19. Teucke, A., Voigt, M., Weidenbach, C.: On the expressivity and applicability of model representation formalisms. In: Herzig, A., Popescu, A. (eds.) Frontiers of Combining Systems—12th International Symposium, FroCoS 2019, London, UK, September 4–6, 2019, Proceedings, Lecture Notes in Computer Science, vol. 11715, pp. 22–39. Springer, Berlin (2019)

    Chapter  Google Scholar 

  20. Teucke, A., Weidenbach, C.: First-order logic theorem proving and model building via approximation and instantiation. In: Lutz, C., Ranise, S. (eds.) Frontiers of Combining Systems: 10th International Symposium, FroCoS 2015, Wroclaw, Poland, September 21–24, 2015, Proceedings, pp. 85–100. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-24246-0_6

    Chapter  Google Scholar 

  21. Teucke, A., Weidenbach, C.: Ordered resolution with straight dismatching constraints. In: P. Fontaine, S. Schulz, J. Urban (eds.) Proceedings of the 5th Workshop on Practical Aspects of Automated Reasoning co-located with International Joint Conference on Automated Reasoning (IJCAR 2016), Coimbra, Portugal, July 2nd, 2016. CEUR Workshop Proceedings, vol. 1635, pp. 95–109. CEUR-WS.org (2016). http://ceur-ws.org/Vol-1635/paper-09.pdf

  22. Teucke, A., Weidenbach, C.: Decidability of the monadic shallow linear first-order fragment with straight dismatching constraints. arXiv:1703.02837 (2017)

  23. Voronkov, A.: AVATAR: the architecture for first-order theorem provers. In: Biere, A., Bloem, R. (eds.) Computer Aided Verification—26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18—22, 2014. Proceedings, Lecture Notes in Computer Science, vol. 8559, pp. 696–710. Springer, Berlin (2014). https://doi.org/10.1007/978-3-319-08867-9_46

    Chapter  Google Scholar 

  24. Weidenbach, C.: Towards an automatic analysis of security protocols in first-order logic. In: Ganzinger, H. (ed.) 16th International Conference on Automated Deduction, CADE-16, LNAI, vol. 1632, pp. 314–328. Springer, Berlin (1999)

    Chapter  Google Scholar 

  25. Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: SPASS version 3.5. In: Schmidt, R.A. (ed.) Automated Deduction—CADE-22, 22nd International Conference on Automated Deduction, Montreal, Canada, August 2–7, 2009. Proceedings, Lecture Notes in Computer Science, vol. 5663, pp. 140–145. Springer, Berlin (2009). https://doi.org/10.1007/978-3-642-02959-2_10

    Chapter  Google Scholar 

Download references

Acknowledgements

We thank the reviewers as well as Konstantin Korovin and Giles Reger for a number of important remarks.

Author information

Authors and Affiliations

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

    Andreas Teucke & Christoph Weidenbach

Authors
  1. Andreas Teucke
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Christoph Weidenbach
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Christoph Weidenbach.

Additional information

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Teucke, A., Weidenbach, C. SPASS-AR: A First-Order Theorem Prover Based on Approximation-Refinement into the Monadic Shallow Linear Fragment. J Autom Reasoning 64, 611–640 (2020). https://doi.org/10.1007/s10817-020-09546-z

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10817-020-09546-z

Keywords

Search

Navigation