Abstract
In literature many proposals for mathematical problem solving can be found, those allowing for manipulating the properties of the mathematical objects involved. If these properties have been expressed in first-order logic language, this task can be performed by using automated deduction methods developed in the frame of natural deduction (see, e.g., Beeson 1989, Suppes and Takahashi 1989) with the advantage of a friendly use. In this frame a method for reasoning on properties, based on a sequent calculus, has been developed and proposed in 1997, 1995; its characteristics, that make it well suited to be embedded in a symbolic mathematical computation system, are also stressed in those papers, also considering different kinds of problems to be approached. In fact, such a sequent calculus is a single method for performing extended deduction, i.e., for solving verificative, generative, and abductive problems in one methodological and integrated way.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Beeson, M. J. (1989): Logic and computation in mathpert: an expert system for learning mathematics. In: Kaltofen, E., Watt, S. M. (eds.): Computers and mathematics. Springer, Berlin Heidelberg New York Tokyo, pp. 202–214.
Cioni, G., Colagrossi, A., Miola, A. (1992): A desk-top sequent calculus machine. In: Calmet, J., Campbell, J. A. (eds.): Artificial intelligence and symbolic mathematical computation. Springer, Berlin Heidelberg New York Tokyo, pp. 224–236 (Lecture notes in computer science, vol. 737).
Cioni, G., Colagrossi, A., Miola, A. (1995): A sequent calculus for symbolic computation systems. J. Symb. Comput. 19: 175–199.
Cioni, G., Colagrossi, A., Miola, A. (1997): Deduction and abduction using a sequent calculus. In: Miola, A., Temperini, M. (eds.): Advances in the design of symbolic computation systems. Springer, Wien New York, pp. 198–216 (this volume).
Gallier, J. H. (1986): Logic for computer science. Harper and Row, New York.
Paepcke, A. (1993): Object-oriented programming, the CLOS perspective. MIT Press, Cambridge, MA.
Suppes, P., Takahashi, S. (1989): An interactive calculus theorem-prover for continuity properties. J. Symb. Comput. 7: 573–590.
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1997 Springer-Verlag Wien
About this chapter
Cite this chapter
Bertoli, P., Cioni, G., Colagrossi, A., Terlizzi, P. (1997). A sequent calculus machine for symbolic computation systems. In: Miola, A., Temperini, M. (eds) Advances in the Design of Symbolic Computation Systems. Texts and Monographs in Symbolic Computation. Springer, Vienna. https://doi.org/10.1007/978-3-7091-6531-7_13
Download citation
DOI: https://doi.org/10.1007/978-3-7091-6531-7_13
Publisher Name: Springer, Vienna
Print ISBN: 978-3-211-82844-1
Online ISBN: 978-3-7091-6531-7
eBook Packages: Springer Book Archive