License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license (CC BY-NC-ND 3.0)
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://dagstuhl.sunsite.rwth-aachen.de/volltexte/2011/3230/
Go to the corresponding LIPIcs Volume Portal

Czajka, Lukasz

A Semantic Approach to Illative Combinatory Logic

pdf-format:
17.pdf (0.5 MB)

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 =		{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
Collection: 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 | Privacy Published by LZI