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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Andreka H. and Nemeti I. (1996) Axiomatization of identity-free equations valid in relation algebras. Algebra Universalis 35:256–264
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
Dawson J.E. and Gore R. (1998) A mechanised proof system for relation algebra using display logic.JELIA’98, LNAI 1489:264–278
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
Frias M. and Orlowska E. (1998) Equational reasoning in non-classical logics. Journ. of Applied Non-Class. Logics 8 (1–2):27–66
Gordeev L. (1995) Cut free formalization of logic with finitely many variables. CSL’94, LNCS 933:136–150
Gordeev L. (1999) Variable compactness in 1-order logic. Journ. of IGPL 7:327–357
Gordeev L. (2000) Finite proof theory: basic result. To appear in Archive for Math. Logic
Gore R. (1997) Cut-free display calculi for relation algebras. CSL’96, LNCS 1249:198–210
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
Henkin L. (1967) Logical systems containing only a finite number of symbols. Les Presses de l’Universite Montreal
Hindley J.R. (1969) An abstract form of Church-Rosser theorem I. Journ. of Symb. Logic 34:545–560
Maddux R. (1989) Finitary algebraic logic. Zeit. f. math. Log. Grundl. d. Math. 35:321–332
Maddux R. (1989) Nonfinite axiomatizability results for cylindric and relation algebras. Journ. of Symb. Logic 54:951–974
Orlowska E. (1988) Relational interpretation of modal logics. In: Andreka H., Monk D. and Nemeti I. (eds) Algebraic Logic, North-Holland, 443–471
Orlowska E. (1992) Relational proof system for relevant logic. Journ. of Symb. Logic 57:1425–1440
Orlowska E. (1995) Relational proof systems for modal logics. In: Wansing H. (ed) Proof theory of modal logics, Kluwer, 55–57
Sinz C. (1998) Untersuchung und Implementation der RPCn Reduktionskalküle. Studienarbeit Universität Tübingen
Sinz C. (2000) System description: ARA — an automatic theorem prover for relation algebras. CADE-17 (to appear)
Tarski A. and Givant S. (1987) A formalization of set theory without variables. AMS Coll. Publ. 41
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights 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