© 2004 by Oxford University Press
Original Article |
Rules and Refutation Rules for the Logic of Finite n-ary Trees
Department of Logic, University of Wroc
aw, Koszarowa 3, 51-149 Wroc
aw, Poland. E-mail: tfskura{at}uni.wroc.pl
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.
Keywords: Intermediate logics, decidability, axiom systems, refutation rules, normal forms.
Received 24 March 2003.