For centuries, the highest level of mathematics has been seen as an isolated creative activity, to produce a proof for review and acceptance by research peers. Mathematics is now at a remarkable inflexion point, with new technology radically extending the power and limits of individuals. ‘Crowdsourcing’ pulls together diverse experts to solve problems; symbolic computation tackles huge routine calculations; and computers, using programs designed to verify hardware, check proofs that are just too long and complicated for any human to comprehend. ‘Social machines’ are new paradigm, identified by Berners-Lee, for viewing a combination of people and computers as a single problem-solving entity. This paper outlines a research agenda for a new vision of a mathematics social machine, a combination of people, computers, and archives to create and apply mathematics, and places it in the context of verification research, computational logic and Roy Dyckhoff's pioneering work on computer proof.

Abstract We consider reasoning about linear systems expressed as block diagrams that give a graphical representation of a system of differential equations or recurrence equations. We use the notion of additive relation borrowed from homological algebra to give a convenient framework in which all diagrams have a semantic value. We give a sound system of Hoare-style rules for the block diagram constructors that singles out a tractable subset of the block diagram language in which all diagrams represent total functions. We show these rules in action on some simple examples from a variety of applications domains.

Abstract Real number theorem proving has many uses, particularly for verification of safety critical systems and systems for which design errors may be costly. We discuss a chain of developments building on real number theorem proving in PVS. This leads from the verification of aspects of an air traffic control system, through work on the integration of computer algebra and automated theorem proving to a new tool, NRV, first presented here that builds on the capabilities of Maple and PVS to provide a verified and automatic analysis of Nichols plots. This automates a standard technique used by control engineers and greatly improves assurance compared with the traditional method of visual inspection of the Nichols plots.

This article presents an abstraction of Hoare logic to traced symmetric monoidal categories, a very general framework for the theory of systems. Our abstraction is based on a traced monoidal functor from an arbitrary traced monoidal category into the category of preorders and monotone relations. We give several examples of how our theory generalizes usual Hoare logics (partial correctness of while programs, partial correctness of pointer programs), and provide some case studies on how it can be used to develop new Hoare logics (runtime analysis of while programs and stream circuits).

\Ve assws the current state of research in the application of coluputcr aidd fbllal rCilsOIliIlg to couqmtrr illgt?~Jl'?l: ihlld argUC ~.llilt f?Ulbdtl(!dVWifiCat.iOllSUppOrt, idlOWS USCI'S t.0 eri,joy its hewfits bvit,liout wwstling wit.11 1:c?c:llilicalit,ics.We illust,rilte t.llis Claim by considering syuholir defiuitw intcgridion, autl prcscnt a Ycrifiable syubolic defiuit,c iIlWglX1 table look up: it systeru which ru,at,cllc!s a (picry comprising il.t1efiuit.cintegral with paraulct,crs ant1 sitlo c:onrlit.ious.iqqiiist.au cnt.r\; iu a W!rifiabk tahlc autl uses a c:a.ll to a librarv of leninias almut t.hc ITids in the tlicwrenl prover P\,'S t.0 Rid iii t.h: I;rilIlsfOrnlatiOIl of the tal.)lC cI1t.qiIlt0 it11 Xlsw-er.11-0 present tlw full model of such il syst~cul as well ilS a tloscriptiou Of our prototype i~ll~,leme~lt,a.tio~~showiug the efficacy of such a syst.eul:for examplc~ the protol.qv2 is al~lc I.0 obtaiu correct.answers in CRSW w-hcrc coinputcr illgehr~~ S~RkIllS [CAYS] Cl0 IlOt.11,-f?('XtCIM.1 Ill)011 Ehtf3n?lIl'S WlY!~)-bilSf!tltable by iuclutling piumllet.ric'IiuliLs of iut,cgra t ion ad queries with side coiidit.ious.

In this paper we demonstrate the use of formal methods tools to provide a semantics for the type hierarchy of the AXIOM computer algebra system, and a methodology for Aldor program analysis and verification. We give examples of abstract specifications of AXIOM primitives, and provide an interface between these abstractions and Aldor code. 1 Introduction We describe work in progress at St Andrews to apply formal methods and machine assisted theorem proving techniques to improve the robustness and reliability of computer algebra systems. This project considers the use of the Larch [7] approach to formal methods through specifications and uses AXIOM [8] for the computer algebra system. We do not exclude other formal methods systems such as VDM [9] or Z [13] nor do we exclude applications to other computer algebra systems (CAS) such as Mathematica [17] or Maple [14]. Indeed the weaker type systems used by the latter packages may benefit more from our approach than AXIOM can. In the remai...

Abstract We consider total well-founded orderings on monadic terms satisfying the replacement and full invariance properties. We show that any such ordering on monadic terms in one variable and two unary function symbols must have order typeω,ω2orωω. We show that a familiar construction gives rise to continuum many such orderings of order typeω. We construct a new family of such orderings of order typeω2, and show that there are continuum many of these. We show that there are only four such orderings of order typeωω, the two familiar recursive path orderings and two closely related orderings. We consider also total well-founded orderings onNnwhich are preserved under vector addition. We show that any such ordering must have order typeωkfor some 1 ≤k≤n. We show that ifk

We describe two new families of orderings on words, and show that each has continuum many distinct members.

Total well-founded orderings on monadic terms satisfying the replacement and full invariance properties are considered. It is shown that any such ordering on monadic terms in one variable and two unary function symbols must have order type omega , omega /sup 2/, or omega /sup omega /. It is further shown that a familiar construction gives rise to continuum many such orderings of order type omega . A new family of such orderings of order type omega is constructed, and it is shown that there are only four such orderings of order type omega /sup omega /, the two familiar recursive path orderings and two closely related orderings. It is shown that any total well-founded ordering on N/sup n/ that is preserved under vector addition must have order type omega /sup lambda / for some 1>