Search

We give sound and complete axiomatizations for XPath with data tests by ‘equality’ or ‘inequality’, and containing the single ‘child’ axis. This data-aware logic predicts over data trees, which are tree-like structures whose every node contains a label from a finite alphabet and a data value from an infinite domain. The language allows us to compare data values of two nodes but cannot access the data values themselves (i.e. there is no comparison by constants). Our axioms are in the style of equational logic, extending the axiomatization of data-oblivious XPath, by B. ten Cate, T. Litak and M. Marx. We axiomatize the full logic with tests by ‘equality’ and ‘inequality’, and also a simpler fragment with ‘equality’ tests only. Our axiomatizations apply both to node expressions and path expressions. The proof of completeness relies on a novel normal form theorem for XPath with data tests. [ABSTRACT FROM AUTHOR]

In this paper we develop the theoretical foundations to exploit symmetries in modal logics. We generalize the notion of symmetries of propositional formulas in conjunctive normal form to modal formulas using the framework provided by coinductive modal models introduced in [5]. Hence, the results apply to a wide class of modal logics including, for example, hybrid logics. We present two graph constructions that enable the reduction of symmetry detection in modal formulas to the graph automorphism detection problem, and we evaluate the graph constructions on modal benchmarks. [ABSTRACT FROM AUTHOR]