10th International Conference on
Artificial Intelligence and Symbolic Computation
AISC 2010
Paris, France, 5th6th July 2010
Conference ProgrammeMonday, July 5th 2010  10:5011:00 Welcome  Session 1 (11:0012:30, Chair: Elena Smirnova)11:0011:30  How to correctly prune tropical trees JeanVincent Loddo and Luca Saiu Abstract: We present _tropical games_, a generalization of combinatorial minmax games
based on tropical algebras. Our model breaks the traditional symmetry of
rational zerosum games where players have exactly opposed goals (min vs.
max), is more widely applicable than minmax and also supports a form of
pruning, despite it being less effective than alphabeta. Actually, minmax
games may be seen as particular cases where both the game and its dual are
tropical: when the dual of a tropical game is also tropical, the power of
alphabeta is completely recovered. We formally develop the model and prove
that the tropical pruning strategy is correct, then conclude by showing how
the problem of approximated parsing can be modeled as a tropical game,
profiting from pruning.
[Preprint] [SpringerLink]  11:3012:00  A mathematical model of the competition between acquired immunity and virus Mikhail Kolev Abstract: A mathematical model describing the interactions between
viral infection and acquired immunity is proposed. The model is formulated in terms of a system of partial integrodifferential bilinear equations. Results of numerical experiments are presented.
[SpringerLink]  12:0012:30  Artificial Intelligence Techniques on Biological Structures Athanasios Alexiou and Panayiotis Vlamos Abstract: We propose a CaseBased Reasoning System as the most suitable and stable solution to response and manage the information concerning sequential terms of biological structures and the implementation of pattern recognition on secondary structures. We will concentrate on the theoretical approaches and the fundamental principles for the design of a machinelearning system.
[PDF] [SpringerLink] 
 Lunch (12:3014:00)
 Invited Talk (14:0015:00)14:0015:00  The Challenges of Multivalued "Functions" James Davenport Abstract: Although, formally, mathematics is clear that a function is a singlevalued object, mathematical practice is looser, particularly with nth roots and various inverse functions. In this paper, we point out some of the looseness, and ask what the implications are, both for Artificial Intelligence and Symbolic Computation, of these practices. In doing so, we look at the steps necessary to convert existing texts into (a) rigorous statements (b) rigorously proved statements. In particular we ask whether there might be a constant "de Bruijn factor" as we make these texts more formal, and conclude
that the answer depends greatly on the interpretation being placed on the symbols.
[SpringerLink] 
 15:0015:30 Break
 Session 3 (15:3016:30, Chair: Bill Farmer)15:3016:00  Automated Reasoning and Presentation Support for Formalizing Mathematics in Mizar Josef Urban and Geoff Sutcliffe Abstract: This paper presents a combination of several automated reasoning and proof presentation tools with the Mizar system for formalization of mathematics. The combination forms an online service called
MizAR, similar to the SystemOnTPTP service for firstorder automated
reasoning. The main differences to SystemOnTPTP are the use of the
Mizar language that is oriented towards human mathematicians (rather
than the pure firstorder logic used in SystemOnTPTP), and setting the
service in the context of the large Mizar Mathematical Library of previous theorems, definitions, and proofs (rather than the isolated problems that are solved in SystemOnTPTP). These differences poses new
challenges and new opportunities for automated reasoning and for proof
presentation tools. This paper describes the overall structure of MizAR,
and presents the automated reasoning systems and proof presentation
tools that are combined to make MizAR a useful mathematical service.
[Preprint] [SpringerLink]  16:0016:30  Structured Formal Development with Quotient Types in Isabelle/HOL Maksym Bortin and Christoph Lüth Abstract: General purpose theorem provers provide sophisticated proof
methods, but lack some of the advanced structuring mechanisms found
in specification languages. This paper builds on previous work extending
the theorem prover Isabelle with such mechanisms. A way to build the
quotient type over a given base type and an equivalence relation on it,
and a generalised notion of folding over quotiented types is given as a
formalised highlevel step called a design tactic. The core of this paper
are four axiomatic theories capturing the design tactic. The applicability
is demonstrated by derivations of implementations for finite multisets
and finite sets from lists in Isabelle.
[SpringerLink] 
 Coffee Break (16:3017:00)
 Session 4 (17:0018:00, Chair: Dongming Wang)17:0017:30  From matrix interpretations over the rationals to matrix interpretations over the naturals Salvador Lucas Abstract: Matrix interpretations generalize linear polynomial interpretations and have been proved useful in the implementation of tools for
automatically proving termination of Term Rewriting Systems. In view
of the successful use of rational coefficients in polynomial interpretations, we have recently generalized traditional matrix interpretations (using natural numbers in the matrix entries) to incorporate real numbers.
However, existing results which formally prove that polynomials over the
reals are more powerful than polynomials over the naturals for proving
termination of rewrite systems failed to be extended to matrix interpretations. In this paper we get deeper into this problem. We show that,
under some conditions, it is possible to transform a matrix interpretation
over the rationals satisfying a set of symbolic constraints into a matrix
interpretation over the naturals (using bigger matrices) which still satisfies the constraints.
[Preprint] [SpringerLink]  17:3018:00  On Krawtchouk Transforms Philip Feinsilver and Rene Schott Abstract: Krawtchouk polynomials appear in a variety of contexts,
most notably as orthogonal polynomials and in coding theory via the
Krawtchouk transform. We present an operator calculus formulation of
the Krawtchouk transform that is suitable for computer implementation.
A positivity result for the Krawtchouk transform is shown. Then our approach is compared with the use of the Krawtchouk transform in coding
theory where it appears in MacWilliams' and Delsarte's theorems on
weight enumerators.
[SpringerLink]  18:0018:30  Some Notes upon "When does <T> equal sat(T)?" Yongbin Li Abstract: Given a regular set T in K[x], Lemaire et al. in ISSAC'08 give
a nice algebraic property: the regular set T generates its saturated ideal
if and only if it is primitive. We dirstly aim at giving a more direct proof
of the above result, generalizing the concept of primitivity of polynomials
and regular sets and presenting a new result which is equivalent to the
above property. On the other hand, based upon correcting an error of
the definition of Uset in AISC'06, we further develop some geometric
properties of triangular sets. To a certain extent, the relation between
the primitivity of T and its Uset is also revealed in this paper.
[SpringerLink] 

Tuesday, July 6th 2010  Invited Talk (9:3010:30)9:3010:30  The Dynamic Dictionary of Mathematical Functions Bruno Salvy Abstract: Mathematical tables have long been used by developers of computer algebra systems. Special functions are implemented in a system using formulas obtained in
these tables for the computation of their derivatives, series or asymptotic expansions, numerical evaluation, simplification, integral transforms,... Recently, more
and more powerful algorithms have been developed by the computer algebra community, so that nowadays, the flow can be reversed and mathematical tables can be
generated automatically for large classes of functions. The gains are obvious: a full
automation of the process that reduces the risk for typographical or other errors;
more flexibility and extra interactivity for the readers, not only in the navigation,
but also in the choice of the actual functions or formulas they need.
Our team has started the development of a Dynamic Dictionary of Mathematical Functions focusing on solutions of linear differential equations (available at
http://ddmf.msrinria.inria.fr/). This development raises several interesting
issues. Algorithmic ones obviously, but also more fundamental ones (what exactly
is needed to define a function?), or practical ones (how should the interaction between computer algebra systems and dynamic mathematical content on the web be
organized?). The talk will discuss these issues and present some of the choices that
were made in our design.
[SpringerLink] 
 Coffee Break (10:3011:00)
 Session 6 (11:0012:30, Chair: Jacques Carette)11:0011:30  Iterms in ordered resolution and superposition calculi : retrieving lost completeness Hicham Bensaid, Ricardo Caferra and Nicolas Peltier Abstract: Ordered resolution and superposition are the stateoftheart
proof procedures used in saturationbased theorem proving, for non equational and equational clause se
ts respectively.
In
this paper, we present extensions of these calculi that permit one to
reason about formulae built from terms
with integer exponents (or Iterms), a schematisation language
allowing one to denote infinite sequences of iterated terms.
We prove that the ordered resolution calculus is still refutationally complete
when applied on (non equational) clauses containing Iterms.
In the equational case, we prove that the superposition
calculus is not complete in the presence of Iterms and we devise a new inference
rule, called Hsuperposition, that restores completeness.
[SpringerLink]  11:3012:00  Instantiation of SMT problems modulo Integers Mnacho Echenim and Nicolas Peltier Abstract: Many decision procedures for SMT problems rely more or
less implicitly on an instantiation of the axioms defining the theories
under consideration, and differ by making use of the additional properties
of each theory, in order to increase efficiency. We present a new technique
for devising complete instantiation schemes on SMT problems over a
combination of linear arithmetic with another theory
T . The method
consists in first instantiating the arithmetic part of the formula, and
then getting rid of the remaining variables in the problem by using an
instantiation strategy which is complete for
T . We provide examples
evidencing that not only is this technique generic (in the sense that it
applies to a wide range of theories) but it is also efficient, even compared
to stateoftheart instantiation schemes for specific theories.
[Preprint] [SpringerLink]  12:0012:15  Efficiency of Automating Problem Solving in
MartinLöf's Type Theory Gohar Marikyan 
 Lunch (12:3014:00)
 Keynote Talk (14:0015:00)14:0015:00  A Revisited Perspective on Symbolic Mathematical Computing and Artificial Intelligence Jacques Calmet, John Campbell Abstract: We provide a perspective on the current state and possible future of
links between symbolic mathematical computing and artificial intelligence, on
the occasion of the 10th biennial conference (AISMC, later AISC) devoted to
those connections. It follows a similar perspective expressed for the first such
conference in 1992 and then revised and expanded 5 years later. Issues related
to the computational management of mathematical knowledge are highlighted.
[SpringerLink] 
 15:00 Closing Remarks 
