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:
Buchtitelbild

2017 | OriginalPaper | Buchkapitel

A Formal Proof Generator from Semi-formal Proof Documents

verfasst von : Adrián Riesco, Kazuhiro Ogata

Erschienen in: Theoretical Aspects of Computing – ICTAC 2017

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

We present the CafeInMaude Proof Assistant (CiMPA) and the CafeInMaude Proof Generator (CiMPG), two complementary extensions of CafeInMaude, a CafeOBJ interpreter implemented in Maude. CiMPA is a proof assistant for inductive properties of CafeOBJ specifications, and CiMPG generates formal proofs that can be fed into CiMPA from semi-formal proof documents called proof scores in CafeOBJ.

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
Nächstes Kapitel Institutions for Behavioural Dynamic Logic with Binders
Fußnoten
1
Note that so-called open-close environments allows for adding further objects and equations to existing theories.
 
Literatur
1.
Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007). doi:10.​1007/​978-3-540-71999-1 MATH
2.
Clavel, M., Palomino, M., Riesco, A.: Introducing the ITP tool: a tutorial. J. Univ. Comput. Sci. 12(11), 1618–1650 (2006). Programming and Languages. Special Issue with Extended Versions of Selected Papers from PROLE 2005: The 5th Spanish Conference on Programming and Languages
3.
Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C: a software analysis perspective. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) SEFM 2012. LNCS, vol. 7504, pp. 233–247. Springer, Heidelberg (2012). doi:10.​1007/​978-3-642-33826-7_​16 CrossRef
4.
Futatsugi, K.: Generate & check method for verifying transition systems in CafeOBJ. In: De Nicola, R., Hennicker, R. (eds.) Software, Services, and Systems. LNCS, vol. 8950, pp. 171–192. Springer, Cham (2015). doi:10.​1007/​978-3-319-15545-6_​13 CrossRef
5.
6.
Gâinâ, D., Zhang, M., Chiba, Y., Arimoto, Y.: Constructor-based inductive theorem prover. In: Heckel, R., Milius, S. (eds.) CALCO 2013. LNCS, vol. 8089, pp. 328–333. Springer, Heidelberg (2013). doi:10.​1007/​978-3-642-40206-7_​26 CrossRef
7.
Garland, S.J., Guttag, J.V.: LP, the Larch Prover (Version 3.1). MIT Laboratory for Computer Science (1991)
8.
Goguen, J., Winkler, T., Meseguer, J., Futatsugi, K., Jouannaud, J.-P.: Introducing OBJ. Software Engineering with OBJ: Algebraic Specification in Action. Kluwer, Boston (2000)CrossRef
9.
10.
Mossakowski, T., Maeder, C., Codescu, M., Lücke, D.: Hets user guide -version 0.97-. Technical report, DFKI GmbH, Formal Methods for Software Development, February 2011
11.
Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle/HOL: A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)MATH
12.
Ogata, K., Futatsugi, K.: Compositionally writing proof scores of invariants in the OTS/CafeOBJ method. J. UCS 19(6), 771–804 (2013)
13.
Ouranos, I., Ogata, K., Stefaneas, P.S.: TESLA source authentication protocol verification experiment in the timed OTS/CafeOBJ method: experiences and lessons learned. IEICE Trans. 97–D(5), 1160–1170 (2014)CrossRef
14.
Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748–752. Springer, Heidelberg (1992). doi:10.​1007/​3-540-55602-8_​217
15.
Paulson, L.C. (ed.): Isabelle: A Generic Theorem Prover. LNCS, vol. 828. Springer, Heidelberg (1994)MATH
16.
Riesco, A., Ogata, K., Futatsugi, K.: A Maude environment for CafeOBJ. Formal Aspects Comput. 29, 1–26 (2016)MATH
17.
Sawada, T., Futatsugi, K., Preining, N.: CafeOBJ Reference Manual (version 1.5.3), February 2015
Metadaten
Titel
A Formal Proof Generator from Semi-formal Proof Documents
verfasst von
Adrián Riesco
Kazuhiro Ogata
Copyright-Jahr
2017
Buch
Theoretical Aspects of Computing – ICTAC 2017

Print ISBN: 978-3-319-67728-6

Electronic ISBN: 978-3-319-67729-3

Copyright-Jahr: 2017

DOI
https://doi.org/10.1007/978-3-319-67729-3_1