Counter-model search in Gödel-Dummett logics

Dominique Larchey-Wendling (1)

1 TYPES - Logic, proof Theory and Programming

We present a new method for deciding Gödel-Dummett logic LC. We first characterize the validity of irreducible sequents of LC by the existence of r-cycles in bi-colored graphs and we propose a linear algorithm to detect r-cycles and build counter-models. Then we characterize the validity of formulae by the existence of r-cycles in boolean constrained graphs. We also give a parallel method to detect r-cycles under boolean constraints. Similar results are given for the finitary versions LCn.

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

Dominique Larchey-Wendling. Counter-model search in Gödel-Dummett logics. Second International Joint Conference on Automated Reasoning - IJCAR 2004, Jul 2004, Cork, Ireland. pp.274 -- 288, ⟨10.1007/978-3-540-25984-8_19⟩. ⟨hal-00008806⟩