La distribution de Rocq/GRAPHS se fait via le serveur de contributions utilisateur

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7755 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 0 insertions, 34 deletions

diff --git a/contrib/graphs/README b/contrib/graphs/README
deleted file mode 100644
index dd342607ad..0000000000
--- a/contrib/graphs/README
+++ /dev/null
@@ -1,34 +0,0 @@
-Satisfiability of inequality constraints and detection of cycles with
-negative weight in graphs
-Author: Jean Goubault 
-Institution: G.I.E. Dyade, Inria Rocquencourt
-Description: 
-	It has been well-known since Bellman [1957] that deciding the
-satisfiability over the set Z of integers of collections K of
-inequalities of the form x<=y+c, where x, y are variables and c is a
-constant of Z, can be done in polynomial time.
-
-	This holds even if we relax the form of our inequalities to be
-x<=c or x>=c.  The idea is to build a directed graph whose vertices
-are the variables (and a special vertex for 0), and whose edges are
-inequalities: the inequality x<=y+c is coded as an edge from x to y,
-with weight c.  Now the set K of inequality constraints is satisfiable
-if and only if the constructed graph has no cycle of negative weight,
-where the weight of a path is defined as the sum of the weights of its
-edges.
-	The aim of this contribution is, first, to reprove these
-results in Coq, and second, to build the decision procedure itself as
-a Coq term.  This allows us (in principle) to construct a reflection
-tactic deciding these kinds of sets K.  The reflection tactic itself
-has not been written, but all contributions are welcome.
-
-	These results are established in the general case where, instead of Z,
-we consider any totally ordered group.  A tableau procedure, coded as a Coq
-term, is provided to decide any positive combination of inequalities of
-the form above (positive meaning: using only conjunction and disjunction).
-When the totally ordered group has a 1, i.e., when it has a minimal strictly
-positive element, then we extend this tableau procedure to the case of
-general quantifier-free formulae built on inequations of the form above.
-This is specialized in zgraph.v to the case of Z.
-
-Keywords: graphs, cycles, paths, constraints, inequalities, reflection