Travelled to:1 × Australia
1 × Belgium
1 × France
1 × Germany
1 × Hungary
1 × Ireland
1 × Italy
1 × Spain
2 × United Kingdom
8 × USA
Collaborated with:∅ I.Green I.Kraan J.Whittle H.Lowe J.Hesketh A.Smaill R.J.Boulton A.Ireland A.Blewitt I.Stark T.Walsh D.A.Basin D.Hutter F.v.Harmelen L.Sterling B.Welham M.Chan J.Lehmann G.Steel M.Maidl D.Winterstein C.A.Gurr S.Colton P.Janicic R.Monroy L.A.Dennis A.Nunes J.A.Abourbih L.Blaney F.McNeill K.Slind M.J.C.Gordon P.Madden G.A.Wiggins C.Horn
Talks about:proof (9) program (8) induct (6) use (6) logic (5) plan (5) synthesi (4) automat (4) reason (4) verif (4)
Person: Alan Bundy
DBLP: Bundy:Alan
Facilitated 1 volumes:
EdContributed to:
2010
2010
200520042001
200019991999199819981997
19971996
1993
199319921992199119901988198819821980Wrote 29 papers:
- IJCAR-2010-AbourbihBBM #automation #calculus
- A Single-Significant-Digit Calculus for Semi-Automated Guesstimation (JAA, LB, AB, FM), pp. 354–368.
- KEOD-2010-ChanLB #automation #evolution #higher-order #ontology #reasoning #representation
- Higher-order Representation and Reasoning for Automated Ontology Evolution (MC, JL, AB), pp. 84–93.
- ASE-2005-BlewittBS #automation #design pattern #java #verification
- Automatic verification of design patterns in Java (AB, AB, IS), pp. 224–232.
- IJCAR-2004-SteelBM #induction #protocol
- Attacking a Protocol for Group Key Agreement by Refuting Incorrect Inductive Conjectures (GS, AB, MM), pp. 137–151.
- IJCAR-2004-WintersteinBG #diagrams #proving #theorem proving
- Dr.Doodle: A Diagrammatic Theorem Prover (DW, AB, CAG), pp. 331–335.
- ASE-2001-BlewittBS #automation #design pattern #java #verification
- Automatic Verification of Java Design Patterns (AB, AB, IS), pp. 324–327.
- ICML-2000-ColtonBW #automation #concept #identification
- Automatic Identification of Mathematical Concepts (SC, AB, TW), pp. 183–190.
- ASE-1999-WhittleBBL #editing #ml
- An ML Editor Based on Proofs-As-Programs (JW, AB, RJB, HL), pp. 166–173.
- CADE-1999-HutterB #contest #design #induction #proving #theorem proving
- The Design of the CADE-16 Inductive Theorem Prover Contest (DH, AB), pp. 374–377.
- CADE-1999-JanicicBG #flexibility #framework #integration #proving #theorem proving
- A Framework for the Flexible Integration of a Class of Decision Procedures into Theorem Provers (PJ, AB, IG), pp. 127–141.
- CADE-1999-WhittleBBL
- System Description: CyNTHIA (JW, AB, RJB, HL), pp. 388–392.
- ASE-1998-MonroyBG #equation #verification
- Planning Equational Verification in CCS (RM, AB, IG), pp. 43–52.
- CADE-1998-SlindGBB #interface
- System Description: An Interface Between CLAM and HOL (KS, MJCG, RJB, AB), pp. 134–138.
- CADE-1997-DennisBG #bisimulation #induction #proving #using
- Using A Generalisation Critic to Find Bisimulations for Coinductive Proofs (LAD, AB, IG), pp. 276–290.
- PLILP-1997-WhittleBL #editing #ml #standard
- An Editor for Helping Novices to Learn Standard ML (JW, AB, HL), pp. 389–405.
- CADE-1996-IrelandB #induction #proving
- Extensions to a Generalization Critic for Inductive Proof (AI, AB), pp. 47–61.
- ICLP-1993-KraanBB #logic programming #reasoning #synthesis
- Middle-Out Reasoning for Logic Program Synthesis (IK, DAB, AB), pp. 441–455.
- LOPSTR-1993-MaddenHGB #automation #generative #performance #proving #source code #theorem proving #using
- A General Technique for Automatically Generating Efficient Programs Through the Use of Proof Planning (PM, JH, IG, AB), pp. 64–66.
- CADE-1992-HeskethBS #reasoning #recursion #source code #synthesis #using
- Using Middle-Out Reasoning to Control the Synthesis of Tail-Recursive Programs (JH, AB, AS), pp. 310–324.
- CADE-1992-WalshNB #proving #theorem proving #using
- The Use of Proof Plans to Sum Series (TW, AN, AB), pp. 325–339.
- LOPSTR-1992-KraanBB #logic programming #proving #synthesis #theorem proving
- Logic Program Synthesis via Proof Planning (IK, DAB, AB), pp. 1–14.
- LOPSTR-1991-WigginsBKH #induction #logic programming #proving #source code #synthesis
- Synthesis and Transfomation of Logic Programs from Constructive, Inductive Proof (GAW, AB, IK, JH), pp. 27–45.
- CADE-1990-Bundy #reasoning
- A Science of Reasoning: Extended Abstract (AB), pp. 633–640.
- CADE-1990-BundyHHS
- The Oyster-Clam System (AB, FvH, CH, AS), pp. 647–648.
- CADE-1990-BundyHSI #induction #proving
- Extensions to the Rippling-Out Tactic for Guiding Inductive Proofs (AB, FvH, AS, AI), pp. 132–146.
- CADE-1988-Bundy #induction #proving #using
- The Use of Explicit Plans to Guide Inductive Proofs (AB), pp. 111–120.
- JICSCP-1988-Bundy88 #logic programming
- A Broader Interpretation of Logic in Logic Programming (AB), pp. 1624–1648.
- CADE-1982-SterlingB #verification
- Meta-Level Inference and Program Verification (LS, AB), pp. 144–150.
- CADE-1980-BundyW #algebra #multi #using
- Using Meta-Level Inference for Selective Application of Multiple Rewrite Rules in Algebraic Manipulation (AB, BW), pp. 24–38.