@online{TeuckearXiv2017,
TITLE = {Decidability of the Monadic Shallow Linear First-Order Fragment with Straight Dismatching Constraints},
AUTHOR = {Teucke, Andreas and Weidenbach, Christoph},
LANGUAGE = {eng},
URL = {http://arxiv.org/abs/1703.02837},
EPRINT = {1703.02837},
EPRINTTYPE = {arXiv},
YEAR = {2017},
ABSTRACT = {The monadic shallow linear Horn fragment is well-known to be decidable and has many application, e.g., in security protocol analysis, tree automata, or abstraction refinement. It was a long standing open problem how to extend the fragment to the non-Horn case, preserving decidability, that would, e.g., enable to express non-determinism in protocols. We prove decidability of the non-Horn monadic shallow linear fragment via ordered resolution further extended with dismatching constraints and discuss some applications of the new decidable fragment.},
}