Extending a Resolution Prover for Inequalities on Elementary Functions

1. Akbarpour, B., Paulson, L.C.: Towards automatic proofs of inequalities involving elementary functions. In: Cook, B., Sebastiani, R. (eds.) PDPAR: Pragmatics of Decision Procedures in Automated Reasoning, pp. 27–37 (2006)

   Google Scholar 

2. Avigad, J., Donnelly, K., Gray, D., Raff, P.: A formally verified proof of the prime number theorem. ACM Transactions on Computational Logic (in press)

   Google Scholar 

3. Avigad, J., Friedman, H.: Combining decision procedures for the reals. Logical Methods in Computer Science 2(4) (2006)

   Google Scholar 

4. 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, Amsterdam (2001)

   Google Scholar 

5. Barwise, J.: An introduction to first-order logic. In: Barwise, J. (ed.) Handbook of Mathematical Logic, pp. 5–46. North-Holland, Amsterdam (1977)

   Google Scholar 

6. Beeson, M.: Automatic generation of a proof of the irrationality of e. JSC 32(4), 333–349 (2001)

   MATH  MathSciNet  Google Scholar 

7. Brown, C.W.: QEPCAD B: a program for computing with semi-algebraic sets using CADs. SIGSAM Bulletin 37(4), 97–108 (2003)

   Article  MATH  Google Scholar 

8. Clarke, E., Zhao, X.: Analytica: A theorem prover for Mathematica. Mathematica Journal 3(1), 56–71 (1993)

   Google Scholar 

9. Dolzmann, A., Sturm, T., Weispfenning, V.: Real quantifier elimination in practice. Technical Report MIP-9720, Universität Passau, D-94030, Germany (1997)

   Google Scholar 

10. Flanagan, C., Joshi, R., Ou, X., Saxe, J.B.: Theorem proving using lazy proof explication. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 355–367. Springer, Heidelberg (2003)

    Google Scholar 

11. Grégoire, B., Mahboubi, A.: Proving equalities in a commutative ring done right in coq. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 98–113. Springer, Heidelberg (2005)

    Google Scholar 

12. Hörmander, L.: The Analysis of Linear Partial Differential Operators II: Differential Operators with Constant Coefficient. Springer, Heidelberg (2006) First published in 1983; cited by Mclaughlin and Harrison [15]

    Google Scholar 

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

14. McCune, W., Wos, L.: Otter: The CADE-13 competition incarnations. Journal of Automated Reasoning 18(2), 211–220 (1997)

    Article  Google Scholar 

15. McLaughlin, S., Harrison, J.: A proof-producing decision procedure for real arithmetic. In: Nieuwenhuis, R. (ed.) CADE-20. LNCS (LNAI), vol. 3632, pp. 295–314. Springer, Heidelberg (2005)

    Google Scholar 

16. Nipkow, T., Paulson, L.C., Wenzel, M. (eds.): Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002)

    MATH  Google Scholar 

17. Prevosto, V., Waldmann, U.: SPASS+T. In: Sutcliffe, G., Schmidt, R., Schulz, S.: (eds.) FLoC 2006 Workshop on Empirically Successful Computerized Reasoning, vol. 192 of CEUR Workshop Proceedings, pp. 18–33 (2006)

    Google Scholar 

Download references