Prolog Tree Algebras. A formal specification of Prolog