Logical Spreadsheets Michael Genesereth Logic Group Stanford University in collaboration with Mike Kassoff and Eric Kao Computerized Spreadsheets Huge Success individual users companies conglomerates Good Features Automatic computation of values Ease of specification using simple math formulas 2 63 Limitations of Traditional Spreadsheets Functional formulas B3 B1 B2 Unidirectional Update B1 B2 B3 2 3 5 3 63 Examples of Non Functional Constraints Scheduling Start times must be before end times Room 104 may not be scheduled after 5 00 pm Only senior managers can reserve the third floor conference room Travel Reservations The number of lap infants in a group on a flight must not exceed the number of adults Academic Programs Students must take at least 2 math courses 4 63 Logical Spreadsheets Extension Relational constraints on the values of cells Good Features Automatic computation of values Ease of set up using logical formulas Challenges Automatic update Temporary inconsistencies User feedback 5 63 Spreadsheet Websheet Applications Data management Design Configuration Smart Forms Interactive Answers 6 63 Definitions 7 63 Logical Spreadsheets A logical spreadsheet consists of a finite set of cells a set of possible values for those cells and a set of constraints on cell values Cells p q r s Possible Values a b c d Constraints If p is assigned a then q must be assigned b or c If r is not a then s must have the same value as q 8 63 Value Assignments A value assignment is a function from cells to values A value assignment is complete if this function is total Otherwise it is partial In what follows we formalize value assignments as sets of ground atomic sentences in which the relation represents the cell and the argument represents the value p a q b r c 9 63 Completeness A value assignment for a logical spreadsheet is complete if and only if it assigns exactly one value to each cell in the spreadsheet i e for every cell there is exactly one constant such that Cells p q r Values a b c d p a q a r a 10 63 Constraint Language A constraint is a boolean formula involving cell names object names variables and equality Cell p must be a or both q and r must both be b p a q b r b If p is assigned a then q must be assigned b or c p a q b q c If p and q are the same then r must be different p x q x r x 11 63 Consistency A value assignment is consistent with a selfconsistent set of constraints if and only if they do not logically entail a contradiction i e Cells p q r Values a b c d p x q x q x r x p a q a r a NB In managing logical spreadsheets we must sometimes deal with inconsistent value assignments 12 63 Goals and Limitations User s Goal complete consistent value assignment satisfying unwritten constraints as well Limitation one cell at a time changing 13 63 General Principles Obedience specified update Propagation consequences shown Fairness no arbitrary choices made by the system Conservation no unnecessary loss of information 14 63 Obedience Update a p b q r p a q r Outcome 15 63 Conservation Update a p b q r c p a q r c Outcome 16 63 Logical Entailment Given a set of constraints a dataset logically entails a conclusion written iff is true in every dataset that contains and satisfies the constraints in Example p x q x x p a p a q a a q a b 17 63 Update and Propagation Divide dataset into specified and computed Addition Compute logical consequences of and the constraints and remove any cells from for which the negation is logically entailed Add to to form Deletion Drop from to form Propagation Compute all logical consequences from and make these 18 63 Adding Data Update p q r a p x r x p x p y x y r x r y x y Outcome p a q r a 19 63 Changing Data Update p a q r a b p x r x p x p y x y r x r y x y Outcome p b q r b 20 63 Erasing Data Update erase p a q r a p x r x p x p y x y r x r y x y Outcome p q r 21 63 Erasing Conclusions Update p a q r a erase p x r x p x p y x y r x r y x y Outcome Erasure of computed values disallowed 22 63 Ambiguity Update p a q a r a p x q x r x Result 23 63 Ambiguity Update p a q a r a p x q x r x Possible Outcomes p a q r a p a q a r p a q r p a q a r a 24 63 Explosion Logical Entailment if and only if every consistent model of is a model of If a set of sentences is inconsistent then it logically entails everything p a b c q a b c r a b c s a b c 25 63 Existential Entailment A set of sentences existentially entails a sentence relative to written if and only if there is an consistent subset of that when added to logically entails and and Existential entailment is not explosive It generates only justified conclusions 26 63 Example Constraints p x q x r x p a q a s c q a r a t c s x t x u x Data p a q a r a Conclusions s c t c 27 63 Propagation Rule modified version Propagation original version Propagation modified version 28 63 Example 29 63 Example QuickTime and a TIFF LZW decompressor are needed to see this picture 30 63 Example QuickTime and a TIFF LZW decompressor are needed to see this picture 31 63 Example QuickTime and a TIFF LZW decompressor are needed to see this picture 32 63 Example QuickTime and a TIFF LZW decompressor are needed to see this picture 33 63 Example 34 63 Example QuickTime and a TIFF LZW decompressor are needed to see this picture 35 63 Example QuickTime and a TIFF LZW decompressor are needed to see this picture 36 63 Example QuickTime and a TIFF LZW decompressor are needed to see this picture 37 63 Example QuickTime and a TIFF LZW decompressor are needed to see this picture 38 63 Conclusion 39 63 Dynamic Constraints Static Constraints X clear a table c on a b on b c clear a table c on a b on b a Dynamic Constraints clear a clear b clear c table a table b table c clear a clear b table b table c on b c clear a table c on b c on a b X 40 63 Existential Entailment Computation The na ve approach to computing existential conclusions from is to take each subset of and derive logical …
View Full Document
Unlocking...