Travelled to:1 × Estonia
1 × Germany
1 × USA
1 × United Kingdom
2 × France
Collaborated with:A.Bundy J.Richardson I.Green C.Castellini B.J.Ross F.v.Harmelen D.Lacey A.Armando J.Hesketh B.L.Richards I.Kraan G.A.Wiggins C.Horn A.Ireland
Talks about:proof (5) program (4) logic (4) synthesi (3) order (3) plan (3) system (2) recurs (2) higher (2) clam (2)
Person: Alan Smaill
DBLP: Smaill:Alan
Contributed to:
2005
20001998
199719941992
19911990Wrote 9 papers:
- CADE-2005-CastelliniS #first-order #logic #proving #theorem proving
- Proof Planning for First-Order Temporal Logic (CC, AS), pp. 235–249.
- CL-2000-LaceyRS #higher-order #logic programming #synthesis
- Logic Program Synthesis in a Higher-Order Setting (DL, JR, AS), pp. 87–100.
- CADE-1998-RichardsonSG #higher-order #logic #proving #theorem proving
- System Description: Proof Planning in Higher-Order Logic with Lambda-Clam (JR, AS, IG), pp. 129–133.
- ASE-1997-ArmandoSG #automation #paradigm #recursion #source code #synthesis
- Automatic Synthesis of Recursive Programs: The Proof-Planning Paradigm (AA, AS, IG), pp. 2–9.
- CADE-1994-RichardsKSW #logic #named
- Mollusc: A General Proof-Development Shell for Sequent-Based Logics (BLR, IK, AS, GAW), pp. 826–830.
- 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.
- ICLP-1991-RossS #algebra #prolog #semantics #termination
- An Algebraic Semantics of Prolog Program Termination (BJR, AS), pp. 316–330.
- 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.