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
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Quantitative Analysis of Collective Adaptive Systems Kapitel lesen Erstes Kapitel lesen

2016 | OriginalPaper | Buchkapitel

Implementation and Evaluation of Contextual Natural Deduction for Minimal Logic

verfasst von : Bruno Woltzenlogel Paleo

Erschienen in: Perspectives of System Informatics

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

The contextual natural deduction calculus (\({\mathbf{ND }^\mathbf{c }}\)) extends the usual natural deduction calculus (\(\mathbf{ND }\)) by allowing the implication introduction and elimination rules to operate on formulas that occur inside contexts. It has been shown that, asymptotically in the best case, \({\mathbf{ND }^\mathbf{c }}\)-proofs can be quadratically smaller than the smallest \(\mathbf{ND }\)-proofs of the same theorems. In this paper we describe the first implementation of a theorem prover for minimal logic based on \({\mathbf{ND }^\mathbf{c }}\). Furthermore, we empirically compare it to an equally simple \(\mathbf{ND }\) theorem prover on thousands of randomly generated conjectures.

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 Branching Processes of Timed Petri Nets
Nächstes Kapitel Hybrid Lustre
Fußnoten
2
\(\mathrm {depth}(A) = 1\), for an atomic A; \(\mathrm {depth}(B \rightarrow C) = \mathrm {max}(\mathrm {depth}(B), \mathrm {depth}(C)) + 1\).
 
Literatur
1.
Bar-Ilan, O., Fuhrmann, O., Hoory, S., Shacham, O., Strichman, O.: Linear-time reductions of resolution proofs. In: Chockler, H., Hu, A.J. (eds.) HVC 2008. LNCS, vol. 5394, pp. 114–128. Springer, Heidelberg (2009)CrossRef
2.
Böhme, S., Nipkow, T.: Sledgehammer: judgement day. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS, vol. 6173, pp. 107–121. Springer, Heidelberg (2010)CrossRef
3.
Boudou, J., Fellner, A., Woltzenlogel Paleo, B.: Skeptik: a proof compression system. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS, vol. 8562, pp. 374–380. Springer, Heidelberg (2014)
4.
Boudou, J., Woltzenlogel Paleo, B.: Compression of propositional resolution proofs by lowering subproofs. In: Galmiche, D., Larchey-Wendling, D. (eds.) TABLEAUX 2013. LNCS, vol. 8123, pp. 59–73. Springer, Heidelberg (2013)CrossRef
5.
Brünnler, K.: Atomic cut elimination for classical logic. In: Baaz, M., Makowsky, J.A. (eds.) CSL 2003. LNCS, vol. 2803, pp. 86–97. Springer, Heidelberg (2003)CrossRef
6.
Brünnler, K., McKinley, R.: An algorithmic interpretation of a deep inference system. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 482–496. Springer, Heidelberg (2008)CrossRef
7.
8.
Bruscoli, P., Guglielmi, A., Gundersen, T., Parigot, M.: A quasipolynomial cut-elimination procedure in deep inference via atomic flows and threshold formulae. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16 2010. LNCS, vol. 6355, pp. 136–153. Springer, Heidelberg (2010)CrossRef
9.
Cotton, S.: Two techniques for minimizing resolution proofs. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol. 6175, pp. 306–312. Springer, Heidelberg (2010)CrossRef
10.
Deharbe, D., Fontaine, P., Woltzenlogel Paleo, B.: Quantifier inference rules in the proof format of verit. In: 1st International Workshop on Proof Exchange for Theorem Proving (2011)
11.
Delahaye, D., Woltzenlogel Paleo, B. (eds.): All about Proofs, Proofs for All. Mathematical Logic and Foundations, vol. 55. College Publications, London (2015)MATH
12.
Fontaine, P., Merz, S., Woltzenlogel Paleo, B.: Compression of propositional resolution proofs via partial regularization. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol. 6803, pp. 237–251. Springer, Heidelberg (2011)CrossRef
13.
Gentzen, G.: Untersuchungen über das logische Schließen. Mathematische Zeitschrift, vol. 39, pp. 176–210, 405–431 (1934–1935)
14.
Gorzny, J., Woltzenlogel Paleo, B.: Towards the compression of first-order resolution proofs by lowering unit clauses. In: Felty, A.P., Middeldorp, A. (eds.) CADE-25. LNCS, vol. 9195, pp. 356–366. Springer, Switzerland (2015)CrossRef
15.
Guenot, N.: Nested proof search as reduction in the lambda-calculus. In: Schneider-Kamp, P., Hanus, M. (eds.) PPDP, pp. 183–194. ACM (2011)
16.
Guglielmi, A.: A system of interaction and structure. CoRR cs.LO/9910023 (1999)
17.
Hetzl, S., Leitsch, A., Weller, D.: Towards algorithmic cut-introduction. In: Bjørner, N., Voronkov, A. (eds.) LPAR-18 2012. LNCS, vol. 7180, pp. 228–242. Springer, Heidelberg (2012)CrossRef
18.
Hetzl, S., Leitsch, A., Weller, D., Woltzenlogel Paleo, B.: Herbrand sequent extraction. In: Autexier, S., Campbell, J., Rubio, J., Sorge, V., Suzuki, M., Wiedijk, F. (eds.) AISC 2008, Calculemus 2008, and MKM 2008. LNCS (LNAI), vol. 5144, pp. 462–477. Springer, Heidelberg (2008)CrossRef
19.
Woltzenlogel Paleo, B.: Herbrand sequent extraction. M.sc. thesis, Technische Universität Dresden; Technische Universität Wien, Dresden, Germany; Wien, Austria (2007)
20.
Woltzenlogel Paleo, B.: Herbrand Sequent Extraction. VDM-Verlag, Saarbrücken, Germany (2008)MATH
21.
Woltzenlogel Paleo, B.: Contextual natural deduction. In: Artemov, S., Nerode, A. (eds.) LFCS 2013. LNCS, vol. 7734, pp. 372–386. Springer, Heidelberg (2013)CrossRef
22.
23.
Bruttomesso, R., Sharygina, N., Tsitovich, A.: Resolution proof transformation for compression and interpolation. Formal Methods Syst. Des. 45(1), 1–41 (2014)CrossRefMATH
24.
Tiu, A.F.: A local system for intuitionistic logic. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol. 4246, pp. 242–256. Springer, Heidelberg (2006)CrossRef
25.
Woltzenlogel Paleo, B.: A general analysis of cut-elimination by CERES. Ph.D. Dissertation, Vienna University of Technology (2009)
26.
Woltzenlogel Paleo, B.: Atomic cut introduction by resolution: proof structuring and compression. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16 2010. LNCS, vol. 6355, pp. 463–480. Springer, Heidelberg (2010)CrossRef
Metadaten
Titel
Implementation and Evaluation of Contextual Natural Deduction for Minimal Logic
verfasst von
Bruno Woltzenlogel Paleo
Copyright-Jahr
2016
Buch
Perspectives of System Informatics

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

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

Copyright-Jahr: 2016

DOI
https://doi.org/10.1007/978-3-319-41579-6_24