Logic and binary trees
by
Irena Atanasova

The theory of binary trees is a theory with equality. In this theory are defined following concepts: atom (x), tree (x), left (x), right (x), subtree and proper subtree. For every tree x is defined a unary functional symbol listtree (x). The value of listtree is a the tuple whose elements are the leaves of x. In the theory of trees are defined following functions: size (x) (the number of nodes and leaves in a tree x), leav (x) (the number of leaves in a tree x) and depth (x) (the number of nodes and leaves in the longest path of a tree x). In the tableau method for proving the validity are using axioms as assertions and the axiom (x=x).

Date received: July 27, 2001