Planning and Patching Proof - Artificial Intelligence and Symbolic Computation - page 36

[Dixon & Fleuriot, 2003] Dixon, L. and Fleuriot, J. D. (2003). IsaPlanner: A prototype
proof planner in Isabelle. In Proceedings of CADE'03 , Lecture Notes in Computer
Science.
[Duncan et al , 2004] Duncan, H., Bundy, A., Levine, J., Storkey, A. and Pollet, M.
(2004). The use of data-mining for the automatic formation of tactics. In Workshop
on Computer-Supported Mathematical Theory Development . IJCAR-04.
[Frank & Basin, 1998] Frank, I. and Basin, D. (1998). Search in games with incomplete
information: A case study using bridge card play. Artificial Intelligence , 100(1-
2):87-123.
[Frank et al , 1992] Frank, I., Basin, D. and Bundy, A. (1992). An adaptation of proof-
planning to declarer play in bridge. In Proceedings of ECAI-92 , pages 72-76, Vi-
enna, Austria. Longer Version available from Edinburgh as DAI Research Paper
No. 575.
[Gow, 2004] Gow, Jeremy. (2004). The Dynamic Creation of Induction Rules Using
Proof Planning . Unpublished Ph.D. thesis, Division of Informatics, University of
Edinburgh.
[Hutter & Kohlhase, 1997] Hutter, D. and Kohlhase, M. (1997). A colored version of
the λ -Calculus. In McCune, W., (ed.), 14th International Conference on Automated
Deduction , pages 291-305. Springer-Verlag. Also available as SEKI-Report SR-95-
05.
[Ireland & Bundy, 1996] Ireland, A. and Bundy, A. (1996). Productive use of failure in
inductive proof. Journal of Automated Reasoning , 16(1-2):79-111. Also available
from Edinburgh as DAI Research Paper No 716.
[Ireland, 1992] Ireland, A. (1992). The Use of Planning Critics in Mechanizing Induc-
tive Proofs. In Voronkov, A., (ed.), International Conference on Logic Programming
and Automated Reasoning - LPAR 92, St. Petersburg , Lecture Notes in Artificial
Intelligence No. 624, pages 178-189. Springer-Verlag. Also available from Edin-
burgh as DAI Research Paper 592.
[Jackson & Lowe, 2000] Jackson, M. and Lowe, H. (June 2000). XBarnacle: Making
theorem provers more accessible. In McAllester, D., (ed.), CADE17 , number 1831
in Lecture Notes in Computer Science, Pittsburg. Springer.
[Kraan et al , 1996] Kraan, I., Basin, D. and Bundy, A. (1996). Middle-out reasoning
for synthesis and induction. Journal of Automated Reasoning , 16(1-2):113-145.
Also available from Edinburgh as DAI Research Paper 729.
[Lowe & Duncan, 1997] Lowe, H. and Duncan, D. (1997). XBarnacle: Making theorem
provers more accessible. In McCune, William, (ed.), 14th International Conference
on Automated Deduction , pages 404-408. Springer-Verlag.
[Lowe et al , 1998] Lowe, H., Pechoucek, M. and Bundy, A. (1998). Proof planning for
maintainable configuration systems. Artificial Intelligence in Engineering Design,
Analysis and Manufacturing , 12:345-356. Special issue on configuration.
[Monroy et al , 1994] Monroy, R., Bundy, A. and Ireland, A. (1994). Proof Plans for the
Correction of False Conjectures. In Pfenning, F., (ed.), 5th International Confer-
ence on Logic Programming and Automated Reasoning, LPAR'94 , Lecture Notes
in Artificial Intelligence, v. 822, pages 54-68, Kiev, Ukraine. Springer-Verlag. Also
available from Edinburgh as DAI Research Paper 681.
[Silver, 1985] Silver, B. (1985). Meta-level inference: Representing and Learning Con-
trol Information in Artificial Intelligence . North Holland, Revised version of the
author's PhD thesis, Department of Artificial Intelligence, U. of Edinburgh, 1984.