Previous  Up  Next

Module Reasoner

module Reasoner: sig .. end

Meta-Level reasoner



Meta-level property

A meta-level statement is just a higher-order term.
type term = Libzipperposition.TypedSTerm.t 
type ty = term 
type property = term 
type fact = term 
val property_ty : Libzipperposition.TypedSTerm.t
Type of meta-level statements. All terms used within the meta-prover should have this type
val property_id : Libzipperposition.ID.t

Meta-Level clause

A Horn clause about meta-level properties
exception Error of string
module Clause: sig .. end
type clause = Clause.t

Proofs

Unit-resolution proofs

module Proof: sig .. end
type proof = Proof.t

Consequences

What can be deduced when the Database is updated with new rules and facts.
type consequence = fact * proof

Fact and Rules Database

A database contains a set of Horn-clauses about properties, that allow to reason about them by forward-chaining.

type t
A DB that holds a saturated set of Horn clauses and facts
val empty : t
Empty DB
val add : t -> clause -> t * consequence Sequence.t
Add a clause to the DB, and propagate. See Reasoner.Seq.of_seq for an efficient batch insertion.
val add_fact : t -> fact -> t * consequence Sequence.t
Add a fact to the DB. Sugar for Reasoner.add
module Seq: sig .. end