photo photo photo photo photo

The next Scottish Theorem Proving meeting in Dundee, 17 June 2011

STP has a long history of similar events, see more about STP and Previous events.

This time, we hold STP jointly with invited lecture by Jeremy Frank, hosted by Karen Petrie and the Theory of Computing and AI group at the School of Computing, Dundee.

The event is sponsored by the Scottish Informatics and Computer Science Aliance SICSA.

Where:

The School of Computing is a modern building in the center of Dundee, within 15 minutes walk from Dundee train station. Approximate route is here.

When:

17 June 2011, 12 pm - 17 pm.

What:

12.00 - 13.00 Invited lecture by Jeremy Frank, the head of AI at NASA.

Constraint and Flight Rule Management for Space Mission Operations: Past, Present and Prologue.

13.00 - 14.00 Lunch. Buffet lunch served in the main hall on the ground floor of the Queen Mother Building (the place is also locally known as "The Street").

14.00 - 17.00 STP talks:

14.00 - 14.40. Christoph Herrmann, University of St Andrews.

Title: Programming of Autonomous Vehicles with Static Guarantees. Lecture slides are available here.

14.40 - 14.50. Discussion and break.

14.50 - 15.30. Omar Rivas, University of Edinburgh.

Title: Scheme-based synthesis of inductive theories.

15.30 - 15.40. Discussion.

15.40 - 16.10. Coffee break. The Street.

16.10 - 16.50. Katya Komendantskaya, University of Dundee.

Title: Statistical Machine Learning for discovery of proof tactics in automated theorem provers.

Lecture slides are available here.

16.50 - 17.00. Discussion.

Social event:

17.00 - 19.30. Dinner.

There will be dinner after the event in the Riverside Inn (a lift provided).

If you intend to attend, please contact komendantskaya@gmail.com

**************************************************

Abstracts of the talks:

Invited lecture by Jeremy Frank, the head of AI at NASA.

Title: Constraint and Flight Rule Management for Space Mission Operations: Past, Present and Prologue.

Abstract: NASA's Mission Operations Directorate (MOD) formalizes thousands of operational constraints to help govern human spaceflight missions. MOD collects, develops, documents and applies these constraints to ensure the safety of the crew, as well as proper operation of the spacecraft systems and payloads.Today, these constraints are stored in human-readable documents, and are used to configure tools used by the flight controllers who plan and fly missions.We have begun developing a novel capability for authoring and maintaining such constraints called the Constraint and Flight Rule Management system (ConFRM).ConFRM provides history tracking and commenting features that allow users to trace the heritage of constraints throughout their lifecycle.ConFRM maintains links between related constraints, and between constraints and source information used to create the constraints.ConFRM uses these links to ensure consistency between constraints throughout their lifecycle, and provides authors and reviewers the ability to navigate between constraints and related data.Finally, ConFRM enables export of constraints into many different forms, including human readable documents and tool configuration formats, thereby eliminating manual labor and reducing transcription errors. In this talk, I will first describe NASA human spaceflight mission operations, operations concepts, and operations tools and products. I will then describe the ConFRM project, architecture and current status. At the end of the talk I will describe future ConFRM capabilities, and discuss the potential of ConFRM for use on deep space missions and as a generic capability for documentation of operational constraints.

Bio: Jeremy Frank received his Ph. D. in Computer Science from the University of California, Davis, and his B.A. in Mathematics from Pomona College. Dr. Frank has worked at NASA Ames Research Center since 1997. He is the lead of the Planning and Scheduling Group, which performs research, advanced prototype and tools development for spaceflight mission operations. Dr. Frank currently leads the Solar Array Constraints Engine (SACE) project to build a solar array planner for International Space Station operations, and is a member of the Autonomous Systems and Avionics (ASA) project, developing advanced concepts for human spaceflight missions to distant destinations such as Near Earth Asteroids or Mars. Dr. Frank is the recipient of a NASA Silver Snoopy award, the Astronaut's personal award for outstanding achievements related to human spaceflight safety or mission success. His academic interests include Artificial Intelligence, particularly planning, scheduling and combinatorial optimization and search. His recreational interests include ceramics, photography, cooking, story readings, gaming, mathematics, and history.

Christoph Herrmann, University of St Andrews.

Title:

Verification of actions of autonomous vehicles using AGDA.

Abstract: We present a domain-specific language (DSL) embedded in Agda for describing actions of autonomous vehicles (AVs) together with certificates in the type for properties of such programs, e.g., that such a vehicle can move from an arbitrary start location (sx,sy) to an arbitrary final location (fx,fy) within a guaranteed upper bound on the time ( | fx-sx | + | fy-sy | + 4 units ), provided no exceptional circumstances will occur. This is based on an operational semantics for the AV in terms of DSL constructs. Challenges are parameterised, non-linear and even non-polynomial constraints in multiple variables, verification of non-finite state systems and proofs of properties without a dedicated witness but a selection of potential witnesses. We use Agda's inductive reasoning capabilities to deal with parameterised formulae that are accessible to inductive proofs. The ring solver module of Agda's standard library simplifies equivalence proofs for arithmetic expressions. Exhaustive, dependently-typed pattern matching can select an appropriate witness from a set of choices; this is carried over from the so-called "trick" in partial evaluation, where a finite case distinction can move static values from a dynamic context into a static context, increasing the amount of available static information. Furthermore, we use embedded DSLs at the level of atomic AV operations as well as at the level of complex AV tasks to increase the level of abstraction from the operational AV semantics. We provide a translation from the complex to the simple language together with an equivalence proof. We will also discuss work in progress of how certificates can be attached to DSL programs that have been generated automatically, e.g., based on an optimisation or search strategy.

Omar Rivas, University of Edinburgh.

Title:

Scheme-based synthesis of inductive theories.

Abstract: We describe a technique to produce conjectures and recursive functions from the signature of inductive theories. The approach uses higher-order formulae as its primary source for invention. We show how the new definitions and the lemmata discovered during the exploration of the theory can be used not only to help with the proof obligations during the exploration, but also to reduce redundancies inherent in most theory formation systems. We implemented our ideas in an automated tool, called IsaScheme, which employs Knuth-Bendix completion and recent automatic inductive proof tools. We have evaluated our system in a theory of natural numbers and a theory of lists.

Katya Komendantskaya, University of Dundee.

Title: Statistical Machine Learning for discovery of proof tactics in automated theorem provers.

Abstract: In this talk, I will explain the motivation behind applying machine learning methods in proof theory. I will show - on some simple examples - the range of problems that arise for this task, and outline some solutions to those. I will pay special attention to coalgebraic methods in proof theory and their applications in machine learning.