search

gmalecha / mirror-core

A framework for extensible, reflective decision procedures.
Other
19 stars 5 forks source link

KnotProver #18

Closed gmalecha closed 8 years ago

gmalecha commented 10 years ago

The knot prover ties a (bounded) knot between two provers enabling them to call each other.

gmalecha commented 10 years ago

A simple sketch that doesn't have good abstraction: da70da94d4c44a474f930c9e26b0208d28799ef2

The big question is: When should they be able to call each other?

gmalecha commented 9 years ago

It is easy to write this when they don't have associated facts, but it isn't immediately clear how to fit facts into the interface.

gmalecha commented 8 years ago

This code is quite antiquated.