Fast decision procedure for propositional Dummett logic based on a multiple premise tableau calculus
We present a procedure to decide propositional Dummett logic. Such a procedure relies on a tableau calculus with a multiple premise rule and optimizations. The resulting implementation outperforms the state of the art graph-based procedure.
dummett logic gdel logic tableau calculi intermediate logics automated theorem proving