A JavaScript propositional logic and resolution library
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
test
.gitignore
COPYING
LICENSE
README.md
cnf.js
lex.js
package.json
parse.js
util.js
vulcan.js

README.md

Vulcan

Codeship Status for RyanMarcus/vulcan

A library for proving statements in propositional logic using resolution.

Vulcan uses a modified version of the excellent lexer and parse from llang.

For examples, see the tests or this blog post.

Simple usage example

// We are using `const` for imports because the reference will never change.`
// See more here: https://developer.mozilla.org/en-US/docs/Web/JavaScript/Reference/Statements/const

const vulcan = require("vulcan");
const proof = vulcan.prove(["A -> B", // the knowledgebase
                            "B -> C", 
                            "C -> D",
                            "D -> E"],
                            "B -> D"); // the query
                            
console.log(vulcan.isProofComplete(proof)); 
console.log(proof)

Will output:

true
[ { label: 'inital expression', tree: '(A -> B)', idx: 0 },
    { label: 'eliminate implication', tree: '(!A | B)', idx: 1 },
    { label: 'inital expression', tree: '(B -> C)', idx: 2 },
    { label: 'eliminate implication', tree: '(!B | C)', idx: 3 },
    { label: 'inital expression', tree: '(C -> D)', idx: 4 },
    { label: 'eliminate implication', tree: '(!C | D)', idx: 5 },
    { label: 'inital expression', tree: '(D -> E)', idx: 6 },
    { label: 'eliminate implication', tree: '(!D | E)', idx: 7 },
    { label: 'knowledge base clause from 1',
    tree: '(!A | B)',
    idx: 8 },
    { label: 'knowledge base clause from 3',
    tree: '(!B | C)',
    idx: 9 },
    { label: 'knowledge base clause from 5',
    tree: '(!C | D)',
    idx: 10 },
    { label: 'assume for a contradiction', tree: 'B', idx: 12 },
    { label: 'assume for a contradiction', tree: '!D', idx: 13 },
    { label: 'resolve of 9 and 12',
    tree: 'C',
    idx: 22,
    req: [ 9, 12 ] },
    { label: 'resolve of 10 and 13',
    tree: '!C',
    idx: 27,
    req: [ 10, 13 ] },
    { label: 'resolve of 22 and 27',
    tree: false,
    idx: 109,
    req: [ 22, 27 ] } ]