# A sequent calculus machine for symbolic computation systems

## 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.

## Keywords

Function Symbol Natural Deduction Sequent Calculus Valid Sequent Atomic Sequent## 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.CrossRefGoogle Scholar
- 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).Google Scholar
- Cioni, G., Colagrossi, A., Miola, A. (1995): A sequent calculus for symbolic computation systems. J. Symb. Comput. 19: 175–199.MathSciNetMATHCrossRefGoogle Scholar
- 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).CrossRefGoogle Scholar
- Gallier, J. H. (1986): Logic for computer science. Harper and Row, New York.MATHGoogle Scholar
- Paepcke, A. (1993): Object-oriented programming, the CLOS perspective. MIT Press, Cambridge, MA.Google Scholar
- Suppes, P., Takahashi, S. (1989): An interactive calculus theorem-prover for continuity properties. J. Symb. Comput. 7: 573–590.MathSciNetMATHCrossRefGoogle Scholar