Handling Inconsistencies in Z Using Quasi-Classical Logic

  • Ralph Miarka
  • John Derrick
  • Eerke Boiten
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2272)


The aim of this paper is to discuss what formal support can be given to the process of living with inconsistencies in Z, rather than eradicating them. Logicians have developed a range of logics to continue to reason in the presence of inconsistencies. We present one representative of such paraconsistent logics, namely Hunter’s quasi-classical logic, and apply it to the analysis of inconsistent Zsc hemas. In the presence of inconsistency quasi-classical logic allows us to derive less, but more “useful”, information. Consequently, inconsistent Z specifications can be analysed in more depth than at present. Part of the analysis of a Zoperation is the calculation of the precondition. However, in the presence of an inconsistency, information about the intended application of the operation may be lost. It is our aim to regain this information. We introduce a new classification of precondition areas, based on the notions of definedness, overdefinedness and undefinedness. We then discuss two options to determine these areas both of which are based on restrictions of classical reasoning.


Classical Logic Proof Theory Operation Change Paraconsistent Logic Expansion Rule 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. Abrial, J.-R. (1996). The B-Book: Assigning Programs to Meanings. Cambridge University Press.Google Scholar
  2. Arthan, R. D. (1991). Formal Specification of a Proof Tool. In Prehn, S. and Toetenel, H., editors, Proceedings of Formal Software Development Methods (VDM’ 91), Lecture Notes in Computer Science 552, pages 356–370, Berlin, Germany. Springer.Google Scholar
  3. Balzer, R. (1991). Tolerating Inconsistency. In Proceedings of the 13th International Conference on Software Engineering, pages 158–165. IEEE Computer Society Press / ACM Press.Google Scholar
  4. Batens, D. (1999). Inconsistency-Adaptive Logics. In Orlowska, E., editor, Logic at Work. Essays Dedicated to the Memory of Helena Rasiowa, Studies in fuzziness and soft computing, Volume 24, pages 445–472, Heidelberg, New York. Physica-Verlag.Google Scholar
  5. Batens, D. (2000). A Survey of Inconsistency-Adaptive Logics. In (Batens et al., 2000), pages 49–73.Google Scholar
  6. Batens, D., Mortensen, C., Priest, G., and Bendegem, J.-P. V., editors (2000). Frontiers of Paraconsistent Logic. Research Studies Press Ltd., Baldock, Hertfordshire, England.zbMATHGoogle Scholar
  7. Beckert, B. (1997). Semantic Tableaux with Equality. Journal of Logic and Computation, 7(1):39–58.zbMATHCrossRefMathSciNetGoogle Scholar
  8. Besnard, P. and Hunter, A. (1995). Quasi-Classical Logic: Non-Trivializable Classical Reasoning from Inconsistent Information. In Froidevaux, C. and Kohlas, J., editors, Proceedings of the ECSQARU European Conference on Symbolic and Quantitive Approaches to Reasoning and Uncertainty, Lecture Notes in Artificial Intelligence 946, pages 44–51, Berlin. Springer Verlag.Google Scholar
  9. Boiten, E. A., Derrick, J., Bowman, H., and Steen, M. W. A. (1999). Constructive consistency checking for partial specification in Z. Science of Computer Programming, 35(1):29–75.zbMATHCrossRefMathSciNetGoogle Scholar
  10. da Costa, N. C. (2000). Paraconsistent Mathematics. In (Batens et al., 2000), pages 165–179.Google Scholar
  11. Finkelstein, A., Gabbay, D., Hunter, A., Kramer, J., and Nuseibeh, B. (1994). Inconsistency Handling in Multi-Perspective Specifications. IEEE Transactions on Software Engineering, 20(8):569–578.CrossRefGoogle Scholar
  12. Fitting, M. C. (1996). First-Order Logic and Automated Theorem Proving. Graduate Texts in Computer Science. Springer-Verlag, Berlin, 2nd edition.Google Scholar
  13. Ghezzi, C. and Nuseibeh, B. (1998). Guest Editorial: Introduction to the Special Section: Managing Inconsistency in Software Development. IEEE Transactions on Software Engineering, 24(11):906–907.Google Scholar
  14. Hunter, A. (1998). Paraconsistent Logic. In Besnard, P. and Hunter, A., editors, Reasoning with Actual and Potential Contradictions, Volume II of Handbook of Defeasible Reasoning and Uncertain Information (Gabbay, D. and Smets, Ph., editors), pages 13–44. Kluwer Academic Publishers, Dortrecht, The Netherlands.Google Scholar
  15. Hunter, A. (2000). Reasoning with Contradictory Information Using Quasi-Classical Logic. Journal of Logic and Computation, 10(5):677–703.zbMATHCrossRefMathSciNetGoogle Scholar
  16. Hunter, A. (2001). A Semantic Tabeau Version of First-Order Quasi-Classical Logic. In Benferhat, S. and Besnard, P., editors, Symbolic and Quantitative Approaches to Reasoning with Uncertainty, Proceedings of the 6th European Conference, ECSQARU 2001, Toulouse, France, Lecture Notes in Artificial Intelligence 2143, pages 544–555. Springer Verlag.Google Scholar
  17. Hunter, A. and Nuseibeh, B. (1997). Analysing Inconsistent Specifications. In Proceedings of the 3rd International Symposium on Requirements Engineering (RE’97), pages 78–86. Annapolis, USA, IEEE Computer Society Press.Google Scholar
  18. Hunter, A. and Nuseibeh, B. (1998). Managing Inconsistent Specifications: Reasoning, Analysis, and Action. ACM Transactions on Software Engineering and Methodology, 7(4):335–367.CrossRefGoogle Scholar
  19. Miarka, R., Boiten, E., and Derrick, J. (2000). Guards, Preconditions, and Refinement in Z. In Bowen, J. P., Dunne, S., Galloway, A., and King, S., editors, ZB2000: Formal Specification and Development in Z and B / First International Conference of B and Z Users, Lecture Notes in Computer Science 1878, pages 286–303, Berlin Heidelberg New York. Springer-Verlag Berlin.Google Scholar
  20. Mortensen, C. (1995). Inconsistent Mathematics. Kluwer Academic Publishers Group, Dordrecht, The Netherlands.Google Scholar
  21. Rescher, N. and Manor, R. (1970). On Inference from Inconsistent Premisses. Theory and Decision, 1:179–217.zbMATHCrossRefGoogle Scholar
  22. Saaltink, M. (1997). The Z/EVES User’s Guide. Technical Report TR-97-5493-06, ORA Canada, 267 Richmond Road, Suite 100, Ottawa, Canada.Google Scholar
  23. Schwanke, R. W. and Kaiser, G. E. (1988). Living with Inconsistency in Large Systems. In Proceedings of the International Workshop on Software Version and Configuration Control, pages 98–118, Grassau, Germany.Google Scholar
  24. Smullyan, R. M. (1968). First-Order Logic, Volume 43 of Ergebnisse der Mathematik und ihrer Grenzgebiete. Springer-Verlag, New York.Google Scholar
  25. Valentine, S. H. (1998). Inconsistency and Undefinedness in Z-A Practical Guide. In Bowen, J. P., Fett, A., and Hinchey, M. G., editors, ZUM’98: The Formal Specification Notation, Lecture Notes in Computer Science 1493, pages 233–249, Berlin Heidelberg New York. Springer Verlag.CrossRefGoogle Scholar
  26. Woodcock, J. and Davies, J. (1996). Using Z-Specification, Refinement, and Proof. Prentice Hall International Series in Computer Science. Prentice Hall Europe. Online: (last access 18/10/2001).

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Ralph Miarka
    • 1
  • John Derrick
    • 1
  • Eerke Boiten
    • 1
  1. 1.Computing LaboratoryUniversity of KentCanterburyUK

Personalised recommendations