License
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2011.174
URN: urn:nbn:de:0030-drops-32303
URL: http://drops.dagstuhl.de/opus/volltexte/2011/3230/
Go to the corresponding Portal


Czajka, Lukasz

A Semantic Approach to Illative Combinatory Logic

pdf-format:
Document 1.pdf (497 KB)


Abstract

This work introduces the theory of illative combinatory algebras, which is closely related to systems of illative combinatory logic. We thus provide a semantic interpretation for a formal framework in which both logic and computation may be expressed in a unified manner. Systems of illative combinatory logic consist of combinatory logic extended with constants and rules of inference intended to capture logical notions. Our theory does not correspond strictly to any traditional system, but draws inspiration from many. It differs from them in that it couples the notion of truth with the notion of equality between terms, which enables the use of logical formulas in conditional expressions. We give a consistency proof for first-order illative combinatory algebras. A complete embedding of classical predicate logic into our theory is also provided. The translation is very direct and natural.

BibTeX - Entry

@InProceedings{czajka:LIPIcs:2011:3230,
  author =	{Lukasz Czajka},
  title =	{{A Semantic Approach to Illative Combinatory Logic}},
  booktitle =	{Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
  pages =	{174--188},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-32-3},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{12},
  editor =	{Marc Bezem},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2011/3230},
  URN =		{urn:nbn:de:0030-drops-32303},
  doi =		{http://dx.doi.org/10.4230/LIPIcs.CSL.2011.174},
  annote =	{Keywords: illative combinatory logic, term rewriting, first-order logic}
}

Keywords: illative combinatory logic, term rewriting, first-order logic
Seminar: Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL
Issue Date: 2011
Date of publication: 31.08.2011


DROPS-Home | Fulltext Search | Imprint Published by LZI