A sequent calculus machine for symbolic computation systems
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.
KeywordsFunction Symbol Natural Deduction Sequent Calculus Valid Sequent Atomic Sequent
Unable to display preview. Download preview PDF.
- 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
- Paepcke, A. (1993): Object-oriented programming, the CLOS perspective. MIT Press, Cambridge, MA.Google Scholar