ALGAE SEMINARS
The ALGAE (Applied Logic Group and Anyone Else) seminar series is run by the Applied Logic Group. All seminars are open to anyone interested unless stated otherwise. Any ALG member may organise an ALGAE seminar and use this page to advertise it. (To add a seminar announcement, click the little "[e]" at the bottom right hand side of this page, then use the ALG username and password to enter "edit" mode when prompted.)
List Of Seminars (Most Recent First)
** UCL Department of Computer Science Distinguished Lecture **
TITLE: An Approach to Cognitive Control for Robots
SPEAKER: Keith Clark, Imperial College London
DATE, TIME AND PLACE: Monday 16 June 2008, 2:30pm, Room 1.03, Malet Place Engineering Building, UCL Department of Computer Science [directions and map]
PRESENTATION IN PDF FORMAT
ABSTRACT:
At the lowest level the control program for a robot must react quickly to sensor readings but be goal directed and robust. At the next level the control program should be able to switch between lower level programs making use of higher level beliefs about the state of is environment inferred from sensor readings. At the highest level, its control architecture should be able to 'think' about goals, react to events, and select appropriate lower level control programs to achieve a particlar goal, or to react to an event.
In this talk we will argue that a control architecture that combines a deliberative software agent architecture with a powerful rule language for programming robot behaviours allows for the smooth integration of the three levels of control.
We start by introducing the robot programming language: Nilsson's Teleo-Reactive (TR) rule procedures. We will demonstrate its use with a simulation and visualisation of purely reactive non-terminating can collecting robot. We shall see that the operational semantics of TR procedures leads naturally to a multi-threaded implementation.
We will then show how TR procedures, augmented with the ability to infer higher level beliefs about the state of the environment from sensor readings, can be used to program a block stacking robot arm that 'knows' what a tower of blocks is, and which can be given different tasks: to build a tower of named blocks, to move a named block to a specific location, or to dismantle towers. Again this will be demonstrated with a simulation and visualisation.
A key feature of TR procedure control is that the robot can helped or hindered in its task and the TR procedure will immediately respond by skipping actions, if helped, or by redoing actions if hindered. This will be demonstrated using the robot arm simulation.
The highest level of control is an event watching thread that invokes appropriate TR procedures, from a library of such procedures, to respond to key events: new commands or significant belief updates resulting from sensor inputs. This control thread can suspend and later resume existing TR procedures threads, taking into account priorities of the events and meta-knowledge about incompatibility between TR procedures (need same resources etc). This control level makes use of ideas from BDI (Beliefs, Desires and Intentions) software agent architectures.
An example of such a switch of behaviour is a can collecting robot that responds to the event of a low-battery signal. It suspends its can collecting TR procedure, and invokes a procedure for finding the recharge plate and recharging the battery. When this is finished, the can collecting is resumed.
TITLE: Density Elimination
SPEAKER: George Metcalfe, Vanderbilt University
DATE, TIME AND PLACE: 2pm Tuesday 27th May in Room 1.13, New Engineering Building, UCL
ABSTRACT:
Elimination of the cut rule is a fundamental topic in Proof Theory, corresponding to the removal of lemmas from proofs. However, the addition and elimination of other rules also merit investigation. In this talk I will consider one such rule, important in the meta-mathematics of Fuzzy Logic: the so-called "density rule" of Takeuti and Titani. Adding this rule to axiomatizations for certain classes of substructural logics guarantees completeness with respect to dense linearly ordered algebras. Density elimination, performed on corresponding Gentzen systems, then establishes this completeness property for the original axiomatizations. The method provides an interesting example of a proof-theoretic proof of an algebraic result where no algebraic proof is known.
TITLE: First-Order Deduction in Neural Networks
SPEAKER: Ekaterina Komendantskaya, INRIA (l'Institute Nationale de Recherche en Informatique et en Automatique), Sophia Antipolis, France.
DATE, TIME AND PLACE: 2pm on March 5th in room 311, Huxley Building, 180 Queens Gate, Imperial College.
ABSTRACT:
Connectionism is a movement in the fields of artificial intelligence, cognitive science, neuroscience, psychology and philosophy of mind which hopes to explain human intellectual abilities using artificial neural networks - a simplified mathematical model of a human brain. One of its areas, Neuro-Symbolic integration, investigates ways of integrating logic and formal languages with neural networks in order to better understand the essence of symbolic (deductive) and human (developing, spontaneous) reasoning, and to show interconnections between them.
There were many neuro-symbolic systems proposed over the last two decades. However, we know little about their practical use in automated reasoning and computational logic. The main obstacle for the implementations of neuro-symbolic networks in computational logic lies in the fact that the majority of existing neuro-symbolic neural networks process truth values of formulae, and do not work directly with their syntax. Many of these networks use semantic operator T_P, which requires infinite iterations in order to reach the least fixed point; and hence it requires complicated finite approximation in order to be processed in finite neural networks.
In this talk, I will introduce SLD neural networks, an alternative to the existing neuro-symbolic networks. SLD neural networks use a novel method of performing the algorithm of SLD-resolution in neural networks. The resulting neural networks work with syntax of formulae, and perform unification and resolution algorithms. They are finite and do not require any approximations. Notably, they embed six learning functions recognised in neurocomputing.
TITLE: A Temporal Logic of Robustness
SPEAKER: John C. McCabe-Dansted, University of Western Australia
DATE, TIME AND PLACE: Wed 5 Sep, 2pm, room 1.02, computer science building, UCL Department of Computer Science
ABSTRACT:
It can be desirable to specify polices that require a system to achieve some outcome even if a certain number of failures occur. This paper proposes a logic, RoCTL*, which extends CTL* with operators from Deontic logic, and a novel operator referred to as "Robustly". This novel operator acts as variety of path quantifier allowing us to consider paths which deviate from the desired behaviour of the system. Unlike most path quantifiers, the Robustly operator must be evaluated over a path rather than just a state; the Robustly operator quantifies over paths produced from the current path by altering a single step. The Robustly operator roughly represents the phrase "even if an additional failure occurs now or in the future". This paper examines the expressivity of this new logic, motivates its use and shows that it is decidable.
TITLE: Modular-E: A Logic for Assimilating Unexpected Observations Along a Time Line
SPEAKER: Rob Miller, UCL
DATE, TIME AND PLACE: Monday 18 June at 2pm in Room 1.03, UCL Department of Computer Science
ABSTRACT:
Modular-E (ME) is a specialized logic for reasoning about actions and events. It allows the user to express general knowledge about the effects of actions, and then use this knowledge to predict the outcome of a particular series of actions along a time line. The actions in question may be executed concurrently and may be nondeterministic. This talk describes how Modular-E can be extended to that it can also assimilate new knowledge that arrives in the form of observations along the time line, in particular when these observations apparently conflict with its original predictions. The problem of assimilating such observations is sometimes referred to in the AI literature as the "qualification problem". [presentation in pdf format]
TITLE: A Quantitative Trust Model for Negotiating Agents: An Argumentation and Reputation-based Approach
SPEAKER: Jamal Bentahar, Concordia University, Canada
DATE, TIME AND PLACE: Friday 8 June at 2pm in Studio B, Huxley Building, Department of Computing, Imperial College London, 180 Queen's Gate, London SW7 2BZ
ABSTRACT:
In this talk, a quantitative trust model for argumentation-based negotiating agents will be presented. The purpose of such a model is to provide a secure environment for agent negotiation within multi-agent systems. In this model, agents are equipped with reasoning capabilities allowing them to interact with each other using logic-based dialogue games. Also, they can reason about the reputation of each other using their argumentation systems. The reputation is dealt with as a quantitative value computed using a set of parameters based on the interaction histories and the notion of social networks. The formulation, algorithmic description, and computational complexity of this model will be addressed.
TITLE: Argumentation Framework for Decision Making
SPEAKER: Maxime Morge, Pisa University
DATE, TIME AND PLACE: Friday 30 March at 12 noon in Room 343 Huxley Building, Department of Computing, Imperial College London, 180 Queen's Gate, London SW7 2BZ
ABSTRACT:
Since a decision can be resolved by confronting and evaluating the justifications of different positions, argumentation can support such a process. This is the reason why many works in the area of Artificial Intelligence focus on computational models of argumentation. In particular, nonmonotonic logic techniques have been used as a model with hierarchies of possibly conflicting rules. However, even if modern techniques are used, this logical approach is still limited to the epistemic reasoning. The point is that a decision is not limited to draw conclusions. For this purpose, we propose an argumentation framework for practical reasoning. A logic language is used as a concrete data structure for holding the statements like knowledge, goals, actions. Different priorities are attached to these items corresponding to the user's preferences, the likelihood of the knowledge and the credibility of alternatives. These concrete data structures consist of information providing the backbone of arguments. Due to the abductive nature of decision making, arguments are built by reasoning backwards. Moreover, arguments are defined as tree-like structures. In this way, our framework suggests some solutions and provides an intelligible explanation of this choice.
This work is supported by the Sixth Framework IST programme of the EC, under the 035200 ARGUGRID project.
+44 (0)20 7679 2000 - Copyright © 1999-2007 UCL