In this paper we introduce a description language for finite trees. Although we briefly note some of its intended applications, the main goal of the paper is to provide it with a sound and complete proof system.We do so using standard axioms from modal provability logic and modal logics of programs, and prove completeness by extending techniques due to Van Benthem and Meyer-Viol [2] and Blackburn and Meyer-Viol [5]. We conclude with a proof of the EXPTIME-completeness of the satisfiability problem, and a discussion of issues related to complexity and theorem proving.

Language Constructs and Features (acm D.3.3), General (acm F.2.0), Nonnumerical Algorithms and Problems (acm F.2.2), General (acm F.4.0), Mathematical Logic (acm F.4.1), Grammars and Other Rewriting Systems (acm F.4.2), Formal Languages (acm F.4.3), Deduction and Theorem Proving (acm I.2.3), Knowledge Representation Formalisms and Methods (acm I.2.4)
Modal logic (including the logic of norms) (msc 03B45), Finite structures (msc 03C13), Complexity of proofs (msc 03F20), Trees (msc 05C05)
CWI
Department of Computer Science [CS]

Blackburn, P, Meyer Viol, W. P. M, & de Rijke, M. (1995). A proof system for finite trees. Department of Computer Science [CS]. CWI.