X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Finference.mli;h=4bb43ea8fa2761538273c750d5d7f7896445b0e4;hb=b0db45531321453e765eaeccb1a0b8c774a4d0c1;hp=0ce2e40a6730cd9d1f7703d9539c18bc9094b169;hpb=e61d023695578ebf09d487480e6e7cac3a2dd2ee;p=helm.git diff --git a/helm/ocaml/paramodulation/inference.mli b/helm/ocaml/paramodulation/inference.mli index 0ce2e40a6..4bb43ea8f 100644 --- a/helm/ocaml/paramodulation/inference.mli +++ b/helm/ocaml/paramodulation/inference.mli @@ -9,13 +9,16 @@ type equality = Cic.term list (* arguments *) and proof = + | NoProof | BasicProof of Cic.term | ProofBlock of Cic.substitution * UriManager.uri * + (Cic.name * Cic.term) * Cic.term * (* name, ty, eq_ty, left, right *) - (Cic.name * Cic.term * Cic.term * Cic.term * Cic.term) * - (Utils.pos * equality) * equality - | NoProof +(* (Cic.name * Cic.term * Cic.term * Cic.term * Cic.term) * *) + (Utils.pos * equality) * proof + | ProofGoalBlock of proof * proof (* equality *) + | ProofSymBlock of Cic.term Cic.explicit_named_substitution * proof type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph @@ -64,6 +67,8 @@ exception TermIsNotAnEquality;; val equality_of_term: ?eq_uri:UriManager.uri -> Cic.term -> Cic.term -> equality +val term_is_equality: ?eq_uri:UriManager.uri -> Cic.term -> bool + (** superposition_left env target source returns a list of new clauses inferred with a left superposition step @@ -83,6 +88,8 @@ val equality_of_term: ?eq_uri:UriManager.uri -> Cic.term -> Cic.term -> (* val demodulation: int -> environment -> equality -> equality -> int * equality *) +val meta_convertibility: Cic.term -> Cic.term -> bool + val meta_convertibility_eq: equality -> equality -> bool val is_identity: environment -> equality -> bool @@ -98,5 +105,8 @@ val fix_metas: int -> equality -> int * equality val extract_differing_subterms: Cic.term -> Cic.term -> (Cic.term * Cic.term) option +val build_proof_term: equality -> Cic.term -val build_term_proof: equality -> Cic.term +val find_library_equalities: + dbd:HMysql.dbd -> Cic.context -> ProofEngineTypes.status -> int -> + equality list * int