PowerPoint PresentationElectronic SpreadsheetsWhy People Like SpreadsheetsLimitations of Traditional SpreadsheetsApplications of Many-to-Many, Multidirectional ConstraintsLogical RepresentationFrom Functions to ConstraintsFormal DefinitionsLogical SpreadsheetsValue AssignmentsConstraintsN-ary RelationsLogical Spreadsheet = Interactive CSPLogical Spreadsheets as DatabasesUpdating Logical SpreadsheetsUser-specified Cells vs. Computed CellsBilevel UpdateDirect ConflictInformation Loss vs. InconsistencyProblemProofs and ExplosionWhat Happened?Proofs Requiring Consistent PremisesArgumentsPropositional Argument-ResolutionArgument Resolution ExampleWhat About Constraints?-argumentsPropositional -ResolutionExampleLogical Spreadsheet DemoSlide 32WebsheetsInterlinked SpreadsheetsWorld Wide SpreadsheetThanks!Logical SpreadsheetsComputational Logic Lecture 18Michael Kassof Autumn 20062Electronic Spreadsheets•Huge success•Used by everyone from multinational conglomerates to individuals •Uses–Financial planning–Scientific data analysis–Shopping lists3Why People Like Spreadsheets•Saves you work–Automatic calculation–Automatic recalculation•Allows “what if” analysis•Programming is easy–You don’t have to be a programmer to program a spreadsheet–Mathematical notation is familiar to people (C1=A1+B1)–Unlike traditional programs, intermediate computation steps are all displayed for you–It’s like being in debug mode all the time4Limitations of Traditional SpreadsheetsUnidirectional updateFunctional definitions, not many-to-many constraints5Applications of Many-to-Many, Multidirectional Constraints•Correct-on-capture data entry (smart forms)–“Start times must be before end times”–“The number of lap infants traveling must not be greater than the number of adults”•Enterprise Management policies–“Only senior managers can reserve the third floor conference room”•Design / Configuration–“If the car’s exterior color is blue, the possible interior colors are blue, tan and gray.”–“Students must take at least 2 math courses to graduate”6Logical RepresentationWe choose to represent many-to-many relationships using logical formulaestart-time(S) and end-time(E) before(S,E) “The start time must be before the end time”event-owner(O) and senior-manager(O) event-room(room301)“Only senior managers can reserve the third floor conference room”Note that the arrows do not imply directionality. Relationships are omnidirectional.7From Functions to ConstraintsExample: Event creation smart form DemoConstraints“Start Time < End Time” “Start Time + Duration = End Time”Formal Definitions9Logical SpreadsheetsA logical spreadsheet consists of a finite set of cells, a set of possible values for those cells, and a set of constraints encoded as logical sentences.Cells: {p, q, r}Possible Values: {a, b, c, d}Constraints: {p(x) q(x), q(x) or r(x)}10Value AssignmentsWe represent value assignments to cells with ground unary atoms{student(bob), major(math)}mathmajorstudentbob11ConstraintsArbitrary first-order constraints over cells are allowedView Definitions:r(x) p(x) q(x)Functional Dependencies:r(x) r(y) x=yExistential Constraints:x.r(x)Integrity Constraints:(p(x) q(x)) r(x)12N-ary RelationsThrough view definitions, can expand language to include n-ary relations without an increase in expressive powerView Definitions:location(x,y) e(x) r(y)Functional Dependencies:location(x,y) location(x,z) y=zExistential Constraints:event(x) y.location(x,y)Integrity Constraints:needs-projector(x) has-projector(y) location(x,y)For the rest of the presentation, we’ll just use unary relations13Logical Spreadsheet = Interactive CSPA constraint satisfaction problem consists of a set of variables, a set of possible values for those variables, and set of constraints“variable” = “single-valued cell”Note the focus on interactivity14Logical Spreadsheets as DatabasesA logical spreadsheet can be viewed as a deductive database (database with constraints) consisting of unary relationsP Q Ra c cUpdating Logical Spreadsheets16User-specified Cells vs. Computed CellsCan assign a value to any cellUser-specified cells are marked with a dark outlineComputed cells contain logical consequences of user-specified cellsUser specifiedSystem generatedbp qbap qap(X) q(X)17Bilevel UpdateQ: Why does a logical spreadsheet distinguish between user specified and system generated values?A: When values are removed from user-specified cells, their consequences go awayUser specifiedSystem generatedp qap qap(X) q(X)18Direct ConflictWhat happens when a newly assigned value conflicts with a previously assigned one?ap qap(X) q(X)bPossible outcomesap qaRejectbp qaConflictbp qbResolve19Information Loss vs. Inconsistencyengcourse1course1(eng) or course2(eng) or course3(eng)course2 course3engPossible outcomesengcourse1 course2 course3engeng engcourse1 course2 course3engcourse1 course2 course3eng engcourse1 course2 course3engeng“Students must take some course from outside the engineering school.”20ProblemA set of sentences logically entails a sentence if and only if every model of is a model of .An inconsistent theory has no models.Explosion!engcourse1 course2 course3engengart,cs,math,…major21Proofs and Explosion= {p(a), q(a), p(a) or q(a)}Question: Is r(b) provable from ?Proof:Pp(a) PremisePq(a) PremisePp(a) or q(a) PremisePr(b) GoalPq(a) [1,3]P{} [2,5] success!22What Happened?1. p(a) Premise2. q(a) Premise.3 p(a) or q(a) Premise.4 r(b) Goal.5 q(a) [1,3]6. {} [2,5] success!Notice that the set of premises used in the proof, {p(a), q(a), p(a) or q(a)} is inconsistentWhat if we were to require that the set of premises in a proof was consistent?23Proofs Requiring Consistent Premises Premises used to obtain this result1. p(a) Premise {p(a)}2. q(a) Premise {q(a)}3. p(a) or q(a) Premise {p(a) or q(a)}3. r(b) Goal {}3. q(a) [1,3] {p(a), p(a) or q(a)}6. {} [2,5] {p(a), p(a) or q(a), q(a)}The final step is disallowed since q(a) is inconsistent with the premises used to prove step 5.Note that since we are restricting ourselves to unary logic, consistency is decidable.24ArgumentsTo formalize this idea, we introduce the notion of an argument.An argument is
View Full Document
Unlocking...