isabelle: src/Tools/Metis/src/Normalize.sig@913162a47d9f (annotated)

39348 6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	1	(* ========================================================================= *)
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	2	(* NORMALIZING FORMULAS *)
72004 913162a47d9f Update Metis to 2.4 desharna parents: 39502 diff changeset	3	(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
39348 6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	4	(* ========================================================================= *)
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	5
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	6	signature Normalize =
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	7	sig
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	8
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	9	(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	10	(* Negation normal form. *)
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	11	(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	12
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	13	val nnf : Formula.formula -> Formula.formula
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	14
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	15	(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	16	(* Conjunctive normal form derivations. *)
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	17	(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	18
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	19	type thm
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	20
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	21	datatype inference =
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	22	Axiom of Formula.formula
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	23	\| Definition of string * Formula.formula
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	24	\| Simplify of thm * thm list
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	25	\| Conjunct of thm
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	26	\| Specialize of thm
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	27	\| Skolemize of thm
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	28	\| Clausify of thm
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	29
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	30	val mkAxiom : Formula.formula -> thm
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	31
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	32	val destThm : thm -> Formula.formula * inference
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	33
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	34	val proveThms :
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	35	thm list -> (Formula.formula * inference * Formula.formula list) list
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	36
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	37	val toStringInference : inference -> string
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	38
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	39	val ppInference : inference Print.pp
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	40
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	41	(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	42	(* Conjunctive normal form. *)
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	43	(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	44
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	45	type cnf
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	46
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	47	val initialCnf : cnf
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	48
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	49	val addCnf : thm -> cnf -> (Thm.clause * thm) list * cnf
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	50
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	51	val proveCnf : thm list -> (Thm.clause * thm) list
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	52
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	53	val cnf : Formula.formula -> Thm.clause list
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	54
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	55	end

author	desharna
	Thu, 09 Jul 2020 11:39:16 +0200
changeset 72004	913162a47d9f
parent 39502	cffceed8e7fa
permissions	-rw-r--r--