Correct! Prolog uses a graph-based, backwards chaining algorithm to explore only the needed part of the search space to answer a query. My system explores an ar

Correct! Prolog uses a graph-based, backwards chaining algorithm to explore only the needed part of the search space to answer a query. My system explores an arbitrarily large portion of the search space (possibly all of it, in the case that no proof exists), and can work on any statement in propositional logic, not just horn clauses/definite clauses/goal clauses.