Universal Quantification and Implication in miniKanren
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 first ~30-40 minutes of the talk will discuss the key ideas behind these goal constructors. The next ~30-40 minutes will cover some of the implementation challenges and performance challenges. We will run some examples to demonstrate performance characteristics. The final ~10-30 minutes will be informal discussions about future work.
Speaker: Lisa Zhang, Ende Jin, Gregory Rosenblatt
Google Meet: https://meet.google.com/myu-dhmz-gvu