MaLeS: a framework for automatic tuning of automated theorem provers

DOI10.1007/S10817-015-9329-1MaRDI QIDQ286787zbMATH OpenOpenAlexWikidataFDO

Authors Daniel Kühlwein, Josef Urban

Publication date 26 May 2016

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/1308.2116

zbMATH Keywords

machine learningautomated theorem proversstrategy selection

Mathematics Subject Classification ID

Learning and adaptive systems in artificial intelligence (68T05)

Abstract: MaLeS is an automatic tuning framework for automated theorem provers. It provides solutions for both the strategy finding as well as the strategy scheduling problem. This paper describes the tool and the methods used in it, and evaluates its performance on three automated theorem provers: E, LEO-II and Satallax. An evaluation on a subset of the TPTP library problems shows that on average a MaLeS-tuned prover solves 8.67% more problems than the prover with its default settings.

Recommendations

• E-MaLeS 1.1
• Hierarchical invention of theorem proving strategies
• scientific article; zbMATH DE number 1696564
• scientific article; zbMATH DE number 1612568
• Paramils: an automatic algorithm configuration framework

Cites work

• scientific article; zbMATH DE number 5850137 (Why is no real title available?)
• scientific article; zbMATH DE number 1809861 (Why is no real title available?)
• scientific article; zbMATH DE number 1809862 (Why is no real title available?)
• scientific article; zbMATH DE number 1196643 (Why is no real title available?)
• scientific article; zbMATH DE number 823069 (Why is no real title available?)
• 10.1162/153244303322753616
• An introduction to support vector machines and other kernel-based learning methods.
• Automated deduction -- CADE-24. 24th international conference on automated deduction, Lake Placid, NY, USA, June 9--14, 2013. Proceedings
• Evaluating general purpose automated theorem proving systems
• LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
• Paramils: an automatic algorithm configuration framework
• Pattern recognition and machine learning.
• SATzilla: portfolio-based algorithm selection for SAT
• Satallax: An Automatic Higher-Order Prover
• The CADE-22 automated theorem proving system competition -- CASC-22
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0

Cited in

(4)

• Portfolio theorem proving and prover runtime prediction for geometry
• ENIGMA: efficient learning-based inference guiding machine
• E-MaLeS 1.1
• Hierarchical invention of theorem proving strategies

Describes a project that uses

Uses Software

• PRMLT
• Python
• BliStr
• E-MaLeS
• E Theorem Prover
• Satallax
• SATzilla
• TPTP
• VAMPIRE
• Paramils
• LEO-II

This page was built for publication: MaLeS: a framework for automatic tuning of automated theorem provers

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q286787)