eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2011-08-31
174
188
10.4230/LIPIcs.CSL.2011.174
article
A Semantic Approach to Illative Combinatory Logic
Czajka, Lukasz
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol012-csl2011/LIPIcs.CSL.2011.174/LIPIcs.CSL.2011.174.pdf
illative combinatory logic
term rewriting
first-order logic