Publications 19982003

Automatic synthesis of recursive programs: the proof
planning
paradigm
A. Armando,
A.Smaill,
I. Green
1999, electronic
copy
 Automating the synthesis of decision
procedures in constructive metatheory
A. Armando,
J. Gallacher, A.
Smaill,
A.
Bundy
1998, electronic
copy
 14th International Conference on Theorem
Proving in Higher
Order Logics: TPHOLs 2001
Volume 2152 of Lecture Notes in
Computer Science,
Springer Verlag
R. Boulton,
P. B. Jackson, editors
September, 2001. Online at
http://link.springer.de/link/service/series/0558/tocs/t2152.htm
 The automation of proof by mathematical
induction
A.
Bundy
2001, electronic
copy
 An intelligent tutoring system for induction
proofs
A.
Bundy, J.
Moore, C.
Zinn
1999, electronic
copy
 Proofs about lists using ellipsis
A.
Bundy,
J.
Richardson
1999, electronic
copy
 A bridge tutoring system
R. Burns
Master's thesis, Division of
Informatics, University
of Edinburgh
2001, electronic
copy
 A systematic
presentation of quantified modal
logics
C. Castellini,
A.
Smaill
2002, abstract,
electronic copy
 Proof planning
for feature interactions: a
preliminary report
C. Castellini,
A.
Smaill
2002, electronic copy
 Tacticbased
theorem proving in firstorder
modal and temporal logics
C. Castellini,
A.
Smaill
2001, abstract,
electronic copy
 Automated theory
formation in pure mathematics
S. Colton
2002, amazon
 Automated theory
formation in pure mathematics
S. Colton
PhD thesis, Division of Informatics,
University
of Edinburgh, 2001
 Automatic
invention of integer sequences
S. Colton,
A. Bundy,
T. Walsh
2000, electronic copy
 On the notion of
interestingness in automated
mathematical discovery
S. Colton,
A.
Bundy, T.
Walsh
2000, electronic copy
 Artificial
intelligence and scientific
creativity
S. Colton,
G.
Steel
1999, electronic
copy
 Automatic
concept formation in pure
mathematics
S.
Colton,
A.Bundy
1999, abstract,
electronic copy
 Deductive
synthesis of recursive plans in
linear logic
S. Cresswell
PhD thesis, Division of Informatics,
University
of Edinburgh, 2001
 Deductive
synthesis of recursive plans in
linear logic
S. Cresswell,
J.
Richardson,
A.
Smaill
1999, electronic copy
 Logicbased
program synthesis via program
extraction
E. Denney
2002, electronic copy
 The synthesis of
a java card tokenisation
algorithm
E. Denney,
2001, electronic copy
 Correctness of
java card method lookup via
logical relations
E.
Denney,
T Jensen
2001, electronic abstract
 Ordinal
arithmetic: a case study for rippling
in a higher
order domain
L. Dennis,
A.
Smaill
2001, abstract,
electronic copy
 Making a
productive use of failure to
generate witnesses
for coinduction from divergent proof attempts
L. Dennis,
A.Bundy,
I. Green
1999, electronic copy
 IsaPlanner: a
prototype of proof planner in
Isabelle
L.
Dixon, J.
Fleuriot
2003, electronic
copy
 An operational
semantics of the java card
firewall
M.
Éluard, T. Jenson, E. Denney
2001, electronic
copy
 An abstract
formalisation of correct schemas
for program synthesis
P. Flener,
K. K.
Lau, M. Ornaghi, J. Richardson
2000,
electronic copy
 A unified view
of programming schemas and
proof methods
P. Flener,
J. Richardson
1999, electronic copy
 A combination of
geometry theorem proving and
nonstandard
analysis, with application to Newton's Principia
J.
Fleuriot
2001, amazon
 Nonstandard
geometric proofs
J.
Fleuriot
2001,
Springer
link
 Theorem proving
in infinitesimal geometry
J.
Fleuriot
2001, electronic
abstract
 Mechanizing
nonstandard real analysis
J.
Fleuriot ,
L. Paulson
2000,
electronic abstract
 On the
mechanization of real analysis in
Isabelle/HOL
J.
Fleuriot
2000, electronic copy
 Extensions to
the estimation calculus
J.
Gow,
A.
Bundy, I. Green
1999, abstract,
electronic copy
 Solving
integrals at the method level
A.
Heneveld, E. Maclean,
A.
Bundy, J.
Fleuriot, A.
Smaill
2000, electronic copy
 Memorybased
problem solving and schema
induction in Go
A.
Heneveld, A.
Bundy, M. Ramscar,
J.
Richardson
2000, electronic
copy
 Schema induction
via analogy
A.
Heneveld
Master's thesis, Division of
Informatics, University
of Edinburgh, 1999
 More automatic
diagnosis of arithmetic errors
E. Hughes
Master's thesis, Division of
Informatics, University of Edinburgh, 2003
 Interactive
proof critics
A. Ireland,
M. Jackson, G.
Reid
2001, electronic copy
 Proof planning
for strategy development
A. Ireland,
J. Stark
2001, Annals
of Mathematics and AI link
 Automatic
verification of functions with
accumulating parameters
A. Ireland,
A.
Bundy
1999, electronic copy
 Formal Aspects
of Computing
A. Ireland,
M. Jackson, G.
Reid
1999, Springer
link
 On the automatic
discovery of loop invariants
A. Ireland,
J. Stark
1997, electronic copy
 Interactive
proof critics in XBarnacle
M. Jackson, H. Lowe
2000
 Interacting with
semiautomated theorem
provers via interactic
proof critics
M. Jackson
PhD thesis, School of Computing,
Napier University, 1999
 Using ERMIA for
the evaluation of a theorem
prover interface
M. Jackson, D.
Benyon, H.
Lowe
1998, electronic copy
 Mathematical
reasoning with diagrams: from
intuition to automation
M.
Jamnik
2001, link to book
 Automating
diagrammatic proofs of arithmetic
arguments
M.
Jamnik
PhD
thesis, Division of Informatics, University
of Edinburgh, 1999
 Verification of
diagrammatic proofs
M.
Jamnik,
A.
Bundy, I. Green
1998, abstract,
electronic copy
 On automating
diagrammatic proofs of
arithmetic arguments
M.
Jamnik,
A.
Bundy, I.Green
1998, abstract,
electronic copy
 Building
decision procedures into theorem
provers
P.
Janicic
PhD thesis, Faculty of Mathematics,
University of Belgrade, 2001
 A general
setting for flexibly combining and
augmenting
decision procedures
P.
Janicic, A.
Bundy
2001,
electronic
copy
 Strict general
setting for building decision
procedures into
theorem provers
P.
Janicic, A.
Bundy
2001, electronic
copy
 A framework for
the flexible integration of a
class of
decision procedures into theorem provers
P.
Janicic,
A.
Bundy, I.Green
1999, abstract,
electronic copy
 Logic program
synthesis in a higher order
setting
D.
Lacey,
J.
Richardson
A.
Smaill
2000, electronic
copy
 Propositional,
probabilistic and evidential
reasoning
W.
Liu
2001, link
to book
 The method of
assigning incidences
W.
Liu, D. McBryan, A.
Bundy
2000, electronic
copy
 Proof planning
for maintainable configuration
systems
H. Lowe,
M.
Pechoucek, A.
Bundy
1998, electronic
copy
 Proofplanning
nonstandard analysis
E.
Maclean, J.
Fleuriot, A.
Smaill
2002,
abstract, electronic copy
 Automating proof
in nonstandard analysis
E.
Maclean
2001, electronic
copy
 Dynamic ontology
refinement
F.
McNeill, A.
Bundy,
M.
Schorlemmer
2003, electronic copy
 Analogy in
inductive theorem proving
E. Melis,
J. Whittle
1998, electronic
copy
 Symmetry and
complexity in propositional
reasoning
J. Molony
PhD thesis, Division of Informatics,
University of Edinburgh, 2001
 On the
correction of faulty formulae
R. Monroy,
A.
Bundy
2001,
electronic copy
 Searching for a
solution to program
verification = equation
solving in CCS
R. Monroy,
A.
Bundy, I. Green
2000, electronic copy
 Planning proofs
of equations in CCS
R. Monroy,
A.
Bundy, I. Green
href="9803/monroy00.ps.gz">
electronic copy
 OBSERVANT: An
annotated termrewriting system
for deciding observation congruence
R. Monroy,
A.
Bundy, I. Green
1998,
electronic copy
 Planning
equational verification in CCS
R. Monroy,
A.
Bundy, I. Green
1998, electronic copy
 Planning proofs
of correctness of CCS systems
R. Monroy
PhD
thesis, Division of Informatics,
University of Edinburgh, 1997
 On process
equivalence=equation solving in
CCS
R. Monroy,
A.
Bundy
2001,
electronic copy
 Lakatosstyle
reasoning
A.
Pease, S.
Colton, A.
Smaill, J.
Lee
2002, electronic
copy
 Semantic
negotiation: modelling ambiguity in
dialogue
A.
Pease, S.
Colton, A.
Smaill, J.
Lee
2002, electronic copy
 A multiagent
approach to modelling
interaction in human mathematical reasoning
A.
Pease, S.
Colton, A.
Smaill, J.
Lee
2001, abstract,
electronic copy
 Proof planning
with schema frameworks
J. Richardson
1998, electronic copy
 Continuations of
proof strategies
J. Richardson,
A.
Smaill
2001, electronic copy
 System
description: proof planning in
higherorder logic with lambdaclam
J. Richardson,
A.
Smaill,
I.Green
1998, electronic copy
 Automatic
diagnosis of arithmetic errors
K. Rigden
Undergraduate project dissertation,
Division of Informatics, University of Edinburgh, 2003
 Why solutions
can be hard to find: a featural
theory of cost
for a local search algorithm on random satisfiability instances
J. Singer
PhD
thesis, Division of Informatics, University
of Edinburgh, 2001
 Backbone
fragility and the local search cost
peak
J. Singer, I. Gent,
A. Smaill
2000, electronic copy
 Local search on
random 2 + psat
J. Singer, I. Gent,
A. Smaill
2000, electronic copy
 Higherorder
annotated terms for proof search
A.
Smaill, I. Green
1996, electronic copy
 Towards
automatic imperative program
synthesis through proof planning
J. Stark,
A. Ireland
1999, electronic
copy
 Invariant
discovery via failed proof attempts
J. Stark, A. Ireland
1998, electronic
copy
 Proof planning
for imperative program
development
J. Stark
PhD thesis, HeriotWatt University,
2000
 Attacking the
AsokanGinzboorg protocol for
key distribution in an adhoc bluetooth network using CORAL
G.
Steel, A.
Bundy, M.
Maidl
2003, electronic
copy
 Finding
counterexamples to inductive
conjectures and discovering
security protocol attacks
G.
Steel, A.
Bundy, E.
Denney
2002, abstract,
electronic copy
 Finding
counterexamples to inductive
conjectures and discovering
security protocol attacks
G.
Steel,
A.
Bundy, E.
Denney
2002, electronic
copy
 Crossdomain
mathematical concept formation
G.
Steel,
S. Colton,
A.
Bundy, T.
Walsh
2000, electronic
copy
 Crossdomain
concept formation using HR
G.
Steel
Master's thesis, Division of
Informatics, University
of Edinburgh, 1999,
abstract
 A tutor for
defence at bridge
T. Tang
Undergraduate project dissertation,
Division of Informatics, University
of Edinburgh, 2003
 An ML editor
based on proofsasprograms
J. Whittle,
A.
Bundy , R.
Boulton,
H. Lowe
1999, abstract,
electronic copy
 System
description: Cynthia
J. Whittle,
A.
Bundy , R.
Boulton,
H. Lowe
1999, abstract,
Springer
link
 The use of
proofsasprograms to build an
analogybased functional program editor
J. Whittle
PhD
thesis, Division of Informatics, University of Edinburgh,
1998
 An adversarial
planning approach to Go
S.
Willmott, J. Richardson,
J.
Levine
1999,
Springer link
 Applying
adversarial planning techniques to
Go
S.
Willmott, J. Richardson,
J.
Levine
1999, electronic copy
 Using animation
in diagrammatic theorem
proving
D.
Winterstein, A.
Bundy, C.
Gurr, M.
Jamnik
2002, electronic copy
 A proposal for
automatic diagrammatic
reasoning in continuous domains
D.
Winterstein, A.
Bundy, M.
Jamnik
2000, electronic copy
FORTHCOMING PUBLICATIONS

Rippling: Metalevel
guidance for mathematical
reasoning
A.
Bundy, D.
Basin, D.
Hutter, A.
Ireland
2003
 Combining proof
plans with partial ordering
for imperative
program synthesis
A. Ireland,
J. Stark
2003
 Using the CORAL
system to discover attacks on
security protocols
G.
Steel, A.
Bundy, E.
Denney
2003