| |
PROGRAM
Wednesday, September 22
| 08:00 | Bus leaves from hotels |
| 08:30 - 09:00 | Registration |
| 09:00 - 09:15 | Opening |
| 09:15 - 10:15 | Invited talk: Helmut Schwichtenberg
Proof Search in Minimal Logic |
| 10:15 - 10:45 | Break |
| 10:45 - 12:30 |
A Paraconsistent Higher Order Logic
Jørgen Villadsen |
Abstraction within Partial Deduction for Linear Logic
Peep Küngas |
A Decision Procedure for Equality Logic with Uninterpreted Functions
Olga Tveretina |
|
| 12:30 - 13:45 | Lunch break |
| 13:45 - 15:30 |
Four Approaches to Automated Reasoning with Differential Algebraic Structures
Jesus Aransay, Clemens Ballarin, Julio Rubio |
Extending Finite Model Searching with Congruence Closure Computation
Jian Zhang, Hantao Zhang |
An Evolutionary Local Search Method for Incremental Satisfiability
M.B. Menaï |
|
| 15:30 - 16:00 | Break |
| 16:00 - 17:10 |
Combination of Nonlinear Terms in Interval Constraint Satisfaction Techniques
Laurent Granvilliers, Mina Ouabiba |
Proving and Constraint Solving in Computational Origami
Tetsuo Ida, Dorin Tepeneu, Bruno Buchberger, Judit Robu |
|
| 17:10 - 17:15 | Short break |
| 17:15 - 18:15 | Klaus Trümper: Logic Programming Tutorial |
| 18:15 | Bus to hotels |
Thursday, September 23
| 08:00 | Bus leaves from hotels |
| 8:30 - 9:30 | Invited talk: Zbigniew Stachniak
Finite Algebras and AI |
| 9:30 - 10:05 | On the Combination of Congruence Closure and Completion
Christelle Scharff, Leo Bachmair |
| 10:05 - 10:30 | Break |
| 10:30 - 12:00 |
Solving Equations Involving Sequence Variables and Sequence Functions
Temur Kutsia |
Verified Computer Algebra in ACL2 (Grobner Bases Computation)
I. Medina-Bulo, F. Palomo-Lozano, J.A. Alonso-Jimenez, J.L. Ruiz-Reina |
Polynomial Interpretations with Negative Coefficients
Nao Hirokawa, Aart Middeldorp |
|
| 12:15 - 13:45 | Lunch break |
| 13:45 - 14:55 |
New developments in Symmetry Breaking in Search Using Computational
Group Theory Tom Kelsey, Steve Linton, Colva Roney-Dougal |
Recognition of Whitehead-minimal Elements in Free Groups of Large Ranks
Alexei D. Miasnikov |
|
| 15:00 - 16:00 |
| Break and Poster Session |
Two Revision Methods Based on Constraints: Application to the Flooding Problem
Mahat Khelfallah, Belaid Benhamou |
Abstraction-Driven Verification of Array Programs
D. Deharbe, A. Imine, S. Ranise |
Singularities in Qualitative Reasoning
Bjorn Gottfried |
From a Computer Algebra Library to a System with an Equational Prover
Serge Mechveliani |
|
| 16:00 - 18:00 | Forest ramble + Détente |
| 18:15 | Bus to hotels |
| 19:30 | Conference dinner |
Friday, September 24
| 8:00 | Bus leaves from hotels |
| 8:30 - 9:30 | Invited talk: Alan Bundy
Planning and Patching Proofs |
| 9:30 - 10:05 |
Generic Hermitian Quantifier Elimination
Andreas Dolzmann, Lorenz A. Gilch |
| 10:05 - 10:35 | Break |
| 10:35 - 11:45 |
Algorithm-Supported Mathematical Theory Explanation: A Personal View and Strategy
Bruno Buchberger |
An Expert System on Detection, Evaluation and Treatment of Hypertension
E. Roanes-Lozano, E. Lopez-Vidriero Jr., L.M. Laita, E.
Lopez-Vidriero,
V. Maojo, E. Roanes-Macias |
|
| 12:00 - 13:30 | Lunch break |
| 13:30 - 14:30 | Invited talk: Markus Rosenkranz
The Algorithmization of Physics: Math Between Science and
Engineering |
| 14:30 - 15:30 | Panel discussions |
| 15:30 - 16:00 | Break |
| 16:00 - 17:00 | Conclusing discussion |
| 17:15 | Bus to hotels |
INVITED SPEAKERS
- Alan Bundy (University of Edinburgh, Edinburgh, UK)
Planning and Patching Proofs
- Markus Rosenkranz (RICAM Institute, Austrian Academy of Sciences, Linz, Austria)
The Algorithmization of Physics: Math Between Science and
Engineering
- Helmut Schwichtenberg (Ludwig-Maximilian University, Munich, Germany)
Proof Search in Minimal Logic
- Zbigniew Stachniak (York University, Toronto, Canada)
Finite Algebras and AI
ACCEPTED PAPERS
- A Paraconsistent Higher Order Logic
Jørgen Villadsen
- Abstraction within Partial Deduction for Linear Logic
Peep Küngas
- A Decision Procedure for Equality Logic with Uninterpreted Functions
Olga Tveretina
- Generic Hermitian Quantifier Elimination
Andreas Dolzmann, Lorenz A. Gilch
- Extending Finite Model Searching with Congruence Closure Computation
Jian Zhang, Hantao Zhang
- On the Combination of Congruence Closure and Completion
Christelle Scharff, Leo Bachmair
- Combination of Nonlinear Terms in Interval Constraint Satisfaction Techniques
Laurent Granvilliers, Mina Ouabiba
- Proving and Constraint Solving in Computational Origami
Tetsuo Ida, Dorin Tepeneu, Bruno Buchberger, Judit Robu
- Two Revision Methods Based on Constraints: Application to the Flooding Problem
Mahat Khelfallah, Belaid Benhamou
- An Evolutionary Local Search Method for Incremental Satisfiability
M.B. Menaï
- Solving Equations Involving Sequence Variables and Sequence Functions
Temur Kutsia
- Verified Computer Algebra in ACL2 (Grobner Bases Computation)
I. Medina-Bulo, F. Palomo-Lozano, J.A. Alonso-Jimenez, J.L. Ruiz-Reina
- Abstraction-Driven Verification of Array Programs
D. Deharbe, A. Imine, S. Ranise
- Polynomial Interpretations with Negative Coefficients
Nao Hirokawa, Aart Middeldorp
- From a Computer Algebra Library to a System with an Equational Prover
Serge Mechveliani
- New developments in Symmetry Breaking in Search Using Computational Group Theory
Tom Kelsey, Steve Linton, Colva Roney-Dougal
- Recognition of Whitehead-minimal Elements in Free Groups of Large Ranks
Alexei D. Miasnikov
- Four Approaches to Automated Reasoning with Differential Algebraic Structures
Jesus Aransay, Clemens Ballarin, Julio Rubio
- Algorithm-Supported Mathematical Theory Explanation: A Personal View and Strategy
Bruno Buchberger
- Singularities in Qualitative Reasoning
Bjorn Gottfried
- An Expert System on Detection, Evaluation and Treatment of Hypertension
E. Roanes-Lozano, E. Lopez-Vidriero Jr., L.M. Laita, E. Lopez-Vidriero, V. Maojo, E. Roanes-Macias
|
