Tree Reasoning Solver
The tree reasoning solver is a software tool which implements research advances in tree logics, and in the analysis of query and programming languages for the web. The core algorithm is a satisfiability solver of an expressive tree logic which is described in Efficiently Deciding μ-calculus with Converse over Finite Trees (TOCL'15). The tree logic is flexible and can easily be used to formulate and solve properties of tree-shaped structures. Initially developed for the analysis of XML/XPath queries, this tool has been extended by the team to support more general query analysis, reasoning with schema constraints, with functions, and with domain specific languages such as cascading style sheets.
Software: Online Demo
You can try the solver online with your own formulas and/or starting from sample formulas generated by applications (see the "demo" tab).
Applications
- Query analysis with tree constraints
- Type-checking programs with functions
- Analysis and refactoring of Cascading Style Sheets
- Analysis of SPARQL queries
For more details on applications, logical foundations, related publications, sample formulas and online demo, see the tree reasoning solver project page.
