|
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 |
|