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 ] } ]