English
 
User Manual Privacy Policy Disclaimer Contact us
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
  On the Expressivity and Applicability of Model Representation Formalisms

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

Item is

Basic

show hide
Item Permalink: http://hdl.handle.net/21.11116/0000-0004-031B-B Version Permalink: http://hdl.handle.net/21.11116/0000-0004-031C-A
Genre: Paper

Files

show Files
hide Files
:
arXiv:1905.03651.pdf (Preprint), 225KB
Name:
arXiv:1905.03651.pdf
Description:
File downloaded from arXiv at 2019-07-10 11:41
Visibility:
Public
MIME-Type / Checksum:
application/pdf / [MD5]
Technical Metadata:
Copyright Date:
-
Copyright Info:
-

Locators

show

Creators

show
hide
 Creators:
Teucke, Andreas1, Author              
Voigt, Marco1, Author              
Weidenbach, Christoph1, Author              
Affiliations:
1Automation of Logic, MPI for Informatics, Max Planck Society, ou_1116545              

Content

show
hide
Free keywords: Computer Science, Logic in Computer Science, cs.LO
 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.

Details

show
hide
Language(s): eng - English
 Dates: 2019-05-092019
 Publication Status: Published online
 Pages: 15 p.
 Publishing info: -
 Table of Contents: -
 Rev. Method: -
 Identifiers: arXiv: 1905.03651
URI: http://arxiv.org/abs/1905.03651
BibTex Citekey: Teucke_arXiv1905.03651
 Degree: -

Event

show

Legal Case

show

Project information

show

Source

show