Room F161, Department of Computing Science, University of Glasgow
17 Lilybank Gardens, Glasgow
This meeting of the Scottish Theorem Proving seminar has been organised by Simon Gay and Alice Miller. Please contact Simon Gay for further details or clarification. In any case, please let Simon Gay know if you are planning to attend, so that we have some idea of numbers.
Travel information, maps etc. can be found here.
More information about Scottish Theorem Proving can be found here.
Abstract
I will present a personal view of the current status of theorem proving (mechanised reasoning) research, highlighting some of the hot topics, and suggesting some challenges for future research. The talk will not be an exhaustive overview of the field, nor a very objective one, but I hope it may stimulate some discussion and provide some inspiration to both newcomers and experienced TP researchers.
Abstract
STE has been very successful in large scale data path verification of hardware circuits. However its link with Theorem Proving have been less explored. The foundation of any possible link rests on the semantic connection between the logic of properties in the STE and the logic of theorem prover. In this talk I'll give some thoughts on what is available and some future directions towards a strong connection between the Theorem Proving and the STE World.
Abstract
Different ways in which symmetry and induction can be used to aid model-checking will be discussed, and examples given. One situation in which symmetry reductions could certainly help is in case-reduction. I will illustrate this scenario via a feature interaction example and ask the question: Can theorem proving help here?
Abstract
This talk presents an investigation into the structure of proof in non-standard analysis using proof-planning. The theory of non-standard analysis was developed by Robinson in the 1960s. It offers a more algebraic way of looking at proof in analysis. Proof-planning is a technique for reasoning about proof at the meta-level. We use proof-planning to encapsulate the patterns of reasoning that occur in non-standard analysis proofs.
We first introduce in detail the mathematical theory and the proof-planning architecture. We then present our research methodology, and describe the formal framework, which includes an axiomatisation. We then present our development of proof-plans for theorems involving limits, continuity and differentiation. Finally, we explain how proof-planning applies to theorems which combine induction and non-standard analysis.