Home | Quick Search | Advanced Search | Bibliography submission | Bibliography submission using bibtex | Bibliography submission using bibtex file | Links | Help | Internal

Details:

   
TitleContext aware calculation and deduction. Ring equalities via Gr\"obner bases in Isabelle.
Author(s) Amine Chaieb, Makarius Wenzel
TypeBook, Chapter in Book, Conference Proceeding
AbstractWe address some aspects of a system architecture for mathematical assistants that integrates 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 latter is extended 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 operate on abstract 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öbner Bases.
ISBN978-3-540-73083-5/pbk
URL http://link.springer.com/chapter/10.1007%2F978-3-540-73086-6_3
LanguageEnglish
Pages27--39
PublisherBerlin: Springer
Year2007
Edition0
Translation No
Refereed No
Webmaster