CISA Seminars

Abstract:
Logical formulas involving special functions such as ln, exp and sin can be proved automatically by MetiTarski: a resolution theorem prover modified to call a decision procedure for the theory of real closed fields. (This theory in particular includes the real numbers with addition, subtraction and multiplication.) Special functions are approximated by upper and lower bounds, which are typically ratios of polynomials. The decision procedure simplifies clauses by deleting literals that are inconsistent with other algebraic facts; the net effect is to split the problem into numerous cases, each covered by a different approximation, and to prove them individually. MetiTarski simplifies arithmetic expressions by conversion to a recursive representation, followed by flattening of nested quotients. It can solve many difficult problems found in mathematics reference works, and it can also solve problems that arise from hybrid and control systems.

Abstract:

Abstract:
In a game from game theory, a Nash equilibrium (NE) is a combination of one strategy per agent such that no agent can increase his payoff by unilaterally changing his strategy. Kuhn proved that all (tree-like) sequential games have NE. Osborne and Rubinstein abstracted over these games and Kuhn's result: they proved a *sufficient* condition on agent *preferences* for all games to have NE. I will present a *necessary and sufficient* condition, thus accounting for the game-theoretic frameworks that were left aside. The proof is *formalised* using Coq, and contrary to usual game theory it adopts an inductive approach to trees for definitions and proofs. By rephrasing a few game-theoretic concepts, by ignoring useless ones, and by characterising the proof-theoretic strength of Kuhn's/Osborne and Rubinstein's development, the talk also intends to clarifies sequential game theory. Then I will sketch an alternative proof. Both proofs so far pre-process the preferences by topological sorting, which is surprising since it decreases the number of NE. Finally I will sketch two other proofs that pre-process the preferences only by transitive closure. The four proofs are all constructive and by induction, and I will compare them when seen as algorithms. The four proofs also constitute diverse viewpoints on the same concepts, the trial of diverse techniques against the same problem, and reusable techniques for similar structures.

Abstract:

Bunched logics, originating in O'Hearn and Pym's BI, are a relatively recent addition to the menagerie of substructural logics. They can be seen as the result of freely combining a standard (additive) propositional logic with a (multiplicative) linear logic. Bunched logics enjoy a Tarskian "resource" interpretation of formulas, which has very successfully been exploited to obtain logics for program analysis - most notably in the shape of separation logic, which is based upon an interpretation of resources as portions of heap memory.

In this talk, we examine bunched logic from a general proof-theoretic perspective. While there has been considerable interest in the semantics of bunched logics, their proof theory by contrast has received comparatively little attention; only BI possesses a well-behaved sequent calculus, which does not naturally extend to the other bunched logics such as BBI. We show how to obtain *display calculi* 'a la Belnap for all four principal bunched logics in a unified manner (each such logic being characterised by the strengths of its additive and multiplicative components). Each of our calculi satisfies cut-elimination and is sound and complete with respect to a Hilbert-style presentation of the corresponding bunched logic. By examining the relationship between our calculi and the BI sequent calculus, we also provide an explanation as to why well-behaved sequent calculi for the other bunched logics have been so elusive.

This talk is based upon a related paper by the speaker [1].

[1] James Brotherston. A unified display proof theory for bunched logic. Submitted, 2009. Available from http://www.doc.ic.ac.uk/~jbrother/

Abstract:
There is a remarkable diversity of cognitive abilities shown by natural agents that pose considerable challenges for computational models. For example, the apparent variety of different forms of reasoning and learning are hard to address with uniform computational frameworks, but also simple perceptual categorization tasks of humans require sophisticated algorithmic approaches for modeling. In this talk, I will present certain cognitively inspired approaches for addressing some of these problems. The main part of the talk will be about analogical reasoning as a tool for integrating non-classical forms of reasoning and learning. In particular, I will focus on the syntactic and semantic aspects of establishing an analogical relation between a source and target domain. Furthermore, I will sketch some ideas of other cognitively inspired approaches like learning semantic knowledge from pure structural information, automatically adapting ontological knowledge in text technological applications, and learning logic with neural networks.