Confluence of an extension of Combinatory Logic by Boolean constants
{\L}ukasz Czajka
TL;DR
This paper proves the confluence of an extended combinatory logic system with Boolean constants, solving a known open problem and formalized in Coq.
Contribution
It introduces and proves confluence for an extension of Combinatory Logic with Boolean constants, addressing a specific open problem.
Findings
Proves confluence of CL-pc^1 system
Formal proof completed in Coq
Solves problem 15 from RTA list
Abstract
We show confluence of a conditional term rewriting system CL-pc, 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 formalised in the Coq proof assistant.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Logic, Reasoning, and Knowledge · Semantic Web and Ontologies