*** empty log message ***

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

1 files changed, 34 insertions, 0 deletions

diff --git a/contrib/graphs/README b/contrib/graphs/README
new file mode 100644
index 000000000..dd342607a
--- /dev/null
+++ b/contrib/graphs/README
@@ -0,0 +1,34 @@
+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