|
(* Title: Tools/Argo/argo_common.ML
Author: Sascha Boehme
Common infrastructure for the decision procedures of Argo.
*)
signature ARGO_COMMON =
sig
type literal = Argo_Lit.literal * Argo_Proof.proof option
datatype 'a implied = Implied of 'a list | Conflict of Argo_Cls.clause
end
structure Argo_Common: ARGO_COMMON =
struct
type literal = Argo_Lit.literal * Argo_Proof.proof option
(* Implied new knowledge accompanied with an optional proof. If there is no proof,
the literal is to be treated hypothetically. If there is a proof, the literal is
to be treated as uni clause. *)
datatype 'a implied = Implied of 'a list | Conflict of Argo_Cls.clause
(* A result of a step of a decision procedure, either an implication of new knowledge
or clause whose literals are known to be false. *)
end
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
