Search

Mathematical texts can be computerised in many ways that capture differing amounts of the mathematical meaning. At one end, there is document imaging, which captures the arrangement of black marks on paper, while at the other end there are proof assistants (e.g., Mizar, Isabelle, Coq, etc.), which capture the full mathematical meaning and have proofs expressed in a formal foundation of mathematics. In between, there are computer typesetting systems (e.g., LTEX and Presentation MathML) and semantically oriented systems (e.g., Content MathML, OpenMath, OMDoc, etc.). In this paper we advocate a style of computerisation of mathematical texts which is flexible enough to connect the different approaches to computerisation, which allows various degrees of formalisation, and which is compatible with different logical frameworks (e.g., set theory, category theory, type theory, etc.) and proof systems. The basic idea is to allow a man-machine collaboration which weaves human input with machine computation at every step in the way. We propose that the huge step from informal mathematics to fully formalised mathematics be divided into smaller steps, each of which is a fully developed method in which human input is minimal. Let us consider the following two questions

In this article a method is proposed for ball tracking using 100 Hz computer vision in a semi-automated foosball table. In this application the behavior of the ball is highly dynamic with speeds up to 10 m/s and frequent bounces occur against the sides of the table and the puppets. Moreover, in the overhead camera view of the field the ball is often fully or partially occluded and there are other objects present that resemble the ball. The table is semi-automated to enable single user game play. This article shows that it is possible to perform fast and robust ball tracking by combining efficient image processing algorithms with a priori knowledge of the stationary environment and position information of the automated rods.

Model checking of temporal logic has already been proposed for automatic planning. In this paper, we introduce a simple adaptation of the ATL model checking algorithm that returns a strategy to achieve given goal. We point out that the algorithm generalizes minimaxing, and that ATL models generalize traditional game trees. The paper ends with suggestions about other game theory concepts that can be transfered to ATL-based planning. Keywords: Multi-agent systems, multi-agent planning, model checking.

NO ABSTRACT

The talk is based on a book about the human-oriented presentation of a mathematical proof in natural language, in a style as we may find it in a typical mathematical text book. How can a proof be other than human-oriented? What we have in mind is a deduction systems, which is implemented on a computer, that proves ��� with some human interaction ��� a mathematical textbook as may be used in an undergraduate course. The proofs generated by these systems today are far from being human-oriented and can in general only be read by an expert in the respective field: proofs between several hundred (for a common mathematical theorem), for more than a thousand steps (for an unusually difficult theorem) and more than ten thousand deduction steps (in a program verification task) are not uncommon. Although these proofs are provably correct, they are typically marred by many problems: to start with, that are usually written in a highly specialised logic such as the resolution calculus, in a matrix format, or even worse, they may be generated by a model checker. Moreover they record every logical step that may be necessary for the minute detail of some term transformation (such as, for example, the rearrangement of brackets) along side those arguments, a mathematician would call important steps or heureka-steps that capture the main idea of the proof. Only these would he be willing to communicate to his fellow mathematicians ��� provided they have a similar academic background and work in the same mathematical discipline. If not, i.e. if the proof was written say for an undergraduate textbook, the option of an important step may be viewed differently depending on the intended reader. Now, even if we were able to isolate the ten important steps ��� out of those hundreds of machine generated proof steps ��� there would still be the startling problem that they are usually written in the "wrong" order. A human reader might say: "they do not have a logical structure"; which is to say that of course they follow a logical pattern (as they are correctly generated by a machine), but, given the convention of the respective field and the way the trained mathematician in this field is used to communicate, they are somewhat strange and ill structured. And finally, there is the problem that proofs are purely formal and recorded in a predicate logic that is very far from the usual presentation that relies on a mixture of natural language arguments interspersed with some formalism. The book (about 800 page) which gives an answer to some of these problems is to appear with Elsevier

Data visualisation can be a great support to the data mining process. We introduce a data structure that allows browsing through the data giving a complete but very manageable overview over the entire data set, where the data is split into subsets and displayed from interesting angles to reveal the relevant patterns for each subset. Based on the features originating from principal separation analysis, a tree is grown. A node of the tree is associated with a feature and a subset of instances, and later on with a two-dimensional visualisation. At the node level, groups of instances of different classes that can be displayed from a more interesting angle are temporarily grouped together in subsets. For each of these subsets child nodes are created that display this part of the data from a more interesting angle, revealing new patterns. This process is continued until no further improved visualisation can be found. After the tree has been constructed, it can be used to easily browse through the data. The nodes correspond with two-dimensional visualisations of the data, but the specific properties of the tree allow for three-dimensional animated transitions from one node to another, further clarifying the patterns in the data.

Relationships are fundamental to all but the most impersonal forms of interaction in business. Human agents who are unsure of themselves seek honourable trading relationships. The establishment and growth of interpersonal relationships is a result of reciprocal exchange of information. This paper addresses the problem of use of information for developing and utilising relationships between negotiating agents. The presence of measurable information on the Internet underpins the philosophy of transparency in electronic business, which has an impact on the behaviour of involved agents. It takes âtwo to tangoâ for conducting business in such a ânet landscapeâ where communities and cliques emerge, shape and evolve. The paper presents a formalism for electronic negotiation technology that treats relationships as a commodity. It supports relationship building, maintaining, evolving, and passing to other agents, and utilises such relationships in agent interaction. The Honourable Negotiator also takes in account information about the relationships in networks of respective agents outside the trading space.

It is a big challenge to guarantee the quality of association rules in some application areas (e.g., in Web information gathering) since duplications and ambiguities of data values (e.g., terms). This paper presents a novel concept of rough association rules to improve the quality of discovered knowledge in these application areas. The premise of a rough association rule consists of a set of terms (items) and a weight distribution of terms (items). The distinct advantage of rough association rules is that they contain more specific information than normal association rules. It is also feasible to update rough association rules dynamically to produce effective results. The experimental results also verify that the proposed approach is promising.

This paper presents a formal model of the knowledge representation scheme KRFP based on the Fuzzy Petri Net (FPN) theory. The model is represented as an 11-tuple consisting of the components of the FPN and two functions that give semantic interpretations to the scheme. For the scheme a fuzzy recognition-inference procedure, based on the dynamical properties of the FPN and the inverse – KRFP scheme, is described in detail. An illustrative example of the fuzzy recognition algorithm for the knowledge base, designed by the KRFP, is given.

In this paper we show how the concepts of answer set programming and fuzzy logic can be succesfully combined into the single framework of fuzzy answer set programming (FASP). The framework offers the best of both worlds: from the answer set semantics, it inherits the truly declarative non-monotonic reasoning capabilities while, on the other hand, the notions from fuzzy logic in the framework allow it to step away from the sharp principles used in classical logic, e.g., that something is either completely true or completely false. As fuzzy logic gives the user great flexibility regarding the choice for the interpretation of the notions of negation, conjunction, disjunction and implication, the FASP framework is highly configurable and can, e.g., be tailored to any specific area of application. Finally, the presented framework turns out to be a proper extension of classical answer set programming, as we show, in contrast to other proposals in the literature, that there are only minor restrictions one has to demand on the fuzzy operations used, in order to be able to retrieve the classical semantics using FASP.