Skip to main content
SpringerLink
Log in

Completion-Based Automated Theory Exploration

  • Conference paper
Advances in Artificial Intelligence and Its Applications (MICAI 2013)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 8265))

Included in the following conference series:

  • 1320 Accesses

Abstract

Completion-based automated theory exploration is a method to explore inductive theories with the aid of a convergent rewrite system. It combines a method to synthesise conjectures/definitions in a theory with a completion algorithm. Completion constructs a convergent rewrite system which is then used to reduce redundancies and improve prove automation during the exploration of the theory. However, completion does not always succeed on a set of identities and a reduction ordering. A common failure occurs when an initial identity or a normal form of a critical pair cannot be oriented by the given ordering. A popular solution to this problem consists in using the instances of those rules which can be oriented for rewriting, namely ordered rewriting. Extending completion to ordered rewriting leads to ‘unfailing completion’. In this paper, we extend the class of theories on which the completion-based automated theory exploration method can be applied by using unfailing completion. This produce stronger normalization methods compared to those in [20,21]. The techniques described are implemented in the theory exploration system IsaScheme.

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. Avenhaus, J., Hillenbrand, T., Löchner, B.: On using ground joinable equations in equational theorem proving. Journal of Symbolic Computation 36(1-2), 217–233 (2003); First Order Theorem Proving.

    Google Scholar 

  2. Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press (1998)

    Google Scholar 

  3. Bahr, P.: Partial order infinitary term rewriting and böhm trees. In: Lynch, C. (ed.) Proceedings of the 21st International Conference on Rewriting Techniques and Applications, Dagstuhl, Germany. Leibniz International Proceedings in Informatics (LIPIcs), vol. 6, pp. 67–84. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik (2010)

    Google Scholar 

  4. Blanchette, J.C., Nipkow, T.: Nitpick: A counterexample generator for higher-order logic based on a relational model finder. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 131–146. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  5. Buchberger, B.: Algorithm Invention and Verification by Lazy Thinking. In: Petcu, D., Negru, V., Zaharie, D., Jebelean, T. (eds.) Proceedings of SYNASC 2003, 5th International Workshop on Symbolic and Numeric Algorithms for Scientific Computing Timisoara, Timisoara, Romania, October 1-4, pp. 2–26. Mirton Publisher (2003)

    Google Scholar 

  6. Buchberger, B., Craciun, A.: Algorithm synthesis by lazy thinking: Using problem schemes. In: Petcu, D., Negru, V., Zaharie, D., Jebelean, T. (eds.) Proceedings of SYNASC 2004, 6th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, Timisoara, Romania, pp. 90–106. Mirton Publisher (2004)

    Google Scholar 

  7. Claessen, K., Hughes, J.: Quickcheck: a lightweight tool for random testing of Haskell programs. In: ICFP 2000: Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming, pp. 268–279. ACM, New York (2000)

    Chapter  Google Scholar 

  8. Claessen, K., Johansson, M., Rosén, D., Smallbone, N.: Automating inductive proofs using theory exploration. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol. 7898, pp. 392–406. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  9. Colton, S.: Automated Theory Formation in Pure Mathematics. PhD thesis, Division of Informatics, University of Edinburgh (2001)

    Google Scholar 

  10. Johansson, M.: Automated Discovery of Inductive Lemmas. PhD thesis, School of Informatics, University of Edinburgh (2009)

    Google Scholar 

  11. Johansson, M., Dixon, L., Bundy, A.: Conjecture synthesis for inductive theories. Journal of Automated Reasoning (2010) (accepted for publication, to appear)

    Google Scholar 

  12. Krauss, A.: Automating Recursive Definitions and Termination Proofs in Higher-Order Logic. PhD thesis, Dept. of Informatics, T. U. München (2009)

    Google Scholar 

  13. Lenat, D.B.: AM: An artificial intelligence approach to discovery in mathematics as heuristic search. In: Knowledge-Based Systems in Artificial Intelligence. McGraw Hill, New York (1982); Stanford as TechReport AIM 286

    Google Scholar 

  14. Lin, Y., Bundy, A., Grov, G.: The use of rippling to automate event-b invariant preservation proofs. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol. 7226, pp. 231–236. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  15. Llano, M.T., Ireland, A., Pease, A.: Discovery of invariants through automated theory formation. In: Refine, pp. 1–19 (2011)

    Google Scholar 

  16. Maclean, E., Ireland, A., Grov, G.: The core system: Animation and functional correctness of pointer programs. In: International Conference on Automated Software Engineering, pp. 588–591 (2011)

    Google Scholar 

  17. Martin, U., Nipkow, T.: Ordered rewriting and confluence. In: Stickel, M.E. (ed.) CADE 1990. LNCS, vol. 449, pp. 366–380. Springer, Heidelberg (1990)

    Chapter  Google Scholar 

  18. Mayr, R., Nipkow, T.: Higher-order rewrite systems and their confluence. Theoretical Computer Science 192, 3–29 (1998)

    Article  MathSciNet  MATH  Google Scholar 

  19. McCasland, R., Bundy, A., Smith, P.: Ascertaining mathematical theorems. In: Carette, J., William, W., Farmer, M. (eds.) Proceedings of Calculemus 2005, Newcastle, UK (2005)

    Google Scholar 

  20. Montano-Rivas, O., McCasland, R., Dixon, L., Bundy, A.: Scheme-based synthesis of inductive theories. In: Sidorov, G., Hernández Aguirre, A., Reyes García, C.A. (eds.) MICAI 2010, Part I. LNCS, vol. 6437, pp. 348–361. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  21. Montano-Rivas, O., McCasland, R., Dixon, L., Bundy, A.: Scheme-based theorem discovery and concept invention. Expert Systems with Applications 39(2), 1637–1646 (2012)

    Article  Google Scholar 

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

    Book  MATH  Google Scholar 

  23. Paulson, L.C.: A higher-order implementation of rewriting. Science of Computer Programming 3, 119–149 (1983)

    Article  MathSciNet  MATH  Google Scholar 

  24. Rubio, A., Nieuwenhuis, R.: A total ac-compatible ordering based on rpo. Theoretical Computer Science 142, 209–227 (1995)

    Article  MathSciNet  MATH  Google Scholar 

  25. Sutcliffe, G., Gao, Y., Colton, S.: A Grand Challenge of Theorem Discovery (June 2003)

    Google Scholar 

  26. Walukiewicz, D.: A total AC-compatible reduction ordering on higher-order terms. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 530–542. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Academia de Tecnologías de Información y Telemática, Universidad Politécnica de San Luis Potosí, Urbano Villalón 500, 78362, San Luis Potosí, S.L.P., México

    Omar Montano-Rivas

Authors
  1. Omar Montano-Rivas
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Universidad Autónoma del Estado de Hidalgo, Ciudad Universitaria,, Carretera Pachuca–Tulancingo km 4.5, Hidalgo, Mexico

    Félix Castro

  2. Centro de Investigación en Computación, Instituto Politécnico Nacional, Av. Juan Dios Bátiz s/n, Col. Nueva Industrial Vallejo, 07738, Mexico City, Mexico

    Alexander Gelbukh

  3. Tecnológico de Monterrey, Campus Estado de México,, Carretera Lago de Guadalupe Km 3.5, Atizapán de Zaragoza,, CP 52926, Estado de México, Mexico

    Miguel González

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Montano-Rivas, O. (2013). Completion-Based Automated Theory Exploration. In: Castro, F., Gelbukh, A., González, M. (eds) Advances in Artificial Intelligence and Its Applications. MICAI 2013. Lecture Notes in Computer Science(), vol 8265. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-45114-0_8

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-45114-0_8

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-45113-3

  • Online ISBN: 978-3-642-45114-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation