Advertisement

Exploring Automated Reasoning in First-Order Logic: Tools, Techniques and Application Areas

  • Vladimir Pavlov
  • Alexander Schukin
  • Tanzilia Cherkasova
Part of the Communications in Computer and Information Science book series (CCIS, volume 394)

Abstract

This paper describes state-of-the-art automated reasoning techniques and applications. We explore mainly first-order logic theorem proving, though our discussion also covers other domains: higher-order logic, propositional logic. We review applications of theorem proving systems in mathematics, formal verification, and other areas.

It is known that resolution is the most popular reasoning technique in first-order logic. Nevertheless, studying other algorithms could facilitate the development of automated reasoning. This article presents a survey of some promising methods. In particular, we give a detailed description of Maslov’s inverse method that is applicable to a broad range of theories and also can be used as a decision procedure. However, this method is not well studied and its real potential is yet to be realized. We describe the architecture of our reasoning system that we use to compare the inverse method with the resolution method in practice. We also present some actual results of experiments.

Keywords

automated reasoning automated theorem proving resolution inverse method first-order logic 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Avigad, J., et al.: A formally verified proof of the prime number theorem. ACM Transactions on Computational Logic (TOCL) 9(1) (2007)Google Scholar
  2. 2.
    Bachmair, L.: Paramodulation, superposition, and simplification. In: Gottlob, G., Leitsch, A., Mundici, D. (eds.) KGC 1997. LNCS, vol. 1289, pp. 1–3. Springer, Heidelberg (1997)CrossRefGoogle Scholar
  3. 3.
    Bachmair, L., Ganzinger, H.: Resolution theorem proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. 1, pp. 19–99 (2001)Google Scholar
  4. 4.
    Baumgartner, P., Furbach, U., Niemelä, I.: Hyper tableaux. In: Orłowska, E., Alferes, J.J., Moniz Pereira, L. (eds.) JELIA 1996. LNCS, vol. 1126, pp. 1–17. Springer, Heidelberg (1996)CrossRefGoogle Scholar
  5. 5.
    Bledsoe, W.W.: Non-resolution theorem proving. Artificial Intelligence 9(1), 1–35 (1977)MathSciNetCrossRefzbMATHGoogle Scholar
  6. 6.
    Bridge, J.P.: Machine learning and automated theorem proving. Technical Report, Cambridge (2010), http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-792.pdf
  7. 7.
    Chen, C., Li, R.: Matematicheskaya logika I avtomaticheskoe dokazatel’stvo teorem (Russian) (Mathematical Logic and Automatic Theorem Proving). In: Translated from English by Davydov, G. V., Mints, G. E., Sochilina, A. V. Edited by Maslov, S.Y. With appendixes by Maslov, S.Y., Mints, G.E., Orevkov, V. P. Nauka, Moscow (1983)Google Scholar
  8. 8.
    Chlipala, A., Necula, G.C.: Cooperative Integration of an Interactive Proof Assistant and an Automated Prover. In: Proceedings of the 6th International Workshop on Strategies in Automated Deduction, STRATEGIES 2006 (2006)Google Scholar
  9. 9.
    Davis, M., Logemann, G., Loveland, D.: A Machine Program for Theorem Proving. Communications of the ACM 5(7), 394–397 (1962)MathSciNetCrossRefzbMATHGoogle Scholar
  10. 10.
    Degtyarev, A., Voronkov, A.: The inverse method. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. 1, pp. 179–272 (2001)Google Scholar
  11. 11.
    Dumitrescu, D., Oltean, M.: An Evolutionary Algorithm for Theorem Proving in Propositional Logic. Studia Universitatis Babes-Bolyai, Informatica 44(2), 87–98 (1999)MathSciNetzbMATHGoogle Scholar
  12. 12.
    Furbach, U., Obermaier, C.: Applications of Automated Reasoning. In: Freksa, C., Kohlhase, M., Schill, K. (eds.) KI 2006. LNCS (LNAI), vol. 4314, pp. 174–187. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  13. 13.
    Gebser, M., et al.: Conflict-driven answer set solving. In: Proceedings of the 20th International Joint Conference on Artificial Intelligence (IJCAI 2007), pp. 386–392 (2007)Google Scholar
  14. 14.
    Gonthier, G.: A computer-checked proof of the Four Colour Theorem. Microsoft Research Cambridge (2005), http://research.microsoft.com/en-us/um/people/gonthier/4colproof.pdf
  15. 15.
    Gonthier, G.: Engineering mathematics: the odd order theorem proof. In: POPL 2013, pp. 1–2 (2013)Google Scholar
  16. 16.
    Hagen, R.A., Goodwin, S., Sattar, A.: Code improvements for model elimination based reasoning systems. In: Proceedings of the 27th Australasian Conference on Computer Science, ACSC 2004, vol. 26, pp. 233–240 (2004)Google Scholar
  17. 17.
    Hähnle, R.: Tableaux and Related Methods. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. 1, pp. 101–177 (2001)Google Scholar
  18. 18.
    Harrison, J.: A short survey of automated reasoning. In: Anai, H., Horimoto, K., Kutsia, T. (eds.) AB 2007. LNCS, vol. 4545, pp. 334–349. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  19. 19.
    Harrison, J.: Floating-Point Verification using Theorem Proving. In: Bernardo, M., Cimatti, A. (eds.) SFM 2006. LNCS, vol. 3965, pp. 211–242. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  20. 20.
    Harrison, J.: Formal verification of IA-64 division algorithms. In: Aagaard, M.D., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol. 1869, pp. 234–251. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  21. 21.
    Harrison, J.: Handbook of Practical Logic and Automated Reasoning. Cambridge University Press, New York (2009)CrossRefzbMATHGoogle Scholar
  22. 22.
    Hoops, H.H., Stützle, T.: Local Search Algorithms for SAT: An Empirical Evaluation. Journal of Automated Reasoning 24(4), 421–481 (2000)CrossRefGoogle Scholar
  23. 23.
    Horrocks, I., Patel-Schneider, P.F.: Knowledge Representation and Reasoning on the Semantic Web: OWL. In: Domingue, J., Fensel, D., Hendler, J.A. (eds.) Handbook of Semantic Web Technologies, pp. 365–398. Springer (2011)Google Scholar
  24. 24.
    Katsiri, E., Mycroft, A.: Model checking for sentient computing: An axiomatic approach. In: Proceedings of the 1st Workshop on Semantics for Mobile Environments, SME 2005 (2005), http://www.cl.cam.ac.uk/research/dtg/www/files/publications/public/ek236/satisfiability6.pdf
  25. 25.
    Kaufmann, M., Moore, J.S.: Some Key Research Problems in Automated Theorem Proving for Hardware and Software Verification. In: Revista de la Real Academia de Ciencias Exactas, Físicas y Naturales. Serie A: Matemáticas (RACSAM) 98(1/2), 181–195 (2004) ISSN 1578-7303Google Scholar
  26. 26.
    Khalifa, M., Raafat, H., Almulla, M.: Machine Learning Approach to Enhance the Design of Automated Theorem Provers. In: Huang, T., Zeng, Z., Li, C., Leung, C.S. (eds.) ICONIP 2012, Part II. LNCS, vol. 7664, pp. 673–682. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  27. 27.
    Kornilowicz, A.: Formalization of the Jordan Curve Theorem in Mizar. In: International Congress of Mathematicians, Volume of Abstracts, p. 611 (2006)Google Scholar
  28. 28.
    Kowalski, R.: Predicate Logic as a Programming Language. In: Proceedings of the IFIP Congress, pp. 569–574 (1974)Google Scholar
  29. 29.
    Letz, R., Stenz, G.: Model elimination and connection tableau procedures. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 2015–2112 (2001)Google Scholar
  30. 30.
    Lifschitz, V.: What is the inverse method? Journal of Automated Reasoning 5(1), 1–23 (1989)MathSciNetCrossRefzbMATHGoogle Scholar
  31. 31.
    Loveland, D.W.: Mechanical Theorem-Proving by Model Elimination. Journal of the ACM 15(2), 236–251 (1968)MathSciNetCrossRefzbMATHGoogle Scholar
  32. 32.
    Maslov, S.Y.: The inverse method for establishing deducibility for logical calculi. Logical and logical-mathematical calculus (Russian). Trudy Mat. Inst. Steklov. 98(pt.I), 26–87 (1968)MathSciNetzbMATHGoogle Scholar
  33. 33.
    McCune, W.: Solution of the Robbins problem. Journal of Automated Reasoning 19(3), 263–276 (1997)MathSciNetCrossRefzbMATHGoogle Scholar
  34. 34.
    Meng, J.: Integration of interactive and automatic provers. In: Second CologNet Workshop on Implementation Technology Computational Logic Systems (2003)Google Scholar
  35. 35.
    Mints, G.: Decidability of the Class E by Maslov”s Inverse Method. In: Blass, A., Dershowitz, N., Reisig, W. (eds.) Gurevich Festschrift. LNCS, vol. 6300, pp. 529–537. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  36. 36.
    Nordin, P., Eriksson, A., Nordahl, M.G.: Genetic Reasoning: Evolutionary Induction of Mathematical Proofs. In: Langdon, W.B., Fogarty, T.C., Nordin, P., Poli, R. (eds.) EuroGP 1999. LNCS, vol. 1598, pp. 221–231. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  37. 37.
    Paskevich, A.: Connection Tableaux with Lazy Paramodulation. Journal of Automated Reasoning 40(2-3), 179–194 (2008)MathSciNetCrossRefzbMATHGoogle Scholar
  38. 38.
    Pratt, V.R.: Anatomy of the Pentium bug. In: Mosses, P.D., Nielsen, M. (eds.) CAAP 1995, FASE 1995, and TAPSOFT 1995. LNCS, vol. 915, pp. 97–107. Springer, Heidelberg (1995)CrossRefGoogle Scholar
  39. 39.
    Reed, J.N., Sinclair, J.E., Guigand, F.: Deductive Reasoning versus Model Checking: Two Formal Approaches for System Development. In: Proceedings of the 1st International Conference on Integrated Formal Methods (IFM), pp. 375–394 (1999)Google Scholar
  40. 40.
    Robinson, J.A.: A Machine-Oriented Logic Based on the Resolution Principle. Communications of the ACM 5, 23–41 (1965)Google Scholar
  41. 41.
    Schulz, S.: E – A Brainiac Theorem Prover. Journal of AI Communications 15(2/3), 111–126 (2002)zbMATHGoogle Scholar
  42. 42.
    Smullyan, R.M.: First-Order Logic. Courier Dover Publications (1995)Google Scholar
  43. 43.
    Stump, A.: Programming with Proofs: Language-Based Approaches to Totally Correct Software. In: Meyer, B., Woodcock, J. (eds.) VSTTE 2005. LNCS, vol. 4171, pp. 502–509. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  44. 44.
    Sutcliffe, J.: Automated theorem proving: theory and practice. AI Magazine 23(1), 121–122 (2002)Google Scholar
  45. 45.
    Sutcliffe, J., Suttner, C.: The TPTP Problem Library. Journal of Automated Reasoning 21(2), 177–203 (1988)MathSciNetCrossRefGoogle Scholar
  46. 46.
    Szekeres, G., Peters, L.: Computer solution to the 17-point Erdős-Szekeres problem. ANZIAM Journal 48(2), 151–164 (2006)MathSciNetCrossRefzbMATHGoogle Scholar
  47. 47.
    Tiwari, A., Gulwani, S.: Logical interpretation: Static program analysis using theorem proving. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 147–166. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  48. 48.
    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)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2013

Authors and Affiliations

  • Vladimir Pavlov
    • 1
  • Alexander Schukin
    • 1
  • Tanzilia Cherkasova
    • 1
  1. 1.Department of Management and Information TechnologySt. Petersburg State Polytechnical UniversitySt. PetersburgRussia

Personalised recommendations