Abstract
Walicki and Meldal have defined a calculus DEQ (“Disjunctive EQuational calculus”) for reasoning about nondeterministic operators when specifying nondeterministic systems in an equation-oriented style.
A variant of DEQ, the calculus DEQ * for axiomatic equality theories with cut-like rules introducing as cut formulas only the negative equalities of a specific axiom, is constructed. For pure positive specific axioms (i.e. with empty antecedents) and for so called non-contrary equality theories DEQ * does not contain cut-like rules at all. The variant of the calculus DEQ * without structural rules of contraction and exchange is constructed. A simple cut-elimination procedure for axiomatic equality theories is presented.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
S. Feferman, Lectures on Proof Theory, LNM, 70, Springer, 1969.
S. Kanger, A simplified proof method for elementary logic. Comput. Progr. and Formal Systems, North-Holland, Amsterdam, 87–94, 1963.
S. Meldal, An abstract axiomatization of pointer types, in Proc. of the 22nd Annual Hawaii International Conference on System Sciences, B.D. Shriver (ed.), IEEE Computer Society Press, vol. 2, 129–134, 1989.
A. Pliuškevičienė, Elimination of cut-type rules in axiomatic theories with equality. Seminars in mathematics V.A. Steklov Mathem. Institute, Leningrad, 16, 90–94, 1971.
A. Pliuškevičienė, Specialization of the use of axioms for deduction search in axiomatic theories with equality, Seminars in mathematics V.A. Steklov Mathem. Institute, Leningrad, J. Soviet Math. 1, 110–116, 1973.
A. Pliuškevičienė, A sequential variant of R.M.Robinson's arithmetic system not containing cut rules. Proc. Steklov Inst. Math., Leningrad, 121, 121–150, 1972.
R. Pliuškevičius, Sequential variant of the calculus of constructive logic for normal formulas. Proc. Steklov Inst. Math., 98, 175–229, 1968.
M. Rogava, Sequential variants of applied predicate calculi without structural deductive rules. Proc. Steklov Inst. Math. 121, 136–164, 1972.
M. Walicki, Algebraic Specifications of nondeterminism, Ph. D thesis, University of Bergen, 1993.
M. Walicki, S. Meldal, A complete calculus for the multialgebraic and functional semantics of nondeterminism, (submitted for publ.) 1993.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Pliuškevičienė, A., Pliuškevičius, R., Walicki, M., Meldal, S. (1994). On specialization of derivations in axiomatic equality theories. In: Nerode, A., Matiyasevich, Y.V. (eds) Logical Foundations of Computer Science. LFCS 1994. Lecture Notes in Computer Science, vol 813. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58140-5_28
Download citation
DOI: https://doi.org/10.1007/3-540-58140-5_28
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58140-6
Online ISBN: 978-3-540-48442-4
eBook Packages: Springer Book Archive