b'@online{Teucke_arXiv1905.03651,'b'\nTITLE = {On the Expressivity and Applicability of Model Representation Formalisms},\nAUTHOR = {Teucke, Andreas and Voigt, Marco and Weidenbach, Christoph},\nLANGUAGE = {eng},\nURL = {http://arxiv.org/abs/1905.03651},\nEPRINT = {1905.03651},\nEPRINTTYPE = {arXiv},\nYEAR = {2019},\nABSTRACT = {A number of first-order calculi employ an explicit model representation<br>formalism for automated reasoning and for detecting satisfiability. Many of<br>these formalisms can represent infinite Herbrand models. The first-order<br>fragment of monadic, shallow, linear, Horn (MSLH) clauses, is such a formalism<br>used in the approximation refinement calculus. Our first result is a finite<br>model property for MSLH clause sets. Therefore, MSLH clause sets cannot<br>represent models of clause sets with inherently infinite models. Through a<br>translation to tree automata, we further show that this limitation also applies<br>to the linear fragments of implicit generalizations, which is the formalism<br>used in the model-evolution calculus, to atoms with disequality constraints,<br>the formalisms used in the non-redundant clause learning calculus (NRCL), and<br>to atoms with membership constraints, a formalism used for example in decision<br>procedures for algebraic data types. Although these formalisms cannot represent<br>models of clause sets with inherently infinite models, through an additional<br>approximation step they can. This is our second main result. For clause sets<br>including the definition of an equivalence relation with the help of an<br>additional, novel approximation, called reflexive relation splitting, the<br>approximation refinement calculus can automatically show satisfiability through<br>the MSLH clause set formalism.<br>},\n}\n'