Commit 6132f13b authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

TODO update

parent e1610e58
......@@ -29,7 +29,7 @@ Record PreModel (M:Type)(sign:signature) :=
predsOk : forall s, sign.(predsymbs) s = get_arity (preds s)
}.
(** A premodel is also called a Σ-structure. For a complete model
(** A premodel is also called a Σ-structure. For a full model
of a theorie, we'll need the axioms of the theories, and
the facts that their interpretations are valid. *)
......
- un depôt a part du cours
- un README detaillé, licence, etc etc
- paquet opam ? depot git a part
- plus de doc et de commentaires dans les .v
- paquet opam ?
- formula parsing
- puis en faire un binaire autonome par extraction
......@@ -25,11 +26,18 @@ General
(x) unionmap_in à revoir, plus gal pourquoi autant de in_map_iff
PreModel : revoir a se passer de BClosed general,
maintenant que Valid impose des temoins BClosed (??)
KO : PreModel : revoir a se passer de BClosed general,
maintenant que Valid impose des temoins BClosed
--> Non, ou alors il faudrait revoir bsubst avec des -1 pour
les bvars au delà de celle qu'on substitue.
- PreModel : funsOk et predsOk sont-ils vraiment utiles ?
ou bien sinon est-ce que AxOk suffit ?
- Axiomes de Peano + exos + modèle Coq
- Idem pour ZF
- Skolem
Axiomes de Peano + exos + modèle Coq
Idem pour ZF
Related works
https://www.isa-afp.org/entries/Completeness-paper.pdf
\ No newline at end of file
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment