Soundness and Completeness Proofs by Coinductive Methods

Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel

Research output: Contribution to Journal › Article › Academic › peer-review

Original languageEnglish
Pages (from-to)149-179
JournalJournal of Automated Reasoning
Volume58
Issue number1
DOIs
Publication statusPublished - Jan 2017

Keywords

  • Codatatypes
  • Lazy evaluation
  • First-order logic
  • Soundness
  • Completeness
  • Gentian systems
  • Proof assistants
  • Isabelle/HOL

Cite this

Blanchette, Jasmin Christian ; Popescu, Andrei ; Traytel, Dmitriy. / Soundness and Completeness Proofs by Coinductive Methods. In: Journal of Automated Reasoning. 2017 ; Vol. 58, No. 1. pp. 149-179.
@article{06e97da65455450c96bc1b0c1039c68a,
title = "Soundness and Completeness Proofs by Coinductive Methods",
keywords = "Codatatypes, Lazy evaluation, First-order logic, Soundness, Completeness, Gentian systems, Proof assistants, Isabelle/HOL",
author = "Blanchette, {Jasmin Christian} and Andrei Popescu and Dmitriy Traytel",
year = "2017",
month = "1",
doi = "10.1007/s10817-016-9391-3",
language = "English",
volume = "58",
pages = "149--179",
journal = "Journal of Automated Reasoning",
issn = "0168-7433",
publisher = "Springer Netherlands",
number = "1",

}

Blanchette, JC, Popescu, A & Traytel, D 2017, 'Soundness and Completeness Proofs by Coinductive Methods' Journal of Automated Reasoning, vol. 58, no. 1, pp. 149-179. https://doi.org/10.1007/s10817-016-9391-3

Soundness and Completeness Proofs by Coinductive Methods. / Blanchette, Jasmin Christian; Popescu, Andrei; Traytel, Dmitriy.

In: Journal of Automated Reasoning, Vol. 58, No. 1, 01.2017, p. 149-179.

Research output: Contribution to Journal › Article › Academic › peer-review

TY - JOUR

T1 - Soundness and Completeness Proofs by Coinductive Methods

AU - Blanchette, Jasmin Christian

AU - Popescu, Andrei

AU - Traytel, Dmitriy

PY - 2017/1

Y1 - 2017/1

KW - Codatatypes

KW - Lazy evaluation

KW - First-order logic

KW - Soundness

KW - Completeness

KW - Gentian systems

KW - Proof assistants

KW - Isabelle/HOL

U2 - 10.1007/s10817-016-9391-3

DO - 10.1007/s10817-016-9391-3

M3 - Article

VL - 58

SP - 149

EP - 179

JO - Journal of Automated Reasoning

JF - Journal of Automated Reasoning

SN - 0168-7433

IS - 1

ER -

Blanchette JC, Popescu A, Traytel D. Soundness and Completeness Proofs by Coinductive Methods. Journal of Automated Reasoning. 2017 Jan;58(1):149-179. https://doi.org/10.1007/s10817-016-9391-3

Access to Document