Gödel-Dummett counter-models through matrix computation

Dominique Larchey-Wendling (1)

1 TYPES - Logic, proof Theory and Programming

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.

Domaines: Logique en informatique [cs.LO]; Intelligence artificielle [cs.AI]; Algorithme et structure de données [cs.DS]

Dominique Larchey-Wendling. Gödel-Dummett counter-models through matrix computation. Workshop on Disproving, IJCAR 2004, 2004, Ireland. ⟨hal-00008808⟩