# Item

ITEM ACTIONSEXPORT

Released

Paper

#### On the Expressivity and Applicability of Model Representation Formalisms

##### MPS-Authors

##### External Resource

No external resources are shared

##### Fulltext (restricted access)

There are currently no full texts shared for your IP range.

##### Fulltext (public)

arXiv:1905.03651.pdf

(Preprint), 225KB

##### Supplementary Material (public)

There is no public supplementary material available

##### Citation

Teucke, A., Voigt, M., & Weidenbach, C. (2019). On the Expressivity and Applicability of Model Representation Formalisms. Retrieved from http://arxiv.org/abs/1905.03651.

Cite as: https://hdl.handle.net/21.11116/0000-0004-031B-B

##### Abstract

A number of first-order calculi employ an explicit model representation

formalism for automated reasoning and for detecting satisfiability. Many of

these formalisms can represent infinite Herbrand models. The first-order

fragment of monadic, shallow, linear, Horn (MSLH) clauses, is such a formalism

used in the approximation refinement calculus. Our first result is a finite

model property for MSLH clause sets. Therefore, MSLH clause sets cannot

represent models of clause sets with inherently infinite models. Through a

translation to tree automata, we further show that this limitation also applies

to the linear fragments of implicit generalizations, which is the formalism

used in the model-evolution calculus, to atoms with disequality constraints,

the formalisms used in the non-redundant clause learning calculus (NRCL), and

to atoms with membership constraints, a formalism used for example in decision

procedures for algebraic data types. Although these formalisms cannot represent

models of clause sets with inherently infinite models, through an additional

approximation step they can. This is our second main result. For clause sets

including the definition of an equivalence relation with the help of an

additional, novel approximation, called reflexive relation splitting, the

approximation refinement calculus can automatically show satisfiability through

the MSLH clause set formalism.

formalism for automated reasoning and for detecting satisfiability. Many of

these formalisms can represent infinite Herbrand models. The first-order

fragment of monadic, shallow, linear, Horn (MSLH) clauses, is such a formalism

used in the approximation refinement calculus. Our first result is a finite

model property for MSLH clause sets. Therefore, MSLH clause sets cannot

represent models of clause sets with inherently infinite models. Through a

translation to tree automata, we further show that this limitation also applies

to the linear fragments of implicit generalizations, which is the formalism

used in the model-evolution calculus, to atoms with disequality constraints,

the formalisms used in the non-redundant clause learning calculus (NRCL), and

to atoms with membership constraints, a formalism used for example in decision

procedures for algebraic data types. Although these formalisms cannot represent

models of clause sets with inherently infinite models, through an additional

approximation step they can. This is our second main result. For clause sets

including the definition of an equivalence relation with the help of an

additional, novel approximation, called reflexive relation splitting, the

approximation refinement calculus can automatically show satisfiability through

the MSLH clause set formalism.