Propagator Networks for Unification and Proof Search

Arved Friedemann

Logical languages have often shown to be useful as they give compact code for a huge variety of search problems. However, their performance highly depends on the underlying search engine. In a different branch of Theoretical Computer Science, something called Propagator Networks have been developed that combine the principles of SAT , SMT and CSP solvers all in one formalism. These networks can be used to get a general notion of what unit propagation means for more than just boolean functions and they can be easily parallelised. Here, we present a framework for Propagator Networks that can be used to easily model unification and branching and create a logical language to perform proof search for PROLOG-like languages.

 Overview  Program