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:
Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic Kapitel lesen Erstes Kapitel lesen

2017 | Supplement | Buchkapitel

Superposition with Structural Induction

verfasst von : Simon Cruanes

Erschienen in: Frontiers of Combining Systems

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

Superposition-based provers have been successfully used to discharge proof obligations stemming from proof assistants. However, many such obligations require induction to be proved. We present a new extension of typed superposition that can perform structural induction. Several inductive goals can be attempted within a single saturation loop, by leveraging \(\text {AVATAR}\) [1]. Lemmas obtained by generalization or theory exploration can be introduced during search, used, and proved, all in the same search space. We describe an implementation and present some promising results.

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 Solving SAT and MaxSAT with a Quantum Annealer: Foundations and a Preliminary Report
Nächstes Kapitel Subtropical Satisfiability
Fußnoten
1
It might even induce rewriting loops in some cases where the term ordering used by superposition and the rewrite system are not compatible. In our experience this does not seem to happen often.
 
2
Our framework allows attempting to prove several distinct inductive goals to solve a single subgoal.
 
3
 
4
Commit 187b71af8d920d0634b2b8b34c4ac4834b2f6a94 at https://​github.​com/​tip-org/​benchmarks.
 
5
Experiments on TPTP were run on a 2.20 GHz Intel \(\text {Xeon}^\circledR \) CPU with 30 s timeout and a memory limit of 2 GB.
 
Literatur
1.
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, Cham (2014). doi:10.​1007/​978-3-319-08867-9_​46
2.
Paulson, L.C., Blanchette, J.C.: Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers. In: Sutcliffe, G., Schulz, S., Ternovska, E. (eds.) IWIL 2010, EasyChair (2012)
3.
4.
Schulz, S.: E - a brainiac theorem prover. AI Commun. 15, 111–126 (2002)MATH
5.
Riazanov, A., Voronkov, A.: Vampire 1.1 (system description). In: Goré, R., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS, vol. 2083, pp. 376–380. Springer, Heidelberg (2001). doi:10.​1007/​3-540-45744-5_​29 CrossRef
6.
Weidenbach, C., Schmidt, R.A., Hillenbrand, T., Rusev, R., Topic, D.: System Description: Spass Version 3.0. In: Pfenning, F. (ed.) CADE 2007. LNCS, vol. 4603, pp. 514–520. Springer, Heidelberg (2007). doi:10.​1007/​978-3-540-73595-3_​38 CrossRef
7.
Bachmair, L., Ganzinger, H.: On restrictions of ordered paramodulation with simplification. In: Stickel, M.E. (ed.) CADE 1990. LNCS, vol. 449, pp. 427–441. Springer, Heidelberg (1990). doi:10.​1007/​3-540-52885-7_​105 CrossRef
8.
Kovács, L., Robillard, S., Voronkov, A.: Coming to terms with quantified reasoning. In: Castagna, G., Gordon, A.D. (eds.) POPL 2017, pp. 260–270. ACM (2017)
9.
Kaufmann, M., Moore, J.S.: ACL2: an industrial strength version of Nqthm. In: Computer Assurance, COMPASS 1996, pp. 23–34. IEEE (1996)
10.
Biundo, S., Hummel, B., Hutter, D., Walther, C.: The karlsruhe induction theorem proving system. In: Siekmann, J.H. (ed.) CADE 1986. LNCS, vol. 230, pp. 672–674. Springer, Heidelberg (1986). doi:10.​1007/​3-540-16780-3_​132 CrossRef
11.
Stratulat, S.: A unified view of induction reasoning for first-order logic. In: Turing-100, The Alan Turing Centenary Conference (2012)
12.
Reynolds, A., Kuncak, V.: Induction for SMT solvers. In: D’Souza, D., Lal, A., Larsen, K.G. (eds.) VMCAI 2015. LNCS, vol. 8931, pp. 80–98. Springer, Heidelberg (2015). doi:10.​1007/​978-3-662-46081-8_​5
13.
Kersani, A., Peltier, N.: Combining superposition and induction: a practical realization. In: Fontaine, P., Ringeissen, C., Schmidt, R.A. (eds.) FroCoS 2013. LNCS, vol. 8152, pp. 7–22. Springer, Heidelberg (2013). doi:10.​1007/​978-3-642-40885-4_​2 CrossRef
14.
Beeson, M.: Otter-lambda, a Theorem-prover with Untyped Lambda-unification. In: Proceedings of the Workshop on Empirically Successful First Order Reasoning, 2nd International Joint Conference on Automated Reasoning (2004)
15.
16.
Riazanov, A., Voronkov, A.: Splitting without backtracking (2001)
17.
Claessen, K., Johansson, M., Rosén, D., Smallbone, N.: TIP: tons of inductive problems. In: Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V. (eds.) CICM 2015. LNCS, vol. 9150, pp. 333–337. Springer, Cham (2015). doi:10.​1007/​978-3-319-20615-8_​23 CrossRef
18.
Bundy, A., Stevens, A., van Harmelen, F., Ireland, A., Smaill, A.: Rippling: a heuristic for guiding inductive proofs. Artif. Intell. 62(2), 185–253 (1993)MathSciNetCrossRefMATH
19.
Boyer, R.S., Moore, J.S.: A Computational Logic Handbook: Formerly Notes and Reports in Computer Science and Applied Mathematics. Elsevier, San Diego (2014)
20.
Kapur, D., Subramaniam, M.: Lemma discovery in automating induction. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol. 1104, pp. 538–552. Springer, Heidelberg (1996). doi:10.​1007/​3-540-61511-3_​112
21.
Aubin, R.: Strategies for mechanizing structural induction. In: IJCAI (1977)
22.
23.
24.
25.
26.
27.
Barrett, C., Shikanian, I., Tinelli, C.: An abstract decision procedure for satisfiability in the theory of inductive data types. J. Satisf. Boolean Model. Comput. 3, 21–46 (2007)MathSciNetMATH
28.
29.
Horbach, M., Weidenbach, C.: Superposition for fixed domains. ACM Trans. Comput. Log. (TOCL) 11(4), 27 (2010)MathSciNetMATH
30.
Zhang, H., Kapur, D., Krishnamoorthy, M.S.: A mechanizable induction principle for equational specifications. In: Lusk, E., Overbeek, R. (eds.) CADE 1988. LNCS, vol. 310, pp. 162–181. Springer, Heidelberg (1988). doi:10.​1007/​BFb0012831 CrossRef
31.
Claessen, K., Johansson, M., Rosén, D., Smallbone, N.: Hipspec: automating inductive proofs of program properties. In: ATx/WInG@ IJCAR (2012)
32.
Runciman, C., Naylor, M., Lindblad, F.: Smallcheck and lazy smallcheck: automatic exhaustive testing for small values. ACM Sigplan Not. 44, 37–48 (2008)CrossRef
33.
Claessen, K., Hughes, J.: QuickCheck: a lightweight tool for random testing of Haskell programs. ACM Sigplan Not. 46(4), 53–64 (2011)CrossRef
34.
Lindblad, F.: Property directed generation of first-order test data. In: Trends in Functional Programming, pp. 105–123, Citeseer (2007)
35.
Cruanes, S.: Extending superposition with integer arithmetic, structural induction, and beyond. Ph.D. thesis, École polytechnique, September 2015
36.
Kotelnikov, E., Kovács, L., Reger, G., Voronkov, A.: The Vampire and the FOOL. In: Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, pp. 37–48. ACM (2016)
37.
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
38.
Metadaten
Titel
Superposition with Structural Induction
verfasst von
Simon Cruanes
Copyright-Jahr
2017
Buch
Frontiers of Combining Systems

Print ISBN: 978-3-319-66166-7

Electronic ISBN: 978-3-319-66167-4

Copyright-Jahr: 2017

DOI
https://doi.org/10.1007/978-3-319-66167-4_10

Premium Partner

    Bildnachweise