Workshop Program
« go back

All talks will be taking place in Lecture Theatre B. Enter the Computing Laboratory via the e-Research Centre entrance on Keble road, and you will be directed where to go.

Quantomatic Mini-workshop (Monday, April 4th)

• Talks, 10:00 -- 13:00 (not necessarily in order)
  • Ross Duncan - graphical languages, the red-green calculus, and MBQC
  • Aleks Kissinger - from monoidal theories to graph rewrite systems
  • Lucas Dixon - !-boxes, matching and rewriting in quantomatic
  • Matvey Soloviev - symmetry elimination in graph matching
  • Alex Merry - design architecture, generalising to arbitrary theories
• Discussion, 14:00 -- ...
• Welcome dinner and drinks for CIAO/Automatheo, 19:30
  • ... at The Royal Oak - 42-44 Woodstock Rd, Oxford OX2 6HT

CIAO/Automatheo, Day 1 (Tuesday, April 5th)

• Breakfast in the Atrium (provided), 9:30 -- 10:30
• Morning session, 10:30 -- 11:30
  • Roy McCasland - Automated Theorem Discovery: Are We There Yet?

    This talk will provide an overview of the current state of Automated Theorem Discovery systems, with particular attention paid to recent developments in the MATHsAiD system (no surprise, there). In addition, I hope to suggest several promising directions of future research in the general area of automated mathematical theory exploration.

  • Gudmund Grov - Some ideas on a proof technique language

    Writing and reading reasoning techniques is very difficult. In particular, the treatment of goals and assumptions, and how to pass them between techniques has turned out to be difficult. In this talk, we will motivate and outline a proof technique language based upon boxes and wires, which we are currently working on in Isaplanner. We will then discuss possible future extensions to this new representation.

• Mid-day session, 12:00 -- 13:00
  • Moa Johansson - Improving the efficiency of IsaCoSy

    IsaCoSy is a theory formation system for inductive theories. I will talk about some recent improvements in the process of being implemented. I will also contrast IsaCoSy to the QuickSpec system and discuss some ideas that we might borrow from it.

  • Wolfgang Windsteiger - Using Theorema in the Formalization of Theoretical Economics

    Theoretical economics makes use of strict mathematical methods. For instance, games as introduced by von Neumann and Morgenstern allow for formal mathematical proofs for certain axiomatized economical situations. Such proofs can -- at least in principle -- also be carried through in formal systems such as Theorema. In this paper we describe experiments carried through using the Theorema system to prove theorems about a particular form of games called pillage games. A pillage game is characterized by a power function which must satisfy some monotonicity axioms. The question then arises whether certain solution sets (in particular two sets, called core and stable set) exist and what they look like.
    
    Concretely we use Theorema to show properties previously proved on paper by two of the co-authors for pillage games with three agents. Of particular interest is a pseudo algorithm which summarizes the results previously shown. Since the computation involves infinite sets the pseudo algorithm is in several ways non-computational. However, in presence of appropriate lemmas, the pseudo algorithm contains sufficient computational content that Theorema can compute stable sets (which are always finite). We have concretely demonstrated this for three different important power functions.

• Lunch break, 13:00 -- 14:30
• Afternoon session, 14:30 -- 15:30
  • Iain Whiteside - Transforming Proof

    I will talk about my PhD project, developing refactoring techniques for proof scripts. In particular, I will motivate and define proof refactoring, then describe a simple declarative-style proof language, similar to Isar, and some proof preserving transformations.

  • Yuhui Lin - Proof Critics: The productive use of failures in formal methods

    The talk presents an outline for the proposal of my PhD project "proof critics: a productive use of failures in formal methods". Proof obligations (POs) arise when applying formal methods (FMs). The undischarged POs can become a bottleneck in the use of FMs in industry. The work we proposed here, as a part of AI4FM project, aims at increasing the proportion of discharged POs by analysing failed proofs and related patches to classify POs as families and construct proof strategies, which can be used to guide proof search for the POs in the same families.

• Snacks in the atrium, 16:00 -- 16:30
• Departmental seminar, 16:30 -- 17:30
  • Alan Bundy -- The Theory behind TheoryMine

    We describe the technology behind the TheoryMine novelty gift company, which sells the rights to name novel mathematical theorems. A tower of four computer systems is used to generate recursive theories, then to speculate conjectures in those theories and then to prove these conjectures. All stages of the process are entirely automatic. The process guarantees large numbers of sound, novel theorems of some intrinsic merit.

• Conference Dinner, TBC

CIAO/Automatheo, Day 2 (Wednesday, April 6th)

• Breakfast in the Atrium (provided), 9:30 -- 10:30
• Morning session, 10:30 -- 11:30
  • Aleks Kissinger - Graph Rewriting with Boxes and Wires

    Box-and-wire diagrams, introduced by Penrose in the 1970s provide a clean and abstract way to describe tensor contraction in multilinear algebra. More generally, they provide an elegant notion for any kind of compound systems with a notion of "plugging inputs into outputs". Graph rewriting techniques could prove a powerful tool for reasoning about these systems. To this end, we describe how box-and-wire diagrams can be encoded as typed digraphs, and how existing graph rewriting techniques can be adapted to obtain the correct notions of rewriting and composition.

  • Serge Autexier - Change Impact Analysis by Semantic Difference Analysis and Graph Rewriting: Possible Next Steps

    Change impact analysis is the task to determine the impact of changes in documents. To provide tool support, we maintain the documents (syntax) and their semantics explicitly and in close relationship, in order to reason about the impact on the semantics of changes made to the syntax. The current approach consist of performing the difference analysis on the syntax and use graph rewriting rules to synchronize the semantics with the changed syntax and propagate the impact of changes. Although this works nicely, it leaves room for improvements, such as how to incorporate more semantics into the difference analysis, how to ensure termination of the graph rewriting process or how to prove properties about the impact analysis procedure itself. In this talk we want to explore what next steps could be, such as to lift the difference analysis from the syntax to the semantics level --- with the option of using Rippling ideas for graph rewriting.

• Mid-day session, 12:00 -- 13:00
  • Dominik Dietrich - Automation of formal *and* human-readable proofs

    It is well known that the level of detail of formal proofs is significantly higher than in human proofs, resulting in very large proofs. This is insignificant in situations where the proof can be generated fully automatically and no explanation is required; however, the ability to understand proofs becomes crucial within interactive proof development or proof tutoring. While human-readable proof languages have been developed as abstract input representation for formal proofs, there is hardly any proof automation for declarative proofs. Moreover, the complexity of the underlying proof objects make it impossible to translate back a proof object to such an abstract representation.
    
    In this talk, I present two key techniques to overcome this deficiency: First, the underlying calculus is lifted to the more abstract assertion level, a proof style in which each reasoning step corresponds to the application of an axiom, lemma, theorem, or hypothesis. As a consequence, proof objects become much shorter and can be translated back to a human-readable proof language, independently of how they were generated. Second, I present a tactic language whose input and output representation corresponds to underspecified human-readable proof scripts.

  • Christoph Lueth - Certification, formal verification and safety in robotics: an experience report

    This talk relates our experiences in applying formal verification in the robotics domain. We outline an algorithm for a safety-related opto-electronic protective device that was specifically designed with safety through formal verification in mind. Our verification methodology is presented, which has also been accepted for use in safety contexts up to SIL 3, and the necessary normative measures that are covered by its use are discussed. Throughout, issues we recognised as being important for a successful application of formal methods in the domain at hand are highlighted. These pertain to the development process, the abstraction level at which specifications should be formulated, and the interplay between simulation and verification, among others. We also discuss the wider applicability of our methodology.

• Invited talk: 14:30 -- 15:30
  • Aaron Sloman - Evolution, robots and mathematics

    Once there were no mathematics teachers. So where did mathematics, as an activity in which mathematical concepts are developed, mathematical conjectures formulated and mathematical proofs discovered, come from? An outline answer seems to be that biological evolution produced some organisms that, in addition to learning particular facts and empirically supported generalisations about their environment, had a further ability. They could reorganise what they had discovered into something like a deductive system that allowed conclusions to be drawn about situations that had never been experienced, including both conclusions about the gains from building new kinds of tools, weapons or shelters, and conclusions about serious dangers in other novel actions. A later evolutionary development of this sort in humans allowed children who had learnt ways of communicating verbally to reorganise what they had learnt into a *generative* system (based on syntactic rules), allowing them to produce or understand utterances they had never heard previously. That process occurs in children without teachers doing anything to make it happen, and I suggest that similar forms of reorganisation can extend knowledge originally acquired empirically about spatial structures and processes. This may also explain creative problem solving in some non-humans. What appears to be unique to humans is the ability to become aware of having this new knowledge and the consequent ability to communicate it to others, and then to discuss its limitations, and collaborate in improving and refining the knowledge. All this is highly speculative, though developmental psychology research by Jean Piaget and Annette Karmiloff-Smith (who labels the process of reorganisation "Representational Redescription") lends support to the conjectues. Examples that work with many adults will also be presented. However, work done so far in automated theorem proving or "intelligent" robotics has so far not produed mahcines capable of makng discoveries of the sorts I'll present. This is a major reason why no robots produced so far by AI researchers even get near the intelligence of a human toddler. I'll sketch a possible research programme to remedy this.

• Business meeting, 15:45 -- ...