xOur data center is currently experiencing power issues. Our colleagues are working hard to resolve the issue and keep downtime to a minimum.
ICFP 2021
Sun 22 - Sat 28 August 2021
Fri 27 Aug 2021 00:30 - 01:00 at miniKanren - Session B Chair(s): Michael Ballantyne

We present constructive universal quantification and implication in miniKanren using the goal constructors (forall (v) domain goal) and (implies goal goal). Our implementation is capable of solving rudimentary logic problems while reasoning about equality, disequality, type constraints, and user-defined relations. The key idea behind handling a universal quantification (forall (v) domain goal) is to first run (exists (v) (conj domain goal)) to find a state describing some v in the domain that satisfies the goal, then use a relative complement process to generate a goal “relcomp” describing the remaining space of v not covered by that state, and then recursively search (forall (v) (conj relcomp domain) goal). The key idea behind handling an implication (implies A B) is to combine two strategies, depending on the form of A. One strategy follows the classical logic rule that “A implies B” is equivalent to “(not A) or B”, and applies when a goal A is decidable and can easily be negated. The other strategy uses syntactic pattern-matching, and applies when the antecedent goal A calls user-defined relations which match those appearing in the consequent goal B.

Thu 26 Aug

Displayed time zone: Seoul change

23:30 - 01:00
Session BminiKanren at miniKanren
Chair(s): Michael Ballantyne Northeastern University
23:30
30m
Paper
Prolog-Style Meta-Programming miniKanren
miniKanren
Nada Amin Harvard University, William E. Byrd University of Alabama at Birmingham, USA, Tiark Rompf Purdue University
Pre-print Media Attached
00:00
30m
Paper
Guarded Fresh Goals: Dependency-Directed Introduction of Fresh Logic Variables
miniKanren
Evan Donahue University of Tokyo
Pre-print Media Attached
00:30
30m
Paper
Universal Quantification and Implication in miniKanren
miniKanren
Ende Jin , Gregory Rosenblatt University of Alabama at Birmingham, USA, Matthew Might University of Alabama at Birmingham | Harvard Medical School, Lisa Zhang University of Toronto Mississauga
Pre-print Media Attached