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:
An Assumption-Based Approach for Solving the Minimal S5-Satisfiability Problem Kapitel lesen Erstes Kapitel lesen

2018 | OriginalPaper | Buchkapitel

From Syntactic Proofs to Combinatorial Proofs

verfasst von : Matteo Acclavio, Lutz Straßburger

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

In this paper we investigate Hughes’ combinatorial proofs as a notion of proof identity for classical logic. We show for various syntactic formalisms including sequent calculus, analytic tableaux, and resolution, how they can be translated into combinatorial proofs, and which notion of identity they enforce. This allows the comparison of proofs that are given in different formalisms.

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 MædMax: A Maximal Ordered Completion Tool
Nächstes Kapitel A Resolution-Based Calculus for Preferential Logics
Fußnoten
1
However, this paper does not speak about normalization of combinatorial proofs. For this topic, the reader is referred to [11, 17, 18].
 
2
Note that this is only a cosmetic limitation. The theory of combinatorial proofs can easily be extended to the full language including implication and general negation.
 
3
It cannot happen that both \(\varGamma \) and \(\varDelta \) are empty.
 
Literatur
1.
Bellin, G., van de Wiele, J.: Subnets of proof-nets in MLL\(^-\). In: Advances in Linear Logic, pp. 249–270. Cambridge University Press (1995)
2.
3.
Cook, S.A., Reckhow, R.A.: The relative efficiency of propositional proof systems. J. Symb. Logic 44(1), 36–50 (1979)MathSciNetCrossRef
4.
Das, A.: On the relative proof complexity of deep inference via atomic flows. Log. Methods Comput. Sci. 11(1), 1–23 (2015)MathSciNetCrossRef
5.
Das, A., Straßburger, L.: On linear rewriting systems for Boolean logic and some applications to proof theory. Log. Methods Comput. Sci. 12(4), 1–27 (2016)MathSciNetMATH
6.
7.
Fitting, M.: First-Order Logic and Automated Theorem Proving. Springer Science & Business Media, Heidelberg (2012)MATH
8.
9.
10.
11.
Hughes, D.: Towards Hilbert’s 24\({}^{\text{ th }}\) problem: combinatorial proof invariants: (preliminary version). Electr. Notes Theor. Comput. Sci. 165, 37–63 (2006)CrossRef
12.
Hughes, D.J.: Unification nets: canonical proof net quantifiers. In: LICS 2018 (2018)
13.
Marin, S., Straßburger, L.: Label-free modular systems for classical and intuitionistic modal logics. In: Advances in Modal Logic 10 (2014)
14.
Retoré, C.: Handsome proof-nets: perfect matchings and cographs. Theor. Comput. Sci. 294(3), 473–488 (2003)MathSciNetCrossRef
15.
Smullyan, R.M.: First-Order Logic. Courier Corporation, Massachusetts (1995)MATH
16.
17.
18.
Straßburger, L.: Combinatorial flows and their normalisation. In: Miller, D. (ed.) FSCD 2017. LIPIcs, vol. 84, pp. 31:1–31:17. Schloss Dagstuhl (2017)
19.
Troelstra, A.S., Schwichtenberg, H.: Basic Proof Theory, vol. 43. Cambridge University Press, Cambridge (2000)CrossRef
Metadaten
Titel
From Syntactic Proofs to Combinatorial Proofs
verfasst von
Matteo Acclavio
Lutz Straßburger
Copyright-Jahr
2018
Buch
Automated Reasoning

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

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

Copyright-Jahr: 2018

DOI
https://doi.org/10.1007/978-3-319-94205-6_32