SGER: Managing Inconsistency in Logical Spreadsheets

Stanford University, Stanford CA

Investigators

Abstract

In traditional spreadsheet systems, such as Excel, cells are partitioned into "directly specified" cells and "computed" cells and the formulas used to specify the values of computed cells are "functional", i.e. for every combination of values of the directly specified cells, the formulas specify unique values for the computed cells. Logical Spreadsheets expand the utility of traditional spreadsheets by dispensing with the distinction between directly specified cells and computed cells and generalizing from functional definitions to logical constraints. One problem with logical spreadsheets is the potential for inconsistency. In using logical spreadsheets, users can select values for cells that are inconsistent with the values of other cells, given the constraint defining the spreadsheet. Simply eliminating inconsistent values is not the answer - (1) rejecting new values that are inconsistent with past values limits the user's freedom and (2) dropping past values that are inconsistent with new values restores consistency but loses information. On the other hand, retaining inconsistencies is problematic when the spreadsheet tries to derive consequences of updates, since inconsistent logical theories entail everything! Unlike logical entailment, existential entailment behaves well in the face of inconsistencies and, therefore, is more useful in this setting. Work in this project includes (1) a study of the behavioral properties of existential entailment in the context of logical spreadsheets, (2) the development of efficient algorithms for computing existential entailment (with special attention to rule transformation, reformulation, and differential logic), (3) the development of an open-source Javascript implementation incorporating these algorithms, and (4) an evaluation of this technology in the form of user surveys, comparative studies, and ablation studies. Further information on the project can be found at the project web site at http://logicalc.stanford.edu.