Two Proof Systems for Peirce Algebras

  • Renate A. Schmidt
  • Ewa Orłowska
  • Ullrich Hustadt
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3051)


This paper develops and compares two tableaux-style proof systems for Peirce algebras. One is a tableau refutation proof system, the other is a proof system in the style of Rasiowa-Sikorski.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Brink, C.: Boolean modules. J. Algebra 71(2), 291–313 (1981)zbMATHCrossRefMathSciNetGoogle Scholar
  2. 2.
    Brink, C., Britz, K., Schmidt, R.A.: Peirce algebras. Formal Aspects of Computing 6(3), 339–358 (1994)zbMATHCrossRefGoogle Scholar
  3. 3.
    Britz, K.: Relations and programs. Master’s thesis, Univ. Stellenbosch, South Africa (1988)Google Scholar
  4. 4.
    Dawson, J., Goré, R.: A mechanised proof system for relation algebra using display logic. In: Dix, J., Fariñas del Cerro, L., Furbach, U. (eds.) JELIA 1998. LNCS (LNAI), vol. 1489, pp. 264–278. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  5. 5.
    de Rijke, M.: Extending Modal Logic. PhD thesis, Univ. Amsterdam (1993)Google Scholar
  6. 6.
    Düntsch, I., Orlowska, E.: A proof system for contact relation algebras. J. Philos. Logic 29, 241–262 (2000)zbMATHCrossRefMathSciNetGoogle Scholar
  7. 7.
    Fitting, M.: First-Order Logic and Automated Theorem Proving. Texts and Monographs in Computer Science. Springer, Heidelberg (1990)zbMATHGoogle Scholar
  8. 8.
    Gargov, G., Passy, S.: A note on Boolean modal logic. In: Petkov, P.P. (ed.) Mathematical Logic: Proc. 1988 Heyting Summerschool, pp. 299–309. Plenum Press, New York (1990)Google Scholar
  9. 9.
    Goré, R.: Cut-free display calculi for relation algebras. In: van Dalen, D., Bezem, M. (eds.) CSL 1996. LNCS, vol. 1258, pp. 198–210. Springer, Heidelberg (1997)Google Scholar
  10. 10.
    Hennessy, M.C.B.: A proof-system for the first-order relational calculus. J. Computer and System Sci. 20, 96–110 (1980)zbMATHCrossRefMathSciNetGoogle Scholar
  11. 11.
    Hustadt, U., Schmidt, R.A.: MSPASS: Modal reasoning by translation and first-order resolution. In: Dyckhoff, R. (ed.) TABLEAUX 2000. LNCS (LNAI), vol. 1847, pp. 67–71. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  12. 12.
    Lyndon, R.C.: The representation of relational algebras. Ann. Math. 51, 707–729 (1950)CrossRefMathSciNetGoogle Scholar
  13. 13.
    MacCaull, W., Orlowska, E.: Correspondence results for relational proof systems with applications to the Lambek calculus. Studia Logica 71, 279–304 (2002)CrossRefMathSciNetGoogle Scholar
  14. 14.
    Maddux, R.D.: A sequent calculus for relation algebras. Ann. Pure Applied Logic 25, 73–101 (1983)zbMATHCrossRefMathSciNetGoogle Scholar
  15. 15.
    Monk, J.D.: On representable relation algebras. Michigan Math. J. 11, 207–210 (1964)zbMATHCrossRefMathSciNetGoogle Scholar
  16. 16.
    Nellas, K.: Reasoning about sets and relations: A tableaux-based automated theorem prover for Peirce logic. Master’s thesis, Univ. Manchester, UK (2001)Google Scholar
  17. 17.
    Orlowska, E.: Relational formalisation of nonclassical logics. In: Brink, C., Kahl, W., Schmidt, G. (eds.) Relational Methods in Computer Science, Advances in Computing, pp. 90–105. Springer, Wien (1997)Google Scholar
  18. 18.
    Rasiowa, H., Sikorski, R.: The Mathematics of Metamathematics. Polish Scientific Publ., Warsaw (1963)zbMATHGoogle Scholar
  19. 19.
    Schmidt, R.A.: Algebraic terminological representation. Master’s thesis, Univ. Cape Town, South Africa (1991); Available as Technical Report MPI-I- 91-216, Max-Planck-Institut für Informatik, Saarbrücken, GermanyGoogle Scholar
  20. 20.
    Schmidt, R.A.: Relational grammars for knowledge representation. In: Böttner, M., Thümmel, W. (eds.) Variable-Free Semantics. Artikulation und Sprache, vol. 3, pp. 162–180. Secolo Verlag, Osnabrück (2000)Google Scholar
  21. 21.
    Schmidt, R.A., Hustadt, U.: Mechanised reasoning and model generation for extended modal logics. In: de Swart, H., Orłowska, E., Schmidt, G., Roubens, M. (eds.) Theory and Applications of Relational Structures as Knowledge Instruments. LNCS, vol. 2929, pp. 38–67. Springer, Heidelberg (2003) (to appear)CrossRefGoogle Scholar
  22. 22.
    Schönfeld, W.: Upper bounds for a proof-search in a sequent calculus for relational equations. Z. Math. Logik Grundlagen Math. 28, 239–246 (1982)zbMATHCrossRefGoogle Scholar
  23. 23.
    Smullyan, R.M.: First Order Logic. Springer, Berlin (1971)Google Scholar
  24. 24.
    Tarski, A.: On the calculus of relations. J. Symbolic Logic 6(3), 73–89 (1941)zbMATHCrossRefMathSciNetGoogle Scholar
  25. 25.
    Wadge, W.W.: A complete natural deduction system for the relational calculus. Theory of Computation Report 5, Univ. Warwick (1975)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Renate A. Schmidt
    • 1
  • Ewa Orłowska
    • 2
  • Ullrich Hustadt
    • 3
  1. 1.University of ManchesterUK
  2. 2.National Institute of TelecommunicationsWarsaw
  3. 3.University of LiverpoolUK

Personalised recommendations