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.

Mots clés: Counter-models; conditional graphs and matrices

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

Dominique Larchey-Wendling. Gödel-Dummett counter-models through matrix computation. Electronic Notes in Theoretical Computer Science, 2005, 125 (3), pp.12. ⟨10.1016/j.entcs.2004.07.022⟩. ⟨hal-00008810⟩