Counter-Model Search in Goedel-Dummett Logics

摘要

We present a new method for deciding Godel-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 LC_n.