Commit be062cbe authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

Theories: premiere version de la saturation de témoins + completion

parent 87b2f2f8
......@@ -17,4 +17,10 @@ General
X Integrer closed dans Valid et valid_deriv ??
ToCoq : revoir a se passer de BClosed general,
maintenant que Valid impose des temoins BClosed
\ No newline at end of file
maintenant que Valid impose des temoins BClosed
gen_fun_symbs ---> funsymbs
et mettre un autre long (plus long) dans le cas d'une signature par liste
Related works
https://www.isa-afp.org/entries/Completeness-paper.pdf
\ No newline at end of file
This diff is collapsed.
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