Unified classical logic completeness: a coinductive pearl

Conference paper

Blanchette, J., Popescu, A. and Traytel, D. 2014. Unified classical logic completeness: a coinductive pearl. 7th International Joint Conference on Automated Reasoning (IJCAR). Vienna, Austria 19 - 22 Jul 2014 Springer International Publishing. pp. 46-60
TypeConference paper
TitleUnified classical logic completeness: a coinductive pearl
AuthorsBlanchette, J., Popescu, A. and Traytel, D.
Abstract

Codatatypes are absent from many programming languages and proof assistants. We make a case for their importance by revisiting a classic result: the completeness theorem for first-order logic established through a Gentzen system. The core of the proof establishes an abstract property of possibly infinite derivation trees, independently of the concrete syntax or inference rules. This separation of concerns simplifies the presentation. The abstract proof can be instantiated for a wide range of Gentzen and tableau systems as well as various flavors of first order logic. The corresponding Isabelle/HOL formalization demonstrates the recently introduced support for codatatypes and the Haskell code generator.

Research GroupFoundations of Computing group
Conference7th International Joint Conference on Automated Reasoning (IJCAR)
Page range46-60
ISSN0302-9743
ISBN
Hardcover9783319085869
PublisherSpringer International Publishing
Publication dates
Print2014
Publication process dates
Deposited23 Apr 2015
Output statusPublished
Accepted author manuscript
Copyright Statement

The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-319-08587-6_4

Additional information

Online ISBN: 9783319085876
Published paper appears in: Automated Reasoning, Volume 8562 of the series Lecture Notes in Computer Science, pp 46-60, 2014

Web address (URL)http://dx.doi.org/10.1007/978-3-319-08587-6_4
LanguageEnglish
Book titleAutomated Reasoning: 7th International Joint Conference, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 19-22, 2014. Proceedings
Permalink -

https://repository.mdx.ac.uk/item/851q9

Log in to edit

Download files

Accepted author manuscript
COMPL.pdf

  • 17
    total views
  • 5
    total downloads
  • 0
    views this month
  • 0
    downloads this month

Export as