Synasc 2006  Invited talks 
Invited speakers Ajith Abraham, South Korea Talk: Tuning Evolutionary Algorithm Performance Using Nature Inspired Heuristics Bruno Buchberger, Austria http://www.risc.unilinz.ac.at/people/buchberger Talk: Mathematical Theory Exploration Abstract: Mathematics is characterized by its method of gaining knowledge, namely reasoning. The automation of reasoning has seen significant advances over the past decades and, thus, the expectation was that these advances would also have significant impact on the practice of doing mathematics. However, so far, this impact is small. We think that the reason for this is the fact that automated reasoning so far concentrated on the automated proof of individual theorems whereas, in the practice of mathematics, one proceeds by building up entire theories in a stepbystep process. This process of exploring mathematical theories consists of the invention of notions, the invention and proof of propositions (lemmas, theorems), the invention of problems, and the invention and verification of methods (algorithms) that solve problems (more) Tetsuo Ida, Japan http://www.score.is.tsukuba.jp/~ida/ Talk: Tiers of webOrigami Programming Abstract: The world wide web is an important knowledge repository for our daily activities, and moreover it is transforming itself to service repository. Many scientists not only publish their results on the web but offer services that accrue from their scientific discoveries and inventions. The webOrigami, under development by SCORE at University of Tsukuba, is one such science service portal that offers services to interested mathematicians and origamists. Its aim is to help them to explore the possibilities of computational origami as well as enjoying the origami art. In this talk I will present the current state of the development of the system, talking about technical problems that we encounters and solutions we came up with. The state of the art of the web programming technology is far from our satisfaction. It often leads us into many undesired pitfalls as well as security problems. The most serious problem, in our view, is the lack of an adequate computational model with which we reason about web programming and computing. Therefore, I will focus on the computation model for web computing that is based on multitiered programming methodology; the computation model with which we are trying to abstract from our programming efforts in constructing the portal. Joel Quinqueton, France Talk: Emergence in Problem Solving, Classification and Machine Learning Abstract: Emergence is usually the way in which a collective organisation behaves differently than the sum of its elements. We propose here an overview of different ways this paradigm is used in several fields of Artificial Intelligence and we propose some theoretical tracks. Stephen Watt, Canada Talk: Improving PenBased Mathematical Interfaces Abstract. Penbased user interfaces offer tantalizing potential for mathematical software systems. In contrast to normal text, entering and editing mathematical formulae with a digital pen can be much more natural than using a keyboard. Machine recognition of mathematical handwriting, however, is more complex than recognizing natural language text. In this context it is necessary to deal with a vast array of similar symbols and the analysis of the twodimensional syntactic structure of formulae. This talk outlines our work in this area. We describe our architecture for a mathematical handwriting component that can be embedded in various applications. These include computer algebra systems, such as Maple, and document processing applications, such as Microsoft Word. We describe the problem of mathematical character recognition and detail how recognition rates can be enhanced using data derived from the analysis of digital libraries. Limsoon Wong, Singapore http://www.comp.nus.edu.sg/~wongls/ Abstract: Whenever a programmer writes a loop, or a mathematician does a proof by induction, an invariant is involved. The discovery and understanding of invariants often underlies problem solving in many domains. I will discuss here my search for powerful invariants over the past decade. My search was/is motivated by a broad spectrum of problems: understanding query languages, engineering data integration systems, optimising disease treatments, recognizing DNA feature sites, and discovering reliable patterns. Clare Dixon, UK http://www.csc.liv.ac.uk/~clare/ Talk: Temporal Logics of Knowledge and their Applications in Security Abstract: Temporal logics of knowledge are useful for reasoning about situations where the knowledge of an agent or component is important, and where change in this knowledge may occur over time. Here we investigate the application of temporal logics of knowledge to the specification and verification of security protocols. We show how typical assumptions relating to authentication protocols can be specified. We consider verification methods for these logics, in particular, focusing on proof using clausal resolution. Finally we present experiences from using a resolution based theorem prover applied to security protocols specified in temporal logics of knowledge. Fabio Martinelli, Italy http://www.iit.cnr.it/staff/fabio.martinelli/ Talk: A uniform framework for the modeling and analysis of security and trust
Abstract. We aim at defining an integrated framework for the specification and (automated) analysis for security and trust in complex and dynamic scenarios. In particular, we show how the same machinery used for the formal verification of security protocols may be used to analyze access control policies based on trust management. In particular, we consider two wellknown languages: 1) the Rolebased Trustmanagement framework ($RT$) and 2) the transitive trust model, for defining trust and recommendation relationships. First, we show an encoding of the transitive trust model into part of $RT$; then, this subset is mapped into the inference construct of the CryptoCCS process algebra. The relationships among these languages could allow us to model and analyze trust and recommendation relationships of distributed systems by means of standard formal techniques, based on inference systems. Also some extensions that considers levels of trust in the credentials are suggested.
