3 ms·
So this is a basic prolog engine in JS. Still a far shot from what I though it would be from the title, i.e., something like Coq.
by zvrba 11y ago
So this is a basic prolog engine in JS. Still a far shot from what I though it would be from the title, i.e., something like Coq.
- panic 11y agoDoesn't Prolog support only Horn clauses? This proof system supports arbitrary propositions in conjunctive normal form. There are also no quantifiers or predicates here: the logic is purely propositional.
- RMarcus 11y agoCorrect! 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.