Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
MTZ-Fachkongress

Antriebe und Energiesysteme von morgen


Austausch von Automobil- und Energiewirtschaft

Am 14./15. Mai geht es in Chemnitz um die Mobilitätswende durch Elektro- und Wasserstofffahrzeuge.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
A Logical Framework for Developing and Mechanizing Set Theories Kapitel lesen Erstes Kapitel lesen

2016 | OriginalPaper | Buchkapitel

Performance of Clause Selection Heuristics for Saturation-Based Theorem Proving

verfasst von : Stephan Schulz, Martin Möhrmann

Erschienen in: Automated Reasoning

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

We analyze the performance of various clause selection heuristics for saturating first-order theorem provers. These heuristics include elementary first-in/first-out and symbol counting, but also interleaved heuristics and a complex heuristic with goal-directed components.
We can both confirm and dispel some parts of developer folklore. Key results include: (1) Simple symbol counting heuristics beat first-in/first-out, but by a surprisingly narrow margin. (2) Proofs are typically small, not only compared to all generated clauses, but also compared to the number of selected and processed clauses. In particular, only a small number of given clauses (clauses selected for processing) contribute to any given proof. However, the results are extremely diverse and there are extreme outliers. (3) Interleaving selection of the given clause according to different clause evaluation heuristics not only beats the individual elementary heuristics, but also their union - i.e. it shows a synergy not achieved by simple strategy scheduling. (4) Heuristics showing better performance typically achieve a higher ratio of given-clause utilization, but even a fairly small improvement leads to better outcomes. There seems to be a huge potential for further progress.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren
Vorheriges Kapitel Selecting the Selection
Nächstes Kapitel Internal Guidance for Satallax
Fußnoten
1
Status Unknown is assigned to problems which should be provable, but for which no machine proof is known.
 
2
Two trivial syntactic test examples were excluded. They tested floating point syntax features that at the time of the experiments were incorrectly handled by E.
 
Literatur
1.
Bachmair, L., Dershowitz, N., Plaisted, D.: Completion without failure. In: Ait-Kaci, H., Nivat, M. (eds.) Resolution of Equations in Algebraic Structures, vol. 2, pp. 1–30. Academic Press, New York (1989)
2.
Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. J. Log. Comput. 3(4), 217–247 (1994)MathSciNetCrossRefMATH
3.
Denzinger, J., Kronenburg, M., Schulz, S.: DISCOUNT: a distributed and learning equational prover. J. Autom. Reason. 18(2), 189–198 (1997). (Special Issue on the CADE 13 ATP System Competition)CrossRef
4.
Denzinger, J., Schulz, S.: Recording and analysing knowledge-based distributed deduction processes. J. Symb. Comput. 21(4/5), 523–541 (1996)CrossRefMATH
5.
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
6.
Hsiang, J., Rusinowitch, M.: On word problems in equational theories. In: Ottmann, T. (ed.) Automata, Languages and Programming. LNCS, vol. 267, pp. 54–71. Springer, Heidelberg (1987)CrossRef
7.
Knuth, D., Bendix, P.: Simple word problems in universal algebras. In: Leech, J. (ed.) Computational Algebra, pp. 263–297. Pergamon Press, Oxford (1970)
8.
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
9.
Kühlwein, D., van Laarhoven, T., Tsivtsivadze, E., Urban, J., Heskes, T.: Overview and evaluation of premise selection techniques for large theory mathematics. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 378–392. Springer, Heidelberg (2012)CrossRef
10.
Löchner, B., Hillenbrand, T.: A phytography of Waldmeister. J. AI Commun. 15(2/3), 127–133 (2002)MATH
11.
12.
McCune, W.: Otter 3.0 Reference Manual and Guide. Technical report ANL-94/6, Argonne National Laboratory (1994)
13.
McCune, W., Wos, L.: Otter: the CADE-13 competition incarnations. J. Autom. Reason. 18(2), 211–220 (1997). (Special Issue on the CADE 13 ATP System Competition)CrossRef
14.
Meng, J., Paulson, L.C.: Lightweight relevance filtering for machine-generated resolution problems. J. Appl. Log. 7(1), 41–57 (2009)MathSciNetCrossRefMATH
15.
Riazanov, A., Voronkov, A.: The design and implementation of VAMPIRE. J. AI Commun. 15(2/3), 91–110 (2002)MATH
16.
Riazanov, A., Voronkov, A.: Limited resource strategy in resolution theorem proving. J. Symb. Comput. 36(1–2), 101–115 (2003)MathSciNetCrossRefMATH
17.
18.
Schäfer, S., Schulz, S.: Breeding theorem proving heuristics with genetic algorithms. In: Gottlob, G., Sutcliffe, G., Voronkov, A. (eds.) Proceedings of Global Conference on Artificial Intelligence, EPiC, vol. 36, pp. 263–274. EasyChair, Tibilisi, Georgia (2015)
19.
Schulz, S.: E - a brainiac theorem prover. J. AI Commun. 15(2/3), 111–126 (2002)MATH
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.
Stump, A., Sutcliffe, G., Tinelli, C.: StarExec: a cross-community infrastructure for logic solving. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS, vol. 8562, pp. 367–373. Springer, Heidelberg (2014)
22.
Sutcliffe, G.: The TPTP problem library and associated infrastructure: the FOF and CNF parts, v3.5.0. J. Autom.Reason. 43(4), 337–362 (2009)CrossRefMATH
23.
Weidenbach, C., Schmidt, R.A., Hillenbrand, T., Rusev, R., Topic, D.: System description: Spass version 3.0. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 514–520. Springer, Heidelberg (2007)CrossRef
Metadaten
Titel
Performance of Clause Selection Heuristics for Saturation-Based Theorem Proving
verfasst von
Stephan Schulz
Martin Möhrmann
Copyright-Jahr
2016
Buch
Automated Reasoning

Print ISBN: 978-3-319-40228-4

Electronic ISBN: 978-3-319-40229-1

Copyright-Jahr: 2016

DOI
https://doi.org/10.1007/978-3-319-40229-1_23

Premium Partner

    Bildnachweise