Module Fact

module Fact: sig .. end

Representation of derived facts and associated meta information.

type fact

type proof =

`\|`	`BuiltinProof`
`\|`	`InputFactProof`
`\|`	`Proof of Term.term * fact array`
`\|`	`DisjProof of int * Term.term * fact array * fact list`
`\|`	`NegProof of Term.term * fact array * fact`
`\|`	`UnknownProof`

val null_fact : fact

val fact_with_unknown_proof : fact

val make_input_fact : Term.term -> fact

val make_derived_fact : Term.term -> fact

val make_derived_fact_with_proof : Term.term -> proof -> fact

val make_fact_like : fact -> Term.term -> fact

Result is like the given fact, but with the given term.

This interface is required by functions in the Access module.

type entry = fact

val get_term : fact -> Term.term

val get_proof : fact -> proof

A proof term is structured as follows:

node(Id, Goal, Rule, Subproofs, NegativeSubproofs) | split(Id, Rule, Subproofs, NegativeSubproofs) | branch(Id, Goal, Subproof) | ref(Id)

Id is an atom identifying the node.
Goal is the subgoal proven by the node.
Rule is an atom or compound representing the applied deduction rule. It is one of
- builtin - not further specified
- input_fact - an input fact
- hyper(Clause) - hypertableau/resolution inference step with the specified input clause. Clause is given as term.
Subproofs is a list of proof terms. It represents the subproofs used to prove Goal with Rule.
NegativeSubproofs are subproofs that resolve head literals. They could result from negative input literals and complement splitting.
A proof term with node/5 structure represents a proof of Goal by applying Rule to Subproofs and NegativeSubproofs
A proof term with split/4 structure represents a disjunction, that has been derived by applying Rule to Subproofs and NegativeSubproofs.
A proof term with branch/3 structure represents a disjunct contained in the disjunction of the split/4 structure Subproof.
A proof term with ref/1 structure is a reference to the node with the given identifier.

val proof_term_for_fact : Term.symbol_table -> fact -> Term.term

type l_proof = proof list

val proof_term_for_l_proof : Term.symbol_table -> l_proof -> Term.term

val make_subproofs : int -> fact array

type proof_term_aux

val make_proof_term_aux : unit -> proof_term_aux

A proof term aux can be shared in separate calls to proof_term_r_proof, to ensure sharing of subproofs...

val proof_term_for_r_proof : Term.symbol_table -> proof_term_aux -> proof -> Term.term