10th International Conference on
Artificial Intelligence and Symbolic Computation
AISC 2010

Paris, France, 5th-6th July 2010

Conference Programme

Monday, July 5th 2010

10:50-11:00 Welcome

Session 1 (11:00-12:30, Chair: Elena Smirnova)

11:00-11:30How to correctly prune tropical trees
Jean-Vincent Loddo and Luca Saiu

Abstract: We present _tropical games_, a generalization of combinatorial min-max games based on tropical algebras. Our model breaks the traditional symmetry of rational zero-sum games where players have exactly opposed goals (min vs. max), is more widely applicable than min-max and also supports a form of pruning, despite it being less effective than alpha-beta. Actually, min-max 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 alpha-beta 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:30-12: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 integro-differential bilinear equations. Results of numerical experiments are presented.


12:00-12:30Artificial Intelligence Techniques on Biological Structures
Athanasios Alexiou and Panayiotis Vlamos

Abstract: We propose a Case-Based 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 machine-learning system.

[PDF] [SpringerLink]

Lunch (12:30-14:00)

Invited Talk (14:00-15:00)

14:00-15:00The Challenges of Multivalued "Functions"
James Davenport

Abstract: Although, formally, mathematics is clear that a function is a single-valued object, mathematical practice is looser, particularly with n-th 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.


15:00-15:30 Break

Session 3 (15:30-16:30, Chair: Bill Farmer)

15:30-16:00Automated 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 first-order automated reasoning. The main differences to SystemOnTPTP are the use of the Mizar language that is oriented towards human mathematicians (rather than the pure first-order 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:00-16: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 high-level 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.


Coffee Break (16:30-17:00)

Session 4 (17:00-18:00, Chair: Dongming Wang)

17:00-17:30From 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:30-18:00On 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.


18:00-18: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 U-set 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 U-set is also revealed in this paper.


Tuesday, July 6th 2010

Invited Talk (9:30-10:30)

9:30-10: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.msr-inria.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.


Coffee Break (10:30-11:00)

Session 6 (11:00-12:30, Chair: Jacques Carette)

11:00-11:30 I-terms in ordered resolution and superposition calculi : retrieving lost completeness
Hicham Bensaid, Ricardo Caferra and Nicolas Peltier

Abstract: Ordered resolution and superposition are the state-of-the-art proof procedures used in saturation-based 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 I-terms), 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 I-terms. In the equational case, we prove that the superposition calculus is not complete in the presence of I-terms and we devise a new inference rule, called H-superposition, that restores completeness.


11:30-12:00Instantiation 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 state-of-the-art instantiation schemes for specific theories.

[Preprint] [SpringerLink]

12:00-12:15Efficiency of Automating Problem Solving in Martin-Löf's Type Theory
Gohar Marikyan

Lunch (12:30-14:00)

Keynote Talk (14:00-15:00)

14:00-15: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.


15:00 Closing Remarks