In previous work, we have advocated continued development of specifications in the presence of inconsistency. To support this, we have used classical logic to represent partial specifications and to identify inconsistencies between them. We now present an adaptation of classical logic, which we term quasi-classical (QC) logic, that allows continued reasoning in the presence of inconsistency. The adaptation is a weakening of classical logic that prohibits all trivial derivations, but still allows all resolvants of the assumptions to be derived. Furthermore, the connectives behave in a classical manner. We then present a development called labelled QC logic that records and tracks assumptions used in reasoning. This facilitates a logical analysis of inconsistent information. We discuss the application of labelled QC logic in the analysis of multi-perspective specifications. Such specifications are developed by multiple participants who hold overlapping, often inconsistent, views of the systems they are developing.
This paper is ACM Transactions on Software Engineering and Methodology, October 1998.
It is also available over the Web: [compressed postscript version].