Logical spreadsheet

Logical Spreadsheets relax these restrictions by dispensing with the distinction between directly specified cells and computed cells and generalizing from functional definitions to logical constraints.

Implemented as a traditional spreadsheet, this spreadsheet would allow the user to enter values into cells a and b, and it would automatically compute cell c. For example, if the user were to type 1 into a and 2 into b, it would compute the value 3 for c. Implemented as a logical spreadsheet, the user would be able to enter values into any of the cells.

The user could type 1 into a and 2 into b, and the spreadsheet would compute the value 3 for c. Alternatively, the user could type 2 into b and 3 into c, and the spreadsheet would compute the value 1 for a.

For example, in this case, we could write formulas involving inequalities and non-invertible functions (such as square root).

More generally, we could build spreadsheets with symbolic, rather than numeric data, and write arbitrary logical constraints on this data.