Skip to Main content Skip to Navigation
Conference papers

On the Expressivity and Applicability of Model Representation Formalisms

Andreas Teucke 1, 2 Marco Voigt 1, 2 Christoph Weidenbach 2, 1
2 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
LORIA - FM - Department of Formal Methods , Inria Nancy - Grand Est, MPII - Max-Planck-Institut für Informatik
Abstract : A number of first-order calculi employ an explicit model representation formalism in support of non-redundant inferences 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 (AR). 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 (ME), 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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [33 references]  Display  Hide  Download

https://hal.inria.fr/hal-02406605
Contributor : Stephan Merz <>
Submitted on : Thursday, December 12, 2019 - 10:59:02 AM
Last modification on : Tuesday, March 3, 2020 - 4:03:27 PM
Long-term archiving on: : Friday, March 13, 2020 - 8:28:02 PM

File

frocos19.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Andreas Teucke, Marco Voigt, Christoph Weidenbach. On the Expressivity and Applicability of Model Representation Formalisms. FroCoS 2019 - 12th International Symposium on Frontiers of Combining Systems, 2019, London, United Kingdom. pp.22-39, ⟨10.1007/978-3-030-29007-8_2⟩. ⟨hal-02406605⟩

Share

Metrics

Record views

46

Files downloads

164