3 ms·
Doesn't Prolog support only Horn clauses? This proof system supports arbitrary propositions in conjunctive normal form. There are also no quantifiers or predi
by panic 11y ago
Doesn'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.