We use the recently developed theory of forest algebras to find algebraic
characterizations of the languages of unranked trees and forests definable in
various logics. These include the temporal logics CTL and EF, and first-order
logic over the ancestor relation. While the characterizations are in general
non-effective, we are able to use them to formulate necessary conditions for
definability and provide new proofs that a number of languages are not
definable in these logics.
Filip Murlak;Charles Paperman;Michał Pilipczuk, Zenodo (CERN European Organization for Nuclear Research), Schema Validation via Streaming Circuits, 2016, San Francisco California USA, 10.1145/2902251.2902299, https://zenodo.org/record/2758470.
Andreas Krebs;Howard Straubing, Lecture notes in computer science, EF+EX Forest Algebras, pp. 128-139, 2015, 10.1007/978-3-319-23021-4_12.