Program

Thursday December 11th

12:00  [60'] Register

13:00  [60'] Lunch

14:00  [30'] Opening

14:30  [30'] Regular Paper
Obtaining an ACL2 specification from an Isabelle/HOL theory.
Jesus Aransay-Azofra, Jose Divasón, Jónathan Heras, Laureano Lambán, María Vico Pascual, Ángel Luis Rubio and Julio Rubio.

15:00  [30'] Regular Paper
Multivalued elementary functions in computer-algebra systems.
David Jeffrey.

15:30  [30'] Coffee Break

16:00  [30'] Regular Paper
Using Representation Theorems for Proving Polynomials Non-negative.
Salvador Lucas.

16:30  [30'] Regular Paper
A Rule-Based Expert System for vaginal cytology diagnosis.
Carlos Gamallo-Chicano, Eugenio Roanes-Lozano and Carlos Gamallo-Amat.

Friday December 12th

9:30  [60'] Invited Talk
Combining Systems for Mathematical Creativity.
Volker Sorge.

10:30  [30'] Regular Paper
Models for Logics and Conditional Constraints in Automated Proofs of Termination.
Salvador Lucas and Jose Meseguer.

11:00  [30'] Coffee Break

11:30  [30'] Regular Paper
A direct propagation method in singly connected causal belief networks with conditional distributions for all causes.
Oumaima Boussarsar, Imen Boukhris and Zied Elouedi.

12:00  [30'] Regular Paper
From Declarative Set Constraint Models to "Good" SAT Instances.
Frederic Lardeux and Eric Monfroy.

12:30  [30'] Regular Paper
A Mathematical Hierarchy of Sudoku Puzzles and its Computation by Boolean Gröbner.
Shutaro Inoue and Yosuke Sato.

13:00  [90'] Lunch

14:30  [30'] Regular Paper
A simple GUI for developing applications that use mathematics software.
Eugenio Roanes-Lozano and Antonio Hernando.

15:00  [30'] Regular Paper
Conformant Planning as a Case Study of Incremental QBF Solving.
Uwe Egly, Martin Kronegger, Florian Lonsing and Andreas Pfandler.

15:30  [30'] Coffee Break

16:00  [30'] Regular Paper
Dynamic symmetry breaking in itemset mining.
Belaid Benhamou.

16:30  [30'] Regular Paper
A distance-based decision in the credal level.
Amira Essaid, Arnaud Martin, Gregory Smits and Boutheina Ben Yaghlane.

17:00  [45'] Bussiness Meeting

18:30 [120'] Social Program

20:30 Gala Dinner

Saturday December 13th

10:00  [60'] Invited Talk
Proving and Computing: Applying Automated Reasoning to the Verification of Symbolic Computation Systems.
José-Luis Ruiz-Reina.

11:00  [30'] Regular Paper
Computing envelopes in dynamic geometry environments.
Francisco Botana and Tomas Recio.

11:30  [30'] Coffee Break

12:00  [30'] Regular Paper
Rational Conchoid and Offset Constructions: Algorithms and Implementation.
Juana Sendra, David Gómez and Valerio Morán.

12:30  [30'] Regular Paper
Algorithmic Aspects of Theory Blending.
Tarek Richard Besold, Maricarmen Martinez, Ulf Krumnack, Alan Smaill, Martin Schmidt, Ahmed M. H. Abdel-Fattah, Helmar Gust, Kai-Uwe Kuehnberger, Alison Pease and Markus Guhe.

13:00 Closing Ceremony