MIT EECS (Emeritus)
4pm Tuesday 11th September 2007
Room 2511, JCMB, King's Buildings
It is well known that large software systems are chock full of inconsistencies among their documentation, use cases, and code. In a way, this is a good thing because if large software systems were required to be consistent, then they would not exist. Fortunately, the rules of classical logic can be modified in order to safely reason about such systems. Direct Logic is an unstratified reflective paraconsistent system (with mathematical induction) that is suitable for reasoning about inconsistent theories for large software systems.
A big advantage of paraconsistent logic is that it makes fewer mistakes than classical logic when dealing with inconsistent theories. Since software engineers have to deal with theories chock full of inconsistencies, paraconsistency should be attractive. However, to make it relevant we need to provide them with tools that are cost effective.
There is also an extended abstract available.