4 ms·
Vulcan: A JavaScript Automated Proof System
- fijal 11y ago"Vulcan" as a name, really? It's a common word, it's already used by one up and coming technology, please be a little more creative (even VulcanJS or VulcanProof, while not very good, would be heaps better)
- amelius 11y agoYou should talk to the creators of the .NET framework.
- RMarcus 11y agoI'll admit I didn't spend a whole lot of time thinking of a name. I was originally going to go with "javascript-resolution-prover", but when I thought of "Vulcan" I thought it was too good not to use. To my great surprise, I don't the name "Vulcan" is being used for any other proof system. A Google search for "Vulcan automated proof" seems to confirm this.
- zvrba 11y agoSo 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.
- RMarcus 11y agoHi everyone, I'm the author. I created this partially to help me understand the concepts in Norvig & Russell's AI book. I plan on using it in a larger project that requires logic-based reasoning after I add in a few search heuristics. The same technique of resolution can pretty easily be applied to first-order logic as well. I think it's a really interesting trick. It's also exciting to see my stuff show up on HN. :)