16th Symposium on the Integration of

Symbolic Computation and Mechanised Reasoning

Symbolic Computation and Mechanised Reasoning

6-7 July 2009, Joint with CICM'09, Ontario, Canada.

8:30-9:30

Invited talk:
Computational Logic and Continuous Mathematics, Pure and Applied

Rob Arthan (Director of Lemma 1, developer of ProofPower)

Rob Arthan (Director of Lemma 1, developer of ProofPower)

9:30-10:00

Combining Coq and Gappa for Certifying Floating-Point Programs

Sylvie Boldo, Jean-Christophe Filliâtre and Guillaume Melquiond.

Sylvie Boldo, Jean-Christophe Filliâtre and Guillaume Melquiond.

10:00-10:30

ACL2 verification of simplicial degeneracy programs in the Kenzo system

Francisco-Jesus Martin-Mateos, Julio Rubio and Jose-Luis Ruiz-Reina.

Francisco-Jesus Martin-Mateos, Julio Rubio and Jose-Luis Ruiz-Reina.

10:30-11:00

break

11:00-11:30

Exploring a Quantum Theory with Graph Rewriting and Computer Algebra

Aleks Kissinger.

Aleks Kissinger.

11:30-12:00

A Comparison of Equality in Computer Algebra and Correctness in Mathematical Pedagogy

Russell Bradford, James Davenport and Christopher Sangwin.

Russell Bradford, James Davenport and Christopher Sangwin.

12:00-3:00

Lunch

3:00-4:00

Invited talk:Math Handwriting Recognition in Windows 7 and Its Benefits

Marko Panic

Marko Panic

4:00-4:30

break

4:30-4:45

Computing Ranking and Unranking Functions for BDDs

Paul Tarau and Brenda Luderman.

Paul Tarau and Brenda Luderman.

4:45-5:00

The Naproche System

Daniel Kuehlwein, Marcos Cramer, Peter Koepke and Bernhard Schröder.

Daniel Kuehlwein, Marcos Cramer, Peter Koepke and Bernhard Schröder.

5:00-5:30

Reasoning with Generic Cases in the Arithmetic of Abstract Matrices

Alan Sexton, Volker Sorge and Stephen Watt.

Alan Sexton, Volker Sorge and Stephen Watt.

9:00-9:30

Combined Decision Techniques for the Existential Theory of the Reals

Grant Olney Passmore and Paul Jackson.

Grant Olney Passmore and Paul Jackson.

9:30-10:00

Invariant Properties of Third-Order Non-Hyperbolic Linear Partial Differential Operators

Ekaterina Shemyakova.

Ekaterina Shemyakova.

10:00-10:30

A Groupoid of Data Transformations

Paul Tarau.

Paul Tarau.

10:30-11:00

break

11:00-11:30

Algorithms for the Functional Decomposition of Laurent Polynomials

Stephen Watt.

Stephen Watt.

11:30-12:00

Conservative retractions of propositional logic theories by means of boolean derivatives. Theoretical foundations

Gonzalo A. Aranda-Corral, Joaquín Borrego-Díaz and M. Magdalena Fernández-Lebrón.

Gonzalo A. Aranda-Corral, Joaquín Borrego-Díaz and M. Magdalena Fernández-Lebrón.

12:00-3:00

Lunch

3:00-4:00

Invited Talk:Abstraction-Based Information Technology: A Framework for Open Mechanized Reasoning

Prof. Jacques Calmet (Universität Karlsruhe)

Prof. Jacques Calmet (Universität Karlsruhe)

4:00-4:30

break

4:30-4:45

Reusing Proofs in a Mathematical Library

Ivan Noyer and Renaud Rioboo.

Ivan Noyer and Renaud Rioboo.

4:45-5:00

Reflecting Data: Formally Correct Results for Efficient (and Dirty) Algorithms

Lucas Dixon.

Lucas Dixon.

5:00-6:00

Calculemus Business Meeting