Context Aware Calculation and Deduction

We address some aspects of a proposed system architecture for mathematical assistants, integrating calculations and deductions by common infrastructure within the Isabelle theorem proving environment. Here calculations may refer to arbitrary extra-logical mechanisms, operating on the syntactic structure of logical statements. Deductions are devoid of any computational content, but driven by procedures external to the logic, following to the traditional “LCF system approach”. The latxtended towards explicit dependency on abstract theory contexts, with separate mechanisms to interpret both logical and extra-logical content uniformly. Thus we are able to implement proof methods that operbstract theories and a range of particular theory interpretations. Our approach is demonstrated in Isabelle/HOL by a proof-procedure for generic ring equalities via Gr¨obner Bases.

• Type: Conference
• Year: 2007
• Where: MKM
• Authors: Amine Chaieb, Makarius Wenzel
• Keywords: Abstract Theory Contexts, Arbitrary Extra-logical Mechanisms, MKM 2007, Theorem Proving Environment