2026-07-20T09:01:05Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:7736 2024-03-06T10:41:02Z ddc:004 open_access

Confluence of an Extension of Combinatory Logic by Boolean Constants Czajka, Lukasz combinatory logic conditional linearization unique normal form property confluence We show confluence of a conditional term rewriting system CL-pc^1, which is an extension of Combinatory Logic by Boolean constants. This solves problem 15 from the RTA list of open problems. The proof has been fully formalized in the Coq proof assistant. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Lukasz Czajka 2017 Is Part Of LIPIcs, Volume 84, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2017.14 urn:nbn:de:0030-drops-77368 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.14 eng https://creativecommons.org/licenses/by/3.0/legalcode