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 1/2017

18.10.2016

Soundness and Completeness Proofs by Coinductive Methods

verfasst von: Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel

Erschienen in: Journal of Automated Reasoning | Ausgabe 1/2017

Einloggen

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

search-config
loading …

Abstract

We show how codatatypes can be employed to produce compact, high-level proofs of key results in logic: the soundness and completeness of proof systems for variations of first-order logic. For the classical completeness result, we first establish an abstract property of possibly infinite derivation trees. The abstract proof can be instantiated for a wide range of Gentzen and tableau systems for various flavors of first-order logic. Soundness becomes interesting as soon as one allows infinite proofs of first-order formulas. This forms the subject of several cyclic proof systems for first-order logic augmented with inductive predicate definitions studied in the literature. All the discussed results are formalized using Isabelle/HOL’s recently introduced support for codatatypes and corecursion. The development illustrates some unique features of Isabelle/HOL’s new coinductive specification language such as nesting through non-free types and mixed recursion–corecursion.
Vorheriger Artikel An Approximation Framework for Solvers and Decision Procedures
Nächster Artikel Finding Proofs in Tarskian Geometry

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
Given formulas \(\psi _1,\ldots ,\psi _k\), we let \({\textsf {Conj}}\;\psi _1\;\ldots \;\psi _k\) denote \({\textsf {Conj}}\;\psi _1\;({\textsf {Conj}}\;\psi _2\;(\ldots \psi _n)\ldots )\). In particular, when \(k = 0\) it denotes the “true” formula \(\top \), defined in a standard way, e.g., as \({\textsf {Imp}}\;a\;a\) for some atom a.
 
2
This is acceptable here, since we employ finitary Horn clauses and the language is countable. Different assumptions may require larger ordinals.
 
3
The definition of \(P_{p,\_}\) works with the original clauses \(\chi \in {\textsf {ind}}_p\), whereas here we apply it to the “copies” \(\chi '\) of \(\chi \) guaranteed to have their variables fresh for \(\Gamma \) and \(\Delta \), as stipulated in the \(p_{\mathrm{split}}\) rule. This is unproblematic, since it is easy to verify that the definition of \(P_{p,\_}\) is invariant under bijective renaming of variables in the clauses \(\chi \).
 
4
Goodness is decidable for cyclic trees in logics where rule application is decidable, such as FOL\(_{\textsf {ind}}\) [16].
 
5
In the proof system from Example 2, \({\textsf {eff}}\) is not deterministic due to the rule All R. It can be made deterministic by refining the rule with a systematic choice of the fresh variable y.
 
6
And Kripke’s degree of rigor in this early article is not far from today’s state of the art in proof theory; see, e.g., Troelstra and Schwichtenberg [51].
 
7
This is the only error we found in this otherwise excellent chapter on tableaux.
 
Literatur
1.
Bell, J.L., Machover, M.: A Course in Mathematical Logic. North-Holland, Amsterdam (1977)MATH
2.
3.
Bertot, Y.: Filters on coinductive streams, an application to Eratosthenes’ sieve. In: Urzyczyn, P. (ed.) TLCA 2005, LNCS, vol. 3461, pp. 102–115. Springer (2005)
4.
Blanchette, J.C., Böhme, S., Popescu, A., Smallbone, N.: Encoding monomorphic and polymorphic types. In: Piterman, N., Smolka, S. (eds.) TACAS 2013, LNCS, vol. 7795, pp. 493–507. Springer (2013)
5.
Blanchette, J.C., Fleury, M., Weidenbach, C.: A verified SAT solver framework with learn, forget, restart, and incrementality. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016, LNCS, vol. 9706. Springer (2016)
6.
Blanchette, J.C., Hölzl, J., Lochbihler, A., Panny, L., Popescu, A., Traytel, D.: Truly modular (co)datatypes for Isabelle/HOL. In: Klein, G., Gamboa, R. (eds.) ITP 2014, LNCS, vol. 8558, pp. 93–110. Springer (2014)
7.
Blanchette, J.C., Popescu, A.: Mechanizing the metatheory of Sledgehammer. In: Fontaine, P., Ringeissen, C., Schmidt, R.A. (eds.) FroCoS 2013, LNCS, vol. 8152, pp. 245–260. Springer (2013)
8.
9.
Blanchette, J.C., Popescu, A., Traytel, D.: Unified classical logic completeness—a coinductive pearl. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014, LNCS, vol. 8562, pp. 46–60. Springer (2014)
10.
11.
Blanchette, J.C., Popescu, A., Traytel, D.: Foundational extensible corecursion: a proof assistant perspective. In: Fisher, K., Reppy, J.H. (eds.) ICFP 2015, pp. 192–204. ACM (2015)
12.
Brotherston, J.: Cyclic proofs for first-order logic with inductive definitions. In: Beckert, B. (ed.) TABLEAUX 2005, LNCS, vol. 3702, pp. 78–92. Springer (2005)
13.
Brotherston, J.: Sequent calculus proof systems for inductive definitions. Ph.D. thesis, University of Edinburgh (2006)
14.
Brotherston, J., Bornat, R., Calcagno, C.: Cyclic proofs of program termination in separation logic. In: Necula, G.C., Wadler, P. (eds.) POPL 2008, pp. 101–112. ACM (2008)
15.
Brotherston, J., Distefano, D., Petersen, R.L.: Automated cyclic entailment proofs in separation logic. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE-23, LNCS, vol. 6803, pp. 131–146. Springer (2011)
16.
Brotherston, J., Gorogiannis, N., Petersen, R.L.: A generic cyclic theorem prover. In: Jhala, R., Igarashi, A. (eds.) APLAS 2012, LNCS, vol. 7705, pp. 350–367. Springer (2012)
17.
Brotherston, J., Simpson, A.: Complete sequent calculi for induction and infinite descent. In: LICS 2007, pp. 51–62. IEEE Computer Society (2007)
18.
Ciaffaglione, A., Gianantonio, P.D.: A certified, corecursive implementation of exact real numbers. Theor. Comput. Sci. 351(1), 39–51 (2006)MathSciNetCrossRefMATH
19.
Diaconescu, R.: Institution-Independent Model Theory. Studies in Universal Logic. Birkhäuser, Basel (2008)MATH
20.
Fitting, M.: First-Order Logic and Automated Theorem Proving. Graduate Texts in Computer Science, 2nd edn. Springer, Berlin (1996)CrossRefMATH
21.
Francez, N.: Fairness. Texts and Monographs in Computer Science. Springer, Berlin (1986)
22.
Gallier, J.H.: Logic for Computer Science: Foundations of Automatic Theorem Proving. Computer Science and Technology. Harper & Row, New York (1986)MATH
23.
Gödel, K.: Über die Vollständigkeit des Logikkalküls. Ph.D. thesis, Universität Wien (1929)
24.
Gordon, M.J.C., Melham, T.F. (eds.): Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, Cambridge (1993)MATH
25.
Haftmann, F., Nipkow, T.: Code generation via higher-order rewrite systems. In: Blume, M., Kobayashi, N., Vidal, G. (eds.) FLOPS 2010, LNCS, vol. 6009, pp. 103–117. Springer (2010)
26.
Hähnle, R.: Tableaux and related methods. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. I, pp. 100–178. Elsevier, Amsterdam (2001)
27.
Harrison, J.: Formalizing basic first order model theory. In: Grundy, J., Newey, M.C. (eds.) TPHOLs ’98, LNCS, vol. 1479, pp. 153–170. Springer (1998)
28.
Ilik, D.: Constructive completeness proofs and delimited control. Ph.D. thesis, École polytechnique (2010)
29.
Jacobs, B., Rutten, J.: A tutorial on (co)algebras and (co)induction. Bull. Eur. Assoc. Theor. Comput. Sci. 62, 222–259 (1997)MATH
30.
Kaplan, D.: Review of Kripke (1959) [32]. J. Symb. Log. 31, 120–122 (1966)
31.
Kleene, S.C.: Mathematical Logic. Wiley, London (1967)MATH
32.
33.
Krivine, J.L.: Une preuve formelle et intuitionniste du théorème de complétude de la logique classique. Bull. Symb. Log. 2(4), 405–421 (1996)CrossRef
34.
35.
36.
Nakata, K., Uustalu, T., Bezem, M.: A proof pearl with the fan theorem and bar induction: walking through infinite trees with mixed induction and coinduction. In: Yang, H. (ed.) APLAS 2011, LNCS, vol. 7078, pp. 353–368. Springer (2011)
37.
Negri, S.: Kripke completeness revisited. In: Primiero, G., Rahman, S. (eds.) Acts of Knowledge: History, Philosophy and Logic: Essays Dedicated to Göran Sundholm, pp. 247–282. College Publications, London (2009)
38.
Nipkow, T., Klein, G.: Concrete Semantics: With Isabelle/HOL. Springer, Berlin (2014)CrossRefMATH
39.
Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: A Proof Assistant for Higher-Order Logic, LNCS, vol. 2283. Springer (2002)
40.
Petria, M.: An institutional version of Gödel’s completeness theorem. In: CALCO 2007, pp. 409–424 (2007)
41.
Pfenning, F.: Review of “Jean H. Gallier: Logic for Computer Science, Harper & Row, New York 1986” [22]. J. Symb. Log. 54(1), 288–289 (1989)
42.
Ridge, T., Margetson, J.: A mechanically verified, sound and complete theorem prover for first order logic. In: Hurd, J., Melham, T.F. (eds.) TPHOLs 2005, LNCS, vol. 3603, pp. 294–309. Springer (2005)
43.
Roşu, G.: Equality of streams is a \(\Pi _2^0\)-complete problem. In: Reppy, J.H., Lawall, J.L. (eds.) ICFP ’06. ACM (2006)
44.
Roşu, G.: An effective algorithm for the membership problem for extended regular expressions. In: Seidl, H. (ed.) FoSSaCS 2007, LNCS, vol. 4423, pp. 332–345. Springer (2007)
45.
Rutten, J.J.M.M.: Automata and coinduction (an exercise in coalgebra). In: Sangiorgi, D., de Simone, R. (eds.) CONCUR ’98, LNCS, vol. 1466, pp. 194–218. Springer (1998)
46.
Rutten, J.J.M.M.: Regular expressions revisited: a coinductive approach to streams, automata, and power series. In: Backhouse, R.C., Oliveira, J.N. (eds.) MPC 2000, LNCS, vol. 1837, pp. 100–101. Springer (2000)
47.
Rutten, J.J.M.M.: Elements of stream calculus (an extensive exercise in coinduction). Electron. Notes Theor. Comput. Sci. 45, 358–423 (2001)CrossRefMATH
48.
Schlichtkrull, A.: Formalization of the resolution calculus for first-order logic. In: Blanchette, J.C., Merz, S. (eds.) ITP 2016, LNCS, vol. 9807. Springer (2016)
49.
Schlöder, J.J., Koepke, P.: The Gödel completeness theorem for uncountable languages. Formaliz. Math. 20(3), 199–203 (2012)MATH
50.
Traytel, D., Popescu, A., Blanchette, J.C.: Foundational, compositional (co)datatypes for higher-order logic: category theory applied to theorem proving. In: LICS 2012, pp. 596–605. IEEE Computer Society (2012)
51.
Troelstra, A.S., Schwichtenberg, H.: Basic Proof Theory, 2nd edn. Cambridge University Press, Cambridge (2000)CrossRefMATH
Metadaten
Titel
Soundness and Completeness Proofs by Coinductive Methods
verfasst von
Jasmin Christian Blanchette
Andrei Popescu
Dmitriy Traytel
Publikationsdatum
18.10.2016
Verlag
Springer Netherlands
Erschienen in
Journal of Automated Reasoning / Ausgabe 1/2017
Print ISSN: 0168-7433
Elektronische ISSN: 1573-0670
DOI
https://doi.org/10.1007/s10817-016-9391-3

Weitere Artikel der Ausgabe 1/2017

Journal of Automated Reasoning 1/2017 Zur Ausgabe

EditorialNotes

Preface

OriginalPaper

The Bayesian Ontology Language

OriginalPaper

Automatically Proving Termination and Memory Safety for Programs with Pointer Arithmetic

OriginalPaper

Solution Validation and Extraction for QBF Preprocessing

OriginalPaper

Finding Proofs in Tarskian Geometry

OriginalPaper

An Approximation Framework for Solvers and Decision Procedures