Integrating Computer Algebra into Proof Planning

Mechanized reasoning systems and computer algebra systems have different objectives. Their integration is highly desirable, since formal proofs often involve both of the two different tasks proving and calculating. Even more important, proof and computation are often interwoven and not easily separable. In this article we advocate an integration of computer algebra into mechanized reasoning systems at the proof plan level. This approach allows us to view the computer algebra algorithms as methods, that is, declarative representations of the problem-solving knowledge specific to a certain mathematical domain. Automation can be achieved in many cases by searching for a hierarchic proof plan at the method level by using suitable domain-specific control knowledge about the mathematical algorithms. In other words, the uniform framework of proof planning allows us to solve a large class of problems that are not automatically solvable by separate systems. Our approach also gives an answer t...

• Type: Journal
• Year: 1998
• Where: JAR
• Authors: Manfred Kerber, Michael Kohlhase, Volker Sorge
• Keywords: Algebra, JAR 1998, Proof Plan, Reasoning Systems