/* tslint:disable */
/* eslint-disable */
/**
* Locate a proof of some composite claims given the provided premises and rules.
*
* ```js
* // (?a, is, awesome) ∧ (?a, score, ?s) -> (?a score, awesome)
* let awesome_score_axiom = {
*     if_all: [
*         [{Unbound: "a"}, {Bound: "is"}, {Bound: "awesome"}, {Bound: "default_graph"}],
*         [{Unbound: "a"}, {Bound: "score"}, {Unbound: "s"}, {Bound: "default_graph"}],
*     ],
*     then: [
*         [{Unbound: "a"}, {Bound: "score"}, {Bound: "awesome"}, {Bound: "default_graph"}]
*     ],
* };
* let proof = prove(
*   [
*      ["you", "score", "unspecified", "default_graph"],
*      ["you", "is", "awesome", "default_graph"],
*   ],
*   [["you", "score", "awesome", "default_graph"]],
*   [awesome_score_axiom],
* );
* expect(proof).to.deep.equal([{
*     rule_index: 0,
*     instantiations: ["you", "unspecified"]
* }])
* ```
* @param {any[]} premises
* @param {any[]} to_prove
* @param {any[]} rules
* @returns {any[]}
*/
export function prove(premises: any[], to_prove: any[], rules: any[]): any[];
/**
* Check is a proof is well-formed according to a ruleset. Returns the set of assumptions used by
* the proof and the set of statements those assumptions imply. If all the assumptions are true,
* then all the implied claims are true under the provided ruleset.
*
* To restate, validating a proof checks whether the proof is valid, but not whether implied
* claims are true. Additional steps need to be performed to ensure the proof is true. You can use
* the following statement to check soundness:
*
* ```customlang
* forall assumed, implied, rules, proof:
*   let { assumed, implied } = validate(rules, proof);
*   If validate() doesn't throw,
*   and all assumed are true
*   and all rules are true
*   then all implied are true
* ```
*
* ```js
* // (?a, is, awesome) ∧ (?a, score, ?s) -> (?a score, awesome)
* let awesome_score_axiom = {
*   if_all: [
*     [{ Unbound: "a" }, { Bound: "is" }, { Bound: "awesome" }, { Bound: "default_graph" }],
*     [{ Unbound: "a" }, { Bound: "score" }, { Unbound: "s" }, { Bound: "default_graph" }],
*   ],
*   then: [
*     [{ Unbound: "a" }, { Bound: "score" }, { Bound: "awesome" }, { Bound: "default_graph" }]
*   ],
* };
* let known_facts = [
*   ["you", "score", "unspecified", "default_graph"],
*   ["you", "is", "awesome", "default_graph"],
* ];
* let valid = validate(
*   [awesome_score_axiom],
*   [{
*     rule_index: 0,
*     instantiations: ["you", "unspecified"]
*   }],
* );
* expect(valid).to.deep.equal({
*   assumed: [
*     ["you", "is", "awesome", "default_graph"],
*     ["you", "score", "unspecified", "default_graph"],
*   ],
*   implied: [
*     ["you", "score", "awesome", "default_graph"],
*   ]
* });
*
* // now we check that all the assumptions made by the proof are known to be true
* for (let f of valid.assumed) {
*   if (!known_facts.some(kf => JSON.stringify(kf) === JSON.stringify(f))) {
*     throw new Error("Proof makes an unverified assumption.");
*   }
* }
*
* // After verifying all the assumptions in the proof are true, we know that the
* // quads in valid.implied are true with respect to the provided rules.
* ```
* @param {any[]} rules
* @param {any[]} proof
* @returns {any}
*/
export function validate(rules: any[], proof: any[]): any;
/**
* Make all possible true inferences given input premises and rules. This is open-ended reasoning.
*
* ```js
* // (?a, is, awesome) ∧ (?a, score, ?s) -> (?a score, awesome)
* let awesome_score_axiom = {
*   if_all: [
*     [{ Unbound: "a" }, { Bound: "is" }, { Bound: "awesome" }, { Bound: "default_graph" }],
*     [{ Unbound: "a" }, { Bound: "score" }, { Unbound: "s" }, { Bound: "default_graph" }],
*   ],
*   then: [
*     [{ Unbound: "a" }, { Bound: "score" }, { Bound: "awesome" }, { Bound: "default_graph" }]
*   ],
* };
* let facts = [
*   ["you", "score", "unspecified", "default_graph"],
*   ["you", "is", "awesome", "default_graph"],
* ];
* let new_facts = infer(facts, [awesome_score_axiom]);
* facts = facts.concat(new_facts);
* expect(facts).to.deep.equal([
*   ["you", "score", "unspecified", "default_graph"],
*   ["you", "is", "awesome", "default_graph"],
*   ["you", "score", "awesome", "default_graph"],
* ]);
* ```
* @param {any[]} premises
* @param {any[]} rules
* @returns {any}
*/
export function infer(premises: any[], rules: any[]): any;