### Skapa referens, olika format (klipp och klistra)

**Harvard**

Ahrendt, W. (2002) *Deductive Search for Errors in Free Data Type Specifications using Model Generation*.

** BibTeX **

@conference{

Ahrendt2002,

author={Ahrendt, Wolfgang},

title={Deductive Search for Errors in Free Data Type Specifications using Model Generation},

booktitle={Lecture Notes in Computer Science. 18th International Conference on Automated Deduction Copenhagen, Denmark, July 27–30, 2002},

isbn={978-3-540-43931-8},

pages={211-225},

abstract={The presented approach aims at identifying false conjectures about free data types. Given a specification and a conjecture, the method performs a search for a model of an according counter specification. The model search is tailor-made for the semantical setting of free data types, where the fixed domain allows to describe models just in terms of interpretations. For sake of interpretation construction, a theory specific calculus is provided. The concrete rules are ‘executed’ by a procedure known as model generation. As most free data types have infinite domains, the ability of automatically solving the non-consequence problem is necessarily limited. That problem is addressed by limiting the instantiation of the axioms. This approximation leads to a restricted notion of model correctness, which is discussed. At the same time, it enables model completeness for free data types, unlike approaches based on limiting the domain size.},

year={2002},

}

** RefWorks **

RT Conference Proceedings

SR Electronic

ID 170475

A1 Ahrendt, Wolfgang

T1 Deductive Search for Errors in Free Data Type Specifications using Model Generation

YR 2002

T2 Lecture Notes in Computer Science. 18th International Conference on Automated Deduction Copenhagen, Denmark, July 27–30, 2002

SN 978-3-540-43931-8

SP 211

OP 225

AB The presented approach aims at identifying false conjectures about free data types. Given a specification and a conjecture, the method performs a search for a model of an according counter specification. The model search is tailor-made for the semantical setting of free data types, where the fixed domain allows to describe models just in terms of interpretations. For sake of interpretation construction, a theory specific calculus is provided. The concrete rules are ‘executed’ by a procedure known as model generation. As most free data types have infinite domains, the ability of automatically solving the non-consequence problem is necessarily limited. That problem is addressed by limiting the instantiation of the axioms. This approximation leads to a restricted notion of model correctness, which is discussed. At the same time, it enables model completeness for free data types, unlike approaches based on limiting the domain size.

LA eng

DO 10.1007/3-540-45620-1_18

LK http://dx.doi.org/10.1007/3-540-45620-1_18

OL 30