Loading...
Please wait, while we are loading the content...
Similar Documents
Twelfth International Conference on Very Large Data Bases
| Content Provider | Semantic Scholar |
|---|---|
| Author | Wiederhold, Gio Manthey, Reinhard Schmidt, Johanna Zaniolo, Carlo Travis, Lori L. Quang, Ν. B. Somers, James E. Bitton, Dina |
| Copyright Year | 2013 |
| Abstract | 1 . I n t r o d u c t i o n I n a database c o n t e x t , a lot of w o r k has been done on i n t e g r i t y en forcement , i .e. , on check ing the v a l i d i t y of a database s t a t e w i t h respect t o a g iven set of i n t e g r i t y c o n s t r a i n t s . T h e q u e s t i o n w h e t h e r t h e c o n s t r a i n t set i t se l f is cons is tent has t i l l now received q u i t e few a t t e n t i o n , a l t h o u g h t h e p r o b l e m is f u n d a m e n t a l ( f 12) c o n s t i t u t e s a n o t a b l e e x c e p t i o n ) . U s u a l l y con s t r a i n t s are e i ther t a c i t l y assumed t o be cons is tent , or t h e use of a theorem prover" is suggested i n order t o detect inconsis tencies . I f c o n s t r a i n t s are r e s t r i c t e d t o come f r o m classes l ike f u n c t i o n a l , m u l t i v a l u e d or i m p l i c a t i o n a l dependencies , consis tency is a l ready i m p l i e d by the s y n t a c t i c a l p roper t i e s of t h e respect ive classes. However , as p o i n t e d out by m a n y a u t h o r s , more general k i n d s of c o n s t r a i n t s have t o be a d m i t t e d , a n d there fore the p r o b l e m has t o be addressed on a m o r e general basis. As the f o r m a l i s m s of r e l a t i o n a l databases a n d p r e d i c a t e loaic arc so closely r e l a t e d , we w i l l consider c o n s t r a i n t s as ar b i t r a l 1 ) closed and func t i on f ree f i rst order f o r m u l a s . Consistency is a necessary wel l formedness c o n d i t i o n for con s t r a i n t sets (as opposed t o . e.g.. n o n r e d u n d a n c y w h i c h is a des i rab le , b u t no t an indispensable r e q u i r e m e n t ) . A n inconsis t e n t set of c o n s t r a i n t s does not a d m i t any v a l i d database s t a t e . In terms of logic , database states can be cons idered as i n t e r p r e t a t i o n s of the c o n s t r a i n t s . V a l i d states c o r respond to i n t e r p r e t a t i o n s in w h i c h every c o n s t r a i n t is t r u e , i .e. , t o models of the c o n s t r a i n t set. Incons is tent sets of f o r m u l a s do no t have any mode) they are unsat i s f iab le . ( T h e m o d e l t h e o r e t i c p r o p e r t y " s a t i s f i a b i l i t y ' is equ iva lent t o the p r o o f t h e o r e t i c p r o p e r t y ' cons is tency ' a c c o r d i n g t o Goedel 's Completeness T h e o r e m ) . As database states correspond to models of the c o n s t r a i n t s , i t is not suf f i c ient to guarantee the existence of any m o d e l in genera l , b u t finite models have to exist in p a r t i c u l a r . In con v e n t i o n a l databases, c o n s t r a i n t s have t o a d m i t f i n i t e models as every s ta te consists of a finite n u m b e r of facts . I n d e f i n i t e d e d u c t i v e databases (as def ined i n |9|) t h e set of d e d u c t i o n rules a lways has a finite m i n i m a l m o d e l , w h i c h is i n t e n d e d to be a m o d e l of the c o n s t r a i n t set as w e l l . S a t i s f i a b i l i t y does not necessarily i m p l y finite satisfiability, i .e . , t h e existence of a f i n i t e mode) . T h e r e are sat is f iable sets of f o rmulas ca l led ' ax ioms of i n f i n i t y ' t h a t have on ly i n f i n i t e models . Cons ider , e.g., a set o f i n t e g r i t y c o n s t r a i n t s for a m a n a g e r i a l databaee c o n t a i n i n g ( a m o n g others ) the f o l l o w i n g c o n s t r a i n t s : • E v e r y b o d y works for somebody . • N o b o d y w o r k s for himsel f . • I f χ w o r k s for y a n d y w o r k s for i . t h e n χ w o r k s for t . Expressed as first-order f o r m u l a s , these three c o n s t r a i n t s cor respond to a w e l l k n o w n a x i o m of i n f i n i t y . A l t h o u g h each o f t h e m appears t o be reasonable as such, an i n f i n i t e n u m b e r of i n d i v i d u a l s is required i n an^v mode l of the set as a w h o l e . T h i s defect cou ld be a v o i d e d by p r o v i d i n g the first c o n s t r a i n t w i t h a prov i so l ike , e.g., " e v e r y b o d y except the top-manager . .* ' . M u c h more complex a x i o m s of i n f i n i t y may be h i d d e n ins ide a large a n d i n t r i c a t e set of c o n s t r a i n t s w h i c h c a n n o t be so easily i d e n t i f i e d as in the example above. There fore , in a d d i t i o n t o p r e v e n t i n g c o n s t r a i n t s f r o m being unsat i s f iab le , ax ioms o f i n finity have t o be avo ided as w e l l . C o n s t r a i n t s have t o be finitely sat is f iab le . as a lready br ie f ly m e n t i o n e d i n |8). F i g u r e 1 i l lus t ra tes how the three proper t i es m e n t i o n e d are r e l a t e d . sat isfiab)«TJijMa t i^fiabl» f i n i t e l y a x i o m o f i n f i n i t y s a t i s f i a b l e unacceptab le as c o n s t r a i n t s F i g . 1 Because of the u n d e c i d a b i l i t y o f s a t i s f i a b i l i t y , no a l g o r i t h m can be c o n s t r u c t e d t h a t s lops for every possible set of for mula*, and reports whether th i s set is finitely sat is f iab le , u n sat is f iab le or an ax iom of i n f i n i t y . F i n i t e s a t i s f i a b i l i t y , as w e l l as u n s a t i s f i a b i l i t y . is undec idab le |17], b u t b o t h are at least semi -dec idab le : a l g o r i t h m s can be cons t ruc ted t h a t are g u a r a n t e e d to repor t the respective p r o p e r t y after finite ( b u t i n d e f i n i t e ) l i m e if app l i ed t o a set t h a t a c t u a l l y has t h i s p r o p e r t y , but possibly r u n forever else. E v e r y r e f u t a t i o n m e t h o d is in fact a semi-decis ion procedure for u n s a t i s f i a b i l i t y . Procedures of th is k i n d have been in use as t h e o r e m provers Permission to copy without fee all or part of this material is granted provided that the copies are not made or distributed for direct commercial advantage, the VLDB copyright notice and the title of the publication and its date appear, and notice is given that copyins is by permission of the Very Large Data Base Endowment. To copy otherwise, or to republish, requires a fee andfor special permission from the Endowment. Proceedings of the Twelfth International Conference on Very Large Data Bases Kyoto, August, 1986 |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | https://epub.ub.uni-muenchen.de/8461/1/8461.pdf |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
