Skip to main content
SpringerLink
Log in

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

  • Conference paper
Book cover Knowledge Engineering and the Semantic Web (KESW 2013)

Part of the book series: Communications in Computer and Information Science ((CCIS,volume 394))

Included in the following conference series:

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.

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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  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. 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)

    Chapter  Google Scholar 

  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. 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)

    Chapter  Google Scholar 

  5. Bledsoe, W.W.: Non-resolution theorem proving. Artificial Intelligence 9(1), 1–35 (1977)

    Article  MathSciNet  MATH  Google Scholar 

  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. 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. 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. Davis, M., Logemann, G., Loveland, D.: A Machine Program for Theorem Proving. Communications of the ACM 5(7), 394–397 (1962)

    Article  MathSciNet  MATH  Google Scholar 

  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. Dumitrescu, D., Oltean, M.: An Evolutionary Algorithm for Theorem Proving in Propositional Logic. Studia Universitatis Babes-Bolyai, Informatica 44(2), 87–98 (1999)

    MathSciNet  MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  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. 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. Gonthier, G.: Engineering mathematics: the odd order theorem proof. In: POPL 2013, pp. 1–2 (2013)

    Google Scholar 

  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. 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. 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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  21. Harrison, J.: Handbook of Practical Logic and Automated Reasoning. Cambridge University Press, New York (2009)

    Book  MATH  Google Scholar 

  22. Hoops, H.H., Stützle, T.: Local Search Algorithms for SAT: An Empirical Evaluation. Journal of Automated Reasoning 24(4), 421–481 (2000)

    Article  Google Scholar 

  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. 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. 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-7303

    Google Scholar 

  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)

    Chapter  Google Scholar 

  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. Kowalski, R.: Predicate Logic as a Programming Language. In: Proceedings of the IFIP Congress, pp. 569–574 (1974)

    Google Scholar 

  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. Lifschitz, V.: What is the inverse method? Journal of Automated Reasoning 5(1), 1–23 (1989)

    Article  MathSciNet  MATH  Google Scholar 

  31. Loveland, D.W.: Mechanical Theorem-Proving by Model Elimination. Journal of the ACM 15(2), 236–251 (1968)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    MathSciNet  MATH  Google Scholar 

  33. McCune, W.: Solution of the Robbins problem. Journal of Automated Reasoning 19(3), 263–276 (1997)

    Article  MathSciNet  MATH  Google Scholar 

  34. Meng, J.: Integration of interactive and automatic provers. In: Second CologNet Workshop on Implementation Technology Computational Logic Systems (2003)

    Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  37. Paskevich, A.: Connection Tableaux with Lazy Paramodulation. Journal of Automated Reasoning 40(2-3), 179–194 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  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. Robinson, J.A.: A Machine-Oriented Logic Based on the Resolution Principle. Communications of the ACM 5, 23–41 (1965)

    Google Scholar 

  41. Schulz, S.: E – A Brainiac Theorem Prover. Journal of AI Communications 15(2/3), 111–126 (2002)

    MATH  Google Scholar 

  42. Smullyan, R.M.: First-Order Logic. Courier Dover Publications (1995)

    Google Scholar 

  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)

    Chapter  Google Scholar 

  44. Sutcliffe, J.: Automated theorem proving: theory and practice. AI Magazine 23(1), 121–122 (2002)

    Google Scholar 

  45. Sutcliffe, J., Suttner, C.: The TPTP Problem Library. Journal of Automated Reasoning 21(2), 177–203 (1988)

    Article  MathSciNet  Google Scholar 

  46. Szekeres, G., Peters, L.: Computer solution to the 17-point Erdős-Szekeres problem. ANZIAM Journal 48(2), 151–164 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Management and Information Technology, St. Petersburg State Polytechnical University, 195251, St. Petersburg, Russia

    Vladimir Pavlov, Alexander Schukin & Tanzilia Cherkasova

Authors
  1. Vladimir Pavlov
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Alexander Schukin
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Tanzilia Cherkasova
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Institute of Artificial Intelligence, University of Ulm, 89069, Ulm, Germany

    Pavel Klinov

  2. Intelligence Systems Laboratory, Saint Petersburg National Research University of Information Technologies, Mechanics and Optics, Kronverksky prospekt 49, office 380,, 197101, St. Petersburg, Russia

    Dmitry Mouromtsev

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Pavlov, V., Schukin, A., Cherkasova, T. (2013). Exploring Automated Reasoning in First-Order Logic: Tools, Techniques and Application Areas. In: Klinov, P., Mouromtsev, D. (eds) Knowledge Engineering and the Semantic Web. KESW 2013. Communications in Computer and Information Science, vol 394. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-41360-5_9

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-41360-5_9

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-41359-9

  • Online ISBN: 978-3-642-41360-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation