Skip to main content
SpringerLink
Log in

Using Mixture of Experts Method in Combining Search-Guiding Heuristics for Theorem Proving

  • Conference paper
  • First Online:
Computer and Information Sciences

Part of the book series: Lecture Notes in Electrical Engineering ((LNEE,volume 62))

  • 813 Accesses

Abstract

The main challenge of automated theorem proving is to find a way to shorten the search process. Therefore using a good heuristic method is essential. Instead of constructing a heuristic from scratch, we propose to use the mixture of experts learning to combine the existing heuristics to construct a heuristic from similar problems. The results show that the combined heuristic is better than each individual heuristic used in combination.

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 169.00
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 219.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 219.99
Price excludes VAT (USA)
  • Durable hardcover 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. J. Denzinger, M. Fuchs, C. Goller, and S. Schulz.: Learning from Previous Proof Experience: A Survey. Technical Report AR-99-4, Fakultät für Informatik der Technischen Universität München, 1999.

    Google Scholar 

  2. M. Fuchs.: Automatic Selection of Search-Guiding Heuristics. Proc. of FLAIRS, pages 1–5, 1997.

    Google Scholar 

  3. C. Suttner and W. Ertel.: Automatic Acquisition of Search Guiding Heuristics. Proc. of International Conference on Automated Deduction, pages 470–484, 1990.

    Google Scholar 

  4. M. Fuchs and M. Fuchs.: Applying Case-Based Reasoning to Automated Deduction. Proc. of International Conference on Case-Based Reasoning, pages 23–32, 1997.

    Google Scholar 

  5. M. Fuchs.: Experiments in the Heuristic Use of Past Proof Experience. Proc. of CADE-13, New Brunswick, LNAI, 1104:523–537, 1996.

    Google Scholar 

  6. W. McCune: OTTER 3.3 Reference Manual. Argonne National Laboratory, Technical Memorandum No.263, 2003.

    Google Scholar 

  7. E. Alpaydin.: Introduction To Machine Learning. MIT, 2004.

    Google Scholar 

  8. S.J. Russell, P. Norvig, J.F. Canny, J. Malik, and D.D. Edwards.: Artificial Intelligence: A Modern Approach. Prentice Hall, NJ, 1995.

    MATH  Google Scholar 

  9. G. Sutcliffe.: The TPTP Problem Library and Associated Infrastructure: The FOF and CNF Parts, v3.5.0. Journal of Automated Reasoning, 43(4):337–362, 2009.

    Article  MATH  Google Scholar 

  10. C. Goller.: A Connectionist Approach for Learning Search-Control Heuristics for Automated Deduction Systems. PhD Dissertation, Technical University of Munich, 1999.

    MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Boğaziçi University, Bebek, 34342, Istanbul, Turkey

    C. Acar Erkek & Tunga Güngör

Authors
  1. C. Acar Erkek
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Tunga Güngör
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to C. Acar Erkek .

Editor information

Editors and Affiliations

  1. , EEE Dept., Imperial College, Exhibition Road, London, SW72BT, United Kingdom

    Erol Gelenbe

  2. , EEE Dept., Imperial College, Exhibition Rd., London, SW72AZ, United Kingdom

    Ricardo Lent

  3. , EEE Dept., Imperial College, Exhibition Rd., London, SW72AZ, United Kingdom

    Georgia Sakellari

  4. , School of Biomedical Eng., Sci. and Heal, Drexel University, Bossone 702, 3120 Market Street, Philadelphia, 19104, Pennsylvania, USA

    Ahmet Sacan

  5. , Dept. of Computer Engineering, Middle East Technical University, Ankara, 06531, Turkey

    Hakki Toroslu

  6. Fac. Engineering, Dept. Computer Engineering, Middle East Technical University - METU, Ankara, 06531, Turkey

    Adnan Yazici

Rights and permissions

Reprints and permissions

Copyright information

© 2011 Springer Science+Business Media B.V.

About this paper

Cite this paper

Erkek, C.A., Güngör, T. (2011). Using Mixture of Experts Method in Combining Search-Guiding Heuristics for Theorem Proving. In: Gelenbe, E., Lent, R., Sakellari, G., Sacan, A., Toroslu, H., Yazici, A. (eds) Computer and Information Sciences. Lecture Notes in Electrical Engineering, vol 62. Springer, Dordrecht. https://doi.org/10.1007/978-90-481-9794-1_2

Download citation

  • DOI: https://doi.org/10.1007/978-90-481-9794-1_2

  • Published:

  • Publisher Name: Springer, Dordrecht

  • Print ISBN: 978-90-481-9793-4

  • Online ISBN: 978-90-481-9794-1

  • eBook Packages: EngineeringEngineering (R0)

Publish with us

Policies and ethics

Search

Navigation