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

Case Splitting in an Automatic Theorem Prover for Real-Valued Special Functions

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

Abstract

Case splitting, with and without backtracking, is compared with straightforward ordered resolution. Both forms of splitting have been implemented for MetiTarski, an automatic theorem prover for real-valued special functions such as \(\exp\), ln , sin, cos and tan − 1. The experimental findings confirm the superiority of true backtracking over the simulation of backtracking through the introduction of new predicate symbols, and the superiority of both over straightforward resolution.

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. Akbarpour, B., Paulson, L.: MetiTarski: An automatic theorem prover for real-valued special functions. J. Autom. Reason. 44(3), 175–205 (2010). doi:10.1007/s10817-009-9149-2

    Article  MathSciNet  MATH  Google Scholar 

  2. Bachmair, L., Ganzinger, H.: Resolution theorem proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, chap. 2, pp. 19–99. Elsevier, Amsterdam (2001)

    Google Scholar 

  3. Denman, W., Akbarpour, B., Tahar, S., Zaki, M., Paulson, L.C.: Formal verification of analog designs using MetiTarski. In: Biere, A., Pixley, C. (eds.) Formal Methods in Computer Aided Design, pp. 93–100. IEEE, Piscataway (2009). doi:10.1109/FMCAD.2009.5351136

    Google Scholar 

  4. Fietzke, A., Weidenbach, C.: Labelled splitting. Ann. Math. Artif. Intell. 55, 3–34 (2009). doi:10.1007/s10472-009-9150-9

    Article  MathSciNet  MATH  Google Scholar 

  5. Hurd, J.: Metis first order prover (2007). URL: http://gilith.com/software/metis/

  6. McCune, W., Wos, L.: Otter: The CADE-13 competition incarnations. J. Autom. Reason. 18(2), 211–220 (1997). doi:10.1023/A:1005843632307

    Article  Google Scholar 

  7. Meng, J., Paulson, L.C.: Lightweight relevance filtering for machine-generated resolution problems. J. Appl. Log. 7(1), 41–57 (2009). doi:10.1016/j.jal.2007.07.004

    Article  MathSciNet  MATH  Google Scholar 

  8. Mitrinović, D.S., Vasić, P.M.: Analytic Inequalities. Springer, New York (1970)

    MATH  Google Scholar 

  9. Nivelle, H.: Splitting through new proposition symbols. In: Nieuwenhuis, R., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning: 8th International Conference, LPAR, LNCS 2250, pp. 172–185. Springer, New York (2001). doi:10.1007/3-540-45653-8_12

    Chapter  Google Scholar 

  10. Nonnengart, A., Weidenbach, C.: Computing small clause normal forms. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, chap. 6, pp. 335–367. Elsevier, Amsterdam (2001)

    Google Scholar 

  11. Riazanov, A., Voronkov, A.: Splitting without backtracking. In: International Joint Conference on Artificial Intelligence (IJCAI-17), vol. 1, pp. 611–617 (2001). http://www.cs.man.ac.uk/~voronkov/papers/ijcai01.ps

  12. Sutcliffe, G., Zimmer, J., Schulz, S.: TSTP data-exchange formats for automated theorem proving tools. In: Zhang, W., Sorge, V. (eds.) Distributed Constraint Problem Solving and Reasoning in Multi-Agent Systems, no. 112 in Frontiers in Artificial Intelligence and Applications, pp. 201–215. IOS Press, Amsterdam (2004)

    Google Scholar 

  13. Weidenbach, C.: SPASS - version 0.49. J. Autom. Reason. 18, 247–252 (1997). doi:10.1023/A:1005812220011

    Article  Google Scholar 

  14. Weidenbach, C.: Combining superposition, sorts and splitting. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, chap. 27, pp. 1965–2013. Elsevier, Amsterdam (2001)

    Google Scholar 

  15. Wos, L., Robinson, G.A., Carson, D.F.: Efficiency and completeness of the set of support strategy in theorem proving. J. ACM 12(4), 536–541 (1965). doi:10.1145/321296.321302

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computer Laboratory, University of Cambridge, Cambridge, UK

    James P. Bridge & Lawrence Charles Paulson

Authors
  1. James P. Bridge
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Lawrence Charles Paulson
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Lawrence Charles Paulson.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Bridge, J.P., Paulson, L.C. Case Splitting in an Automatic Theorem Prover for Real-Valued Special Functions. J Autom Reasoning 50, 99–117 (2013). https://doi.org/10.1007/s10817-012-9245-6

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10817-012-9245-6

Keywords

Search

Navigation