We introduce Unified Decomposition-Aggregation (UDA) Rules . They are a family of axiom schemata that are instantiated at run-time to add new axioms to a logical theory. These new axioms are implications, whose preconditions will be constructed from an analysis of the goal to be proved and the theory in which it is to be proved. We illustrate their application to query answering using the FRANK system.

The demand for insights into how artificial intelligent systems work is rapidly growing.This has arisen as AI systems are being integrated into almost every aspect of our lives from finance to health, security and our social lives.Current techniques for generating explanations focus on explaining opaque algorithms such as neural network models.However, considering the fact that these models do not work in isolation, but are combined, either manually or automatically, with other inference operations, local explanations of individual components are simply not enough to give the user adequate insights into how an intelligent system works.It is not unusual for a system made up of fairly intuitive components to become opaque when it is combined with others to build an intelligent agent.In this paper we argue that there is the need to combine diverse forms of reasoning in order to generate explanations that span the entire chain of reasoning: not just explanations for the, so called, black-box models.Our hypothesis is that: A hybrid approach using statistical and deductive reasoning makes possible a richer form of explanation not available to purely statistical ML approaches.We explore the concepts of 'local' and 'global' explanations and show how to give users a wide range of insights, using what we term an 'explanation blanket'.We tackle this challenge using the FRANK query answering system and show that its hybrid approach facilitates this kind of reasoning with explanations.It is important to note that the evaluation of user preferences for explanation is outside the scope of this work.

Abstract The use of formal method techniques can contribute to the production of more reliable and dependable systems. However, a common bottleneck for industrial adoption of such techniques is the needs for interactive proofs. We use a popular formal method, called Event-B , as our working domain, and set invariant preservation (INV) proofs as targets, because INV proofs can account for a significant proportion of the proofs requiring human interactions. We apply an inductive theorem proving technique, called rippling, for Event-B INV proofs. Rippling automates proofs using meta-level guidance. The guidance is in particular useful to develop proof patches to recover failed proof attempts. We are interested in the case when a missing lemma is required. We combine a scheme-based theory-exploration system, called IsaScheme [ MRMDB10 ], with rippling to develop a proof patch via lemma discovery. We also develop two new proof patches to unfold operator definitions and to suggest case-splits, respectively. The combined use of rippling with these three proof patches as a proof method significantly improves the proof automation for our evaluation set.

The aim of the MATHsAiD project is to build a tool for automated theorem-discovery; to design and build a tool to automatically conjecture and prove theorems (lemmas, corollaries, etc.) from a set of user-supplied axioms and definitions. No other input is required. This tool would, for instance, allow a mathematician to try several versions of a particular definition, and in a relatively small amount of time, be able to see some of the consequences, in terms of the resulting theorems, of each version. Moreover, the automatically discovered theorems could perhaps help the users to discover and prove further theorems for themselves. The tool could also easily be used by educators (to generate exercise sets, for instance) and by students as well. In a similar fashion, it might also prove useful in enabling automated theorem provers to dispatch many of the more difficult proof obligations arising in software verification, by automatically generating lemmas which are needed by the prover, in order to finish these proofs.

Smart-cards are considered to be one of the most secure, tamper-resistant, and trusted devices for implementing confidential operations, such as authentication, key management, encryption and decryption for financial, communication, security and data management purposes. The commonly used RSA PKCS#11 standard defines the Application Programming Interface for cryptographic devices such as smart-cards. Though there has been work on formally verifying the correctness of the implementation of PKCS#11 in the API level, little attention has been paid to the low-level cryptographic protocols that implement it.

We describe ORS, an ontology repair system. In contrast to most ontology matching systems, ORS is designed to repair an ontology that does not accurately model its domain. ORS’s ontology repairs include belief revisions, but more often makes signature repairs. It does not require full access to the ontologies of other agents and works entirely automatically and dynamically. ORS is the first example of a new breed of dynamic, automatic ontology-repair mechanisms, which we believe will be essential to realise the vision of autonomous, interacting agents, such as envisaged in the emantic Web. Full access to another (potentially rival) agent’s ontology is unrealistic; static and interactive matching mechanisms are unrealistic in the context of huge, dynamic populations of agents and full ontological agreement is pragmatically unrealistic. We present encouraging experimental results, plus an analysis of current limitations to be addressed in future work.

The Annual Boole Lecture was established and is sponsored by the Boole Centre for Research in Informatics, the Cork Constraint Computation Centre, the Department of Computer Science, and the School of Mathematics, Applied Mathematics and Statistics, at University College Cork. The series in named in honour of George Boole, the first professor of Mathematics at UCC, whose seminal work on logic in the mid-1800s is central to modern digital computing. To mark this great contribution, leaders in the field of computing and mathematics are invited to talk to the general public on directions in science, on past achievements and on visions for the future.

In this paper we show that the automated reasoning technique of deductive synthesis can be applied to address the problem of machine-assisted composition of e-Science workflows according to users' specifications. We encode formal specifications of e-Science data, services and workflows, constructed from their descriptions, in the generic theorem prover Isabelle. Workflows meeting this specification are then synthesised as a side-effect of proving that these specifications can be met.

Design patterns are widely used by designers and developers for building complex systems in object-oriented programming languages such as Java. However, systems evolve over time, increasing the chance that the pattern in its original form will be broken.To verify that a design pattern has not been broken requires specifying the original intent of the design pattern. Whilst informal descriptions of design patterns exist, no formal specifications are available due to differences in implementations between programming languages.We present a pattern specification language, Spine, that allows patterns to be defined in terms of constraints on their implementation in Java. We also present some examples of patterns defined in Spine and show how they are processed using a proof engine called Hedgehog.The conclusion discusses the type of patterns that are amenable to defining in Spine, and highlights some repeated mini-patterns discovered in the formalisation of these design patterns.

Abstract. C Y NTHIA is a transformation-based editor for a functional subset of ML that lies somewhere between a structure editor and a framework for formal program development. Users construct programs from existing code by applying editing commands that make a semantic analysis of the program's behaviour, e.g., whether it is terminating. All analysis is done using the Oyster system, which is an implementation of proofs-as-programs. We concentrate on identifying analyses that can be done fully automatically (e.g., using a decision procedure) and hence can be hidden from the user. As a result, C Y NTHIA represents progress towards a goal of program editors that make an intelligent analysis of their code, but in a way that requires no extra input from the programmer.

Design patterns are widely used by object oriented designers and developers for building complex systems in object oriented programming languages such as Java. However, systems evolve over time, increasing the chance that the pattern in its original form will be broken. We attempt to show that many design patterns (implemented in Java) can be verified automatically. Patterns are defined in terms of variants, mini-patterns, and artifacts in a pattern description language called SPINE. These specifications are then processed by Hedgehog, an automated proof tool that attempts to prove that Java source code meets these specifications.

LIA

C/sup Y/NTHIA is a novel editor for the functional programming language ML in which each function definition is represented as the proof of a simple specification. Users of C/sup Y/NTHIA edit programs by applying sequences of high-level editing commands to existing programs. These commands make changes to the proof representation from which a new program is then extracted. The use of proofs is a sound framework for analysing ML programs and giving useful feedback about errors. Amongst the properties analysed within C/sup Y/NTHIA at present is termination. C/sup Y/NTHIA has been successfully used in the teaching of ML in two courses at Napier University, Scotland. C/sup Y/NTHIA is a convincing, real-world application of the proofs-as-programs idea.

Proof by mathematical induction plays a crucial role in reasoning about functional programs. A generalization step often holds the key to discovering an inductive proof. We present a generalization technique which is particularly applicable when reasoning about functional programs involving accumulating parameters. We provide empirical evidence for the success of our technique and show how it is contributing to the ongoing development of a parallelizing compiler for Standard ML.

Most efforts to automate the formal verification of communicating systems have centred around finite-state systems (FSSs). However, FSSs are incapable of modelling many practical communicating systems, and hence there is interest in a novel class of problems, which we call VIPSs (Value-passing Infinite-state Parameterised Systems). Existing approaches using model checking over FSSs are insufficient for VIPSs, due to their inability both to reason with and about domain-specific theories, and to cope with systems having an unbounded or arbitrary state space. We use the Calculus of Communicating Systems (CCS) with parameterised constants to express and specify VIPSs. We use the laws of CCS to conduct the verification task. This approach allows us to study communicating systems, regardless of their state space, and the data such systems communicate. Automating theorem proving in this system is an extremely difficult task. We provide automated methods for CCS analysis; they are applicable to both FSSs and VIPSs. Adding these methods to the Clam proof-planner, we have implemented an automated theorem prover that is capable of dealing with problems outside the scope of current methods. This paper describes these methods, gives an account as to why they work and provides a short summary of experimental results.

1Department of Artificial Intelligence, University of Edinburgh, Edinburgh, UK, 2Department of Private Law, University of Edinburgh, Edinburgh, UK

I am broadly in sympathy with Cheeseman’s attempt to promote the use of Bayesian probability in artificial intelligence; it may well have a role to play in inference, especially in the representation of uncertainty and jumping to conclusions. However, Cheeseman’s argument is deficient in a number of key areas, and so fails to carry the force that he would like

An interval anthmetm package, INT, which generalizes previous interval packages by using information about the monotonicity of functions is described.INT has been used in an algebraic manipulation package, PRESS, to check the conditions of rewrite rules and the solutions to equations.