Combining theorem proving and symbolic mathematical computing | Zendy

Karsten Homann | Zendy; Jacques Calmet | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Combining theorem proving and symbolic mathematical computing

Author(s) -

Karsten Homann,

Jacques Calmet

Publication year - 1995

Publication title -

lecture notes in computer science

Language(s) - English

Resource type - Book series

SCImago Journal Rank - 0.249

H-Index - 400

eISSN - 1611-3349

pISSN - 0302-9743

ISBN - 3-540-60156-2

DOI - 10.1007/3-540-60156-2_3

Subject(s) - computer science , automated theorem proving , symbolic computation , theoretical computer science , calculator , symbolic numeric computation , symbolic data analysis , representation (politics) , gas meter prover , algebraic number , algebra over a field , mathematical knowledge management , mathematical theory , knowledge representation and reasoning , computation , symbolic trajectory evaluation , knowledge base , algorithm , artificial intelligence , mathematics , mathematical proof , model checking , pure mathematics , procedural knowledge , law , mathematical analysis , operating system , geometry , quantum mechanics , political science , physics , politics

An intelligent mathematical environment must enable symbolic mathematical computation and sophisticated reasoning techniques on the underlying mathematical laws. This paper disscusses different possible levels of interaction between a symbolic calculator based on algebraic algorithms and a theorem prover. A high level of interaction requires a common knowledge representation of the mathematical knowledge of the two systems. We describe a model for such a knowledge base mainly consisting of type and algorithm schemata, algebraic algorithms and theorems.

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research