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
Journal of Automated Reasoning
Erschienen in: Journal of Automated Reasoning 3/2016

01.10.2016

Proof Generalization in \(\mathrm {LK}\) by Second Order Unifier Minimization

verfasst von: Thierry Boy de la Tour, Nicolas Peltier

Erschienen in: Journal of Automated Reasoning | Ausgabe 3/2016

Einloggen

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

search-config
loading …

Abstract

We devise a method for generalizing proofs in Gentzen’s sequent calculus \(\mathrm {LK}\), presented in a typed \(\lambda \)-calculus flavor. A constrained version \(\mathrm {LK}^{{{\mathrm {c}}}}\) of the calculus is introduced, aiming at collecting a second order constraint ensuring that all the inference steps occurring in a proof are syntactically correct. A semantics is provided for \(\mathrm {LK}^{{{\mathrm {c}}}}\), extending the standard semantics of \(\mathrm {LK}\). It is then established that \(\mathrm {LK}\)-proofs correspond to \(\mathrm {LK}^{{{\mathrm {c}}}}\)-proofs with valid constraint thanks to the use of eigenterms replacing \(\mathrm {LK}\)’s eigenvariables. Next, a lifting theorem shows how a valid \(\mathrm {LK}^{{{\mathrm {c}}}}\)-proof can be lifted to a most general proof, yielding a non-trivial constraint together with a solution. An algorithm is then provided that minimizes this solution of the constraint. The result, applied to the most general proof, yields a valid proof that translates to an \(\mathrm {LK}\)-proof more general than the initial one. Finally, clues are given for extending this method to other logics with due care on proof lifting.
Vorheriger Artikel A Learning-Based Fact Selector for Isabelle/HOL

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 "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

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
Fußnoten
1
Formal definitions are given in Sect. 2, see in particular Fig. 1 for the inference rules.
 
2
We assume w.l.o.g. that \(D \cap (\mathcal {C}\cup \mathcal {V})= \emptyset \) and that D contains no non-atomic terms in \(\mathcal {T}_D\).
 
3
More precisely on a special kind of formulæ called “matrices”.
 
4
Note that the \(\mathcal {X}_i\)’s are not part of these meta-variables.
 
5
In all rigor the same should be done in [13] for the (\(\Rightarrow \)-L) rule from [25].
 
6
These constants cannot be generalized simply because there is no variable of the corresponding types. The equality predicate could be generalized if its specific properties are not used in the proof, i.e., if no paramodulation inference is applied on it. Of course, if no \(\wedge \)-rule is applied on a formula \((\wedge \;t_1\, t_2)\) then it can be generalized by a variable of type \(\mathbf {o}\).
 
7
In particular, if \(v\in \{\forall ,\exists \}\) then \(m=1\) and \(z_1\) has type \({\varvec{\i }}^{n+1}\rightarrow \mathbf {o}\). If v is a binary connective then \(m=2\) since t has \(\mathcal {V}\)-type.
 
8
Another way to do this is to allow principal formulæ to occur anywhere in the conclusions of the rules. For instance, the (\(\lnot \)-L) rule would be \(\displaystyle \frac{\varGamma ,\varSigma \vdash \varDelta ,\phi }{\varGamma ,\lnot \phi ,\varSigma \vdash \varDelta }.\)
 
Literatur
1.
2.
3.
Caferra, R., Zabel, N.: Building models by using tableaux extended by equational problems. J. Log. Comput. 3, 3–25 (1993)CrossRef
4.
Cavagnetto, S.: The lengths of proofs: Kreisel’s conjecture and Gödel’s speed-up theorem. J. Math. Sci. 158(5), 689–707 (2009)MathSciNetMATHCrossRef
5.
Dowek, G.: Higher-order unification and matching. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, Volume II, Chapter 16, pp. 1009–1062. Elsevier Science, New York (2001)CrossRef
6.
7.
Farmer, W.M.: A unification-theoretic method for investigating the \(k\)-provability problem. Ann. Pure Appl. Log. 51(3), 173–214 (1991)MathSciNetMATHCrossRef
8.
Felty, A.P., Howe, D.J.: Generalization and reuse of tactic proofs. In: Pfenning, F. (eds.) LPAR, Volume 822 of Lecture Notes in Computer Science, pp. 1–15. Springer, Berlin (1994)
9.
Giese, M.: Incremental closure of free variable tableaux. In Goré, R., Leitsch, A., Nipkow, T. (eds.) Proceedings of International Joint Conference on Automated Reasoning, Siena, Italy, number 2083 in LNCS, pp. 545–560. Springer (2001)
10.
Hagiya, M.: A typed lambda-calculus for proving-by-example and bottom-up generalization procedure. Theor. Comput. Sci. 137(1), 3–23 (1995)MathSciNetMATHCrossRef
11.
Hetzl, S.: A sequent calculus with implicit term representation. In Dawar, A., Veith, H. (eds.) Computer Science Logic, volume 6247 of Lecture Notes in Computer Science, pp. 351–365. Springer, Berlin (2010)
12.
Johnsen, E.B., Lüth, C.: Theorem reuse by proof term transformation. In: Slind, K., Bunker, A., Gopalakrishnan, G. (eds.) TPHOLs, volume 3223 of Lecture Notes in Computer Science, pp. 152–167. Springer (2004)
13.
Krajíček, J., Pudlák, P.: The number of proof lines and the size of proofs in first order logic. Arch. Math. Log. 27, 69–84 (1988)MathSciNetMATHCrossRef
14.
15.
16.
Miller, D.: Proofs in Higher-Order Logic. PhD thesis, Carnegie-Mellon University (1983). Technical report: MS-CIS-83-37
17.
18.
19.
Moser, G., Zach, R.: The epsilon calculus (tutorial). In: Baaz, M., Makowsky, J.A. (eds.) Computer Science Logic, 17th International Workshop, CSL 2003, 12th Annual Conference of the EACSL, and 8th Kurt Gödel Colloquium, KGC 2003, Vienna, Austria, August 25–30, 2003, Proceedings, volume 2803 of Lecture Notes in Computer Science, p. 455. Springer, (2003)
20.
21.
22.
23.
Pfenning, F.: Unification and anti-unification in the calculus of constructions. In: Proceedings of Sixth Annual IEEE Symposium on Logic in Computer Science, 1991. LICS ’91, pp. 74–85 (1991)
24.
Rümmer, P.: A constraint sequent calculus for first-order logic with linear integer arithmetic. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning, volume 5330 of Lecture Notes in Computer Science, pp. 274–289. Springer, Berlin (2008)
25.
Takeuti, G.: Proof Theory, 2nd edn. North Holland, New York (1987)MATH
26.
27.
Zach, R.: The practice of finitism: epsilon calculus and consistency proofs in Hilbert’s program. Synthese 137(1–2), 211–259 (2003)MathSciNetCrossRef
Metadaten
Titel
Proof Generalization in by Second Order Unifier Minimization
verfasst von
Thierry Boy de la Tour
Nicolas Peltier
Publikationsdatum
01.10.2016
Verlag
Springer Netherlands
Erschienen in
Journal of Automated Reasoning / Ausgabe 3/2016
Print ISSN: 0168-7433
Elektronische ISSN: 1573-0670
DOI
https://doi.org/10.1007/s10817-016-9367-3

Premium Partner

    Bildnachweise