Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
History and Prospects for First-Order Automated Deduction Read chapter Read first chapter

2015 | OriginalPaper | Chapter

System Description: E.T. 0.1

Authors : Cezary Kaliszyk, Stephan Schulz, Josef Urban, Jiří Vyskočil

Published in: Automated Deduction - CADE-25

Publisher: Springer International Publishing

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

E.T. 0.1 is a meta-system specialized for theorem proving over large first-order theories containing thousands of axioms. Its design is motivated by the recent theorem proving experiments over the Mizar, Flyspeck and Isabelle data-sets. Unlike other approaches, E.T. does not learn from related proofs, but assumes a situation where previous proofs are not available or hard to get. Instead, E.T. uses several layers of complementary methods and tools with different speed and precision that ultimately select small sets of the most promising axioms for a given conjecture. Such filtered problems are then passed to E, running a large number of suitable automatically invented theorem-proving strategies. On the large-theory Mizar problems, E.T. considerably outperforms E, Vampire, and any other prover that does not learn from related proofs. As a general ATP, E.T. improved over the performance of unmodified E in the combined FOF division of CASC 2014 by 6 %.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now
previous chapter The Lean Theorem Prover (System Description)
next chapter Playing with AVATAR
Footnotes
1
We will use AITP as an abbreviation for the ATP/ITP cooperation, hinting also at the AI aspects of that topic.
 
2
Although never publicly described, similar methods used are one of the main dark sources of Vampire’s success.
 
3
The current limit for formula/clause size is 5kb. This filters out only a few of formulas from the large corpora of interest, and in practice does not influence completeness.
 
4
E.T. runs its strategies sequentially by default. It is also possible to run the strategies, premise selectors, and feature extractors in parallel when more cores are available.
 
5
Parameters are used in the order given above. Missing parameters use E’s built-in default values.
 
Literature
1.
Alama, J., Heskes, T., Kühlwein, D., Tsivtsivadze, E., Urban, J.: Premise selection for mathematics by corpus analysis and kernel methods. J. Autom. Reasoning 52(2), 191–213 (2014)CrossRef
2.
Beeson, M., Wos, L.: OTTER proofs in Tarskian geometry. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS, vol. 8562, pp. 495–510. Springer, Heidelberg (2014)
3.
4.
Cambazoglu, B.B., Zaragoza, H., Chapelle, O., Chen, J., Liao, C., Zheng, Z., Degenhardt, J.: Early exit optimizations for additive machine learned ranking systems. In: Davison, B.D., Suel, T., Craswell, N., Liu, B. (eds.) WSDM, pp. 411–420. ACM, New York (2010)
5.
Chaudhri, V.K., Elenius, D., Goldenkranz, A., Gong, A., Martone, M.E., Webb, W., Yorke-Smith, N.: Comparative analysis of knowledge representation and reasoning requirements across a range of life sciences textbooks. J. Biomed. Semant. 5, 51 (2014)CrossRefMATH
6.
Furbach, U., Glöckner, I., Pelzer, B.: An application of automated reasoning in natural language question answering. AI Commun. 23(2–3), 241–265 (2010)MathSciNetMATH
7.
Hoder, K., Voronkov, A.: Sine Qua Non for large theory reasoning. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol. 6803, pp. 299–314. Springer, Heidelberg (2011) CrossRef
8.
Hoder, K., Voronkov, A.: The 481 ways to split a clause and deal with propositional variables. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol. 7898, pp. 450–464. Springer, Heidelberg (2013) CrossRef
9.
Kaliszyk, C., Urban, J.: MizAR 40 for Mizar 40. CoRR, abs/1310.2805 (2013)
10.
Kaliszyk, C., Urban, J.: Stronger automation for Flyspeck by feature weighting and strategy evolution. In: Blanchette, J.C., Urban, J. (eds.) PxTP 2013, EPiC Series, vol. 14, pp. 87–95. EasyChair (2013)
11.
12.
13.
Kaliszyk, C., Urban, J., Vyskočil, J.: Machine learner for automated reasoning 0.4 and 0.5. CoRR, abs/1402.2359, PAAR 2014 (2014, to appear)
14.
Kaliszyk, C., Urban, J., Vyskočil,J.: Efficient semantic features for automated reasoning over large theories. In: IJCAI (2015, to appear)
15.
Kovács, L., Voronkov, A.: First-order theorem proving and Vampire. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 1–35. Springer, Heidelberg (2013) CrossRef
16.
Kühlwein, D., Blanchette, J.C., Kaliszyk, C., Urban, J.: MaSh: machine learning for Sledgehammer. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 35–50. Springer, Heidelberg (2013) CrossRef
17.
Meng, J., Paulson, L.C.: Lightweight relevance filtering for machine-generated resolution problems. J. Appl. Logic 7(1), 41–57 (2009)MathSciNetCrossRefMATH
18.
Pease, A., Schulz, S.: Knowledge engineering for large ontologies with sigma KEE 3.0. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS, vol. 8562, pp. 519–525. Springer, Heidelberg (2014)
19.
Quaife, A.: Automated Development of Fundamental Mathematical Theories. Kluwer Academic Publishers, Dordrecht (1992)
20.
Schulz, S.: System description: E 1.8. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR-19 2013. LNCS, vol. 8312, pp. 735–743. Springer, Heidelberg (2013) CrossRef
21.
22.
Sutcliffe, G.: The TPTP problem library and associated infrastructure: the FOF and CNF parts, v3.5.0. J. Autom. Reasoning 43(4), 337–362 (2009)CrossRefMATH
23.
Sutcliffe, G.: The 6th IJCAR automated theorem proving system competition - CASC-J6. AI Commun. 26(2), 211–223 (2013)MathSciNetMATH
24.
Sutcliffe, G., Puzis, Y.: SRASS - a semantic relevance axiom selection system. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 295–310. Springer, Heidelberg (2007) CrossRef
25.
Sutcliffe, G., Suda, M., Teyssandier, A., Dellis, N., de Melo, G.: Progress towards effective automated reasoning with world knowledge. In: Guesgen, H.W., Murray, R.C. (eds.) FLAIRS. AAAI Press, Menlo Park (2010)
26.
27.
Urban, J.: MPTP 0.2: design, implementation, and initial experiments. J. Autom. Reasoning 37(1–2), 21–43 (2006)MATH
28.
Urban, J.: BliStr: The Blind Strategymaker. CoRR, abs/1301.2683 (2013)
29.
Urban, J., Hoder, K., Voronkov, A.: Evaluation of automated theorem proving on the Mizar mathematical library. In: Fukuda, K., Hoeven, J., Joswig, M., Takayama, N. (eds.) ICMS 2010. LNCS, vol. 6327, pp. 155–166. Springer, Heidelberg (2010) CrossRef
30.
Voronkov, A.: AVATAR: the architecture for first-order theorem provers. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 696–710. Springer, Heidelberg (2014)
Metadata
Title
System Description: E.T. 0.1
Authors
Cezary Kaliszyk
Stephan Schulz
Josef Urban
Jiří Vyskočil
Copyright Year
2015
Book
Automated Deduction - CADE-25

Print ISBN: 978-3-319-21400-9

Electronic ISBN: 978-3-319-21401-6

Copyright Year: 2015

DOI
https://doi.org/10.1007/978-3-319-21401-6_27

Premium Partner

    Image Credits