Core.logic – From solving puzzles to finding proofs

Description

For this presentation I want to follow the steps of two books from the The Little Schemer series: The Reasoned Schemer and The Little Prover. The Little Prover examples are build upon J-Bob, a proof assistant based on the ACL2 (A Computational Logic for Applicative Common Lisp”) theorem prover. For this talk I’ll be using a port for clojure made by juxtin, called clj-bob.Logic programming depends on logic variables (or lvars, variables that can take sereval values, but only one at a time), a set of constraints (expressions that limit the values the lvars may assume) and a solution engine in order to find a value that satisfies the logic expression as a whole.The idea is to work on a specific (unsolvable) puzzle from the book GEB (Gödel, Escher, Bach) and work through it on one side from core.logic, using it as a rule system in which we define, declaratively, the rules of the system and try to solve it making attempts to find a value that satisfies this set of rules. On the other side, we will use the proof assistant in order to validate wether the “proof” for this unsolvability is really a proof.

For this talk I’ll be using a port for clojure made by juxtin, called clj-bob.Logic programming depends on logic variables (or lvars, variables that can take sereval values, but only one at a time), a set of constraints (expressions that limit the values the lvars may assume) and a solution engine in order to find a value that satisfies the logic expression as a whole.The idea is to work on a specific (unsolvable) puzzle from the book GEB (Gödel, Escher, Bach) and work through it on one side from core.logic, using it as a rule system in which we define, declaratively, the rules of the system and try to solve it making attempts to find a value that satisfies this set of rules.
On the other side, we will use the proof assistant in order to validate wether the “proof” for this unsolvability is really a proof.


Speakers

Erick Santana
Insatiable learner, solver of puzzles and designer of fun.
I have become passionate about Lisp after reading the article “Beating the Averages”, started to understand it after reading “The Little Schemer” and have used it professionally while working at Nubank.