Rules and refutation rules for the logic of finite n-ary trees
In this paper we give a new syntactic decision procedure for the logic of finite n-ary trees (axiomatized by Gabbay and de Jongh by means of semantic methods). In the decision procedure we use the simple concept of a rule both for proving valid formulas and for refuting invalid ones. Refutation rules with certain normal forms are introduced, and it is shown in a constructive way that every normal form is either provable or refutable.
refutation rules normal forms intermediate logics decidability axiom systems