A Semantic Approach to Illative Combinatory Logic

Author Lukasz Czajka

Thumbnail PDF


  • Filesize: 496 kB
  • 15 pages

Document Identifiers

Author Details

Lukasz Czajka

Cite AsGet BibTex

Lukasz Czajka. A Semantic Approach to Illative Combinatory Logic. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 174-188, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)


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.
  • illative combinatory logic
  • term rewriting
  • first-order logic


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads