Skip to main content
SpringerLink
Log in

Proof Systems in Relation Algebra

  • Chapter
Relational Methods for Computer Science Applications

Part of the book series: Studies in Fuzziness and Soft Computing ((STUDFUZZ,volume 65))

Abstract

We expose two different notions of validity in relation algebras: one is based on Tarski’s equational calculus (say, ‘T-validity’), and the other arises by the canonical 1-order translation from the ordinary semantic validity (say, ‘t-validity’). In the first section we characterize both validities via provability in finite-variable logics and the corresponding cutfree derivability in formula-rewriting 1-order systems. In the second section we characterize T-validity via derivability in a suitable cutfree term-rewriting system in the basic algebraic language, which is equivalent to the algebraic display calculus of Gore. In the third section we address 1-order 2-variable decidability and validity using both methods.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Andreka H. and Nemeti I. (1996) Axiomatization of identity-free equations valid in relation algebras. Algebra Universalis 35:256–264

    Article  MathSciNet  MATH  Google Scholar 

  2. Chin L. and Tarski A. (1951) Distributive and modular laws in the arithmetic of relation algebras. Univ. of Calif. Publ. in Math 9:341–384

    MathSciNet  Google Scholar 

  3. Dawson J.E. and Gore R. (1998) A mechanised proof system for relation algebra using display logic.JELIA’98, LNAI 1489:264–278

    MathSciNet  Google Scholar 

  4. Frias M. and Orlowska E. (1995) A proof system for fork algebras and its applications to reasoning in logics based on intuitionism. Logique et Analyse 150–151–152:239–284

    MathSciNet  Google Scholar 

  5. Frias M. and Orlowska E. (1998) Equational reasoning in non-classical logics. Journ. of Applied Non-Class. Logics 8 (1–2):27–66

    MathSciNet  MATH  Google Scholar 

  6. Gordeev L. (1995) Cut free formalization of logic with finitely many variables. CSL’94, LNCS 933:136–150

    MathSciNet  Google Scholar 

  7. Gordeev L. (1999) Variable compactness in 1-order logic. Journ. of IGPL 7:327–357

    Article  MathSciNet  MATH  Google Scholar 

  8. Gordeev L. (2000) Finite proof theory: basic result. To appear in Archive for Math. Logic

    Google Scholar 

  9. Gore R. (1997) Cut-free display calculi for relation algebras. CSL’96, LNCS 1249:198–210

    MathSciNet  Google Scholar 

  10. Grädel E., Kolaitis P. and Vardi M. (1997) On the decision problem for twovariable first-order logic. Bull. of Symb. Logic 3:53–69

    Article  MATH  Google Scholar 

  11. Henkin L. (1967) Logical systems containing only a finite number of symbols. Les Presses de l’Universite Montreal

    Google Scholar 

  12. Hindley J.R. (1969) An abstract form of Church-Rosser theorem I. Journ. of Symb. Logic 34:545–560

    Article  MathSciNet  MATH  Google Scholar 

  13. Maddux R. (1989) Finitary algebraic logic. Zeit. f. math. Log. Grundl. d. Math. 35:321–332

    Article  MathSciNet  MATH  Google Scholar 

  14. Maddux R. (1989) Nonfinite axiomatizability results for cylindric and relation algebras. Journ. of Symb. Logic 54:951–974

    Article  MathSciNet  MATH  Google Scholar 

  15. Orlowska E. (1988) Relational interpretation of modal logics. In: Andreka H., Monk D. and Nemeti I. (eds) Algebraic Logic, North-Holland, 443–471

    Google Scholar 

  16. Orlowska E. (1992) Relational proof system for relevant logic. Journ. of Symb. Logic 57:1425–1440

    Article  MathSciNet  MATH  Google Scholar 

  17. Orlowska E. (1995) Relational proof systems for modal logics. In: Wansing H. (ed) Proof theory of modal logics, Kluwer, 55–57

    Google Scholar 

  18. Sinz C. (1998) Untersuchung und Implementation der RPCn Reduktionskalküle. Studienarbeit Universität Tübingen

    Google Scholar 

  19. Sinz C. (2000) System description: ARA — an automatic theorem prover for relation algebras. CADE-17 (to appear)

    Google Scholar 

  20. Tarski A. and Givant S. (1987) A formalization of set theory without variables. AMS Coll. Publ. 41

    MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. WSI für Informatik, Logik und Sprachtheorie, Tübingen University, Köstlinstr. 6, D-72074, Tübingen, Germany

    Lev Gordeev

Authors
  1. Lev Gordeev
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Institute of Telecommunications, ul. Szachowa 1, 04-894, Warsaw, Poland

    Ewa Orłowska

  2. Institute of Informatics, University of Warsaw, ul. Banacha 2, 02-097, Warsaw, Poland

    Andrzej Szałas

Rights and permissions

Reprints and permissions

Copyright information

© 2001 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Gordeev, L. (2001). Proof Systems in Relation Algebra. In: Orłowska, E., Szałas, A. (eds) Relational Methods for Computer Science Applications. Studies in Fuzziness and Soft Computing, vol 65. Physica, Heidelberg. https://doi.org/10.1007/978-3-7908-1828-4_13

Download citation

  • DOI: https://doi.org/10.1007/978-3-7908-1828-4_13

  • Publisher Name: Physica, Heidelberg

  • Print ISBN: 978-3-662-00362-6

  • Online ISBN: 978-3-7908-1828-4

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation