Gödel-Dummett Counter-models through Matrix Computation

We present a new method for deciding Gödel-Dummett logic. Starting from a formula, it proceeds in three steps. First build a conditional graph based on the decomposition tree of the formula. Then try to remove some cycles in this graph by instantiating these boolean conditions. In case this is possible, extract a counter-model from such an instance graph. Otherwise the initial formula is provable. We emphasize on cycle removal through matrix computation, boolean constraint solving and counter-model extraction.