Publications

Always in need of updating!
Last updated: Jan 2008.

2008

• diagrams and separation logic paper
• agents paper
• Jamnik, M.
  Can machines reason?
  Research Horizons, 5:13. Cambridge University Press. 2008.
  (pdf)

2007

• Jamnik, M.
  Kako sklepajo stroji? (How can machines reason?).
  EMZIN - Revija za kulturo, Letnik 17(3-4):88--89. 2007.
  
• Jamnik, M.
  Lahko stroji sklepajo kot ljudje v matematiki? (Can machines reason like humans in mathematics?).
  Konferenca slovenskih znanstvenikov in gospodarstvenikov iz sveta in Slovenije, 5:64--67. 2007. Slovenian World Congress.
  
• Benzmueller, C., Sorge, V., Jamnik, M. and Kerber, M.
  Combined reasoning by automated cooperation.
  Journal of Applied Logic, ?(?):?--? Elsevier. 2007. In print.
  (postscript, pdf)

2006

• Dennis, L.A., Jamnik, M. and Pollet, M.
  On the comparison of proof planning systems: LambdaClam, Omega and IsaPlanner.
  Electronic Notes in Theoretical Computer Science, 151(1):93--110. 2006. (postscript, pdf)

2005

• Computer scientist and a woman?. Computing. 9 June 2005.

• Computer scientist and a woman? Newsletter, page 14. Cambridge University Press, June/July 2005.

• What is a proof?. (with A. Bundy and A. Fugard). Philosophical Transactions of Royal Society A: The Nature of Mathematical Proof, 363(1835):2377--2391.

• Can a higher-order and a first-order theorem prover cooperate?. (with C. Benzmueller, V. Sorge and M. Kerber). In Proceedings of the 11th International Conference on Logic for Programming and Automated Reasoning, LPAR, Lecture Notes in Artificial Intelligence. Springer Verlag. 2005. To appear.

• Psychological validity of schematic proofs. (with A. Bundy). In Hutter, D. and Stephan, W., (eds.), Mechanizing Mathematical Reasoning: Essays in Honor of Joerg H. Siekmann on the Occasion of His 60th Birthday, number 2605 in Lecture Notes in Artificial Intelligence, pages 321--341. Springer Verlag. 2005.

2004

• An experimental comparison of diagrammatic and algebraic logics. (with D. Winterstein, A. Bundy and C. Gurr). In Blackwell, A., Marriott, K. and Shimojima, A., (eds.), Theory and Application of Diagrams: Third International Conference, Diagrams 2004, Proceedings, number 2980 in Lecture Notes in Artificial Intelligence, pages 432--434. Springer Verlag. 2004.

• On differences between the real plane and physical plane. (with D. Winterstein and A. Bundy). In Blackwell, A., Marriott, K. and Shimojima, A., (eds.), Theory and Application of Diagrams: Third International Conference, Diagrams 2004, Proceedings, number 2980 in Lecture Notes in Artificial Intelligence, pages 29--31. Springer Verlag. 2004.

2003

• Automatic learning of proof methods in proof planning. (with M. Kerber, M. Pollet and C. Benzmueller). Logic Journal of the IGPL, 11(6):647--673. 2003.

• Informal human mathematical reasoning. AISB Quarterly, 114:3. Society for the Study of Artificial Intelligence and Simulation of Behaviour. 2003.

• Learning strategies for mechanised building of decision procedures. (with P. Janicic). Electronic Notes in Theoretical Computer Science, 86(1). 2003.

• Can decision procedures be learnt automatically?. (with P. Janicic). In Dahn, I. and Vigneron, L., (eds.), Proceedings of the 4th International Workshop on First-order Theorem Proving, FTP 2003, pages 35--48. Universidad Politecnica de Valencia.

2002

• Automatic learning of proof methods in proof planning. (with M. Kerber, M. Pollet and C. Benzmueller). Technical Report CSRP-02-05, School of Computer Science, University of Birmingham. 2002.

• Automatic learning in proof planning. (with M. Kerber and M. Pollet). In van Harmelen, F., (ed.), Proceedings of 15th ECAI, pages 282--286. European Conference on Artificial Intelligence, IOS Press. Also available as Technical Report CSRP-02-03. 2002.

• LearnOmatic: System description. (with M. Kerber, M. Pollet and C. Benzmueller). In Voronkov, A., (ed.), 18th Conference on Automated Deduction, number 2392 in Lecture Notes in Artificial Intelligence, pages 150--155. Springer Verlag. 2002.

• Automatic learning in proof planning.. (with M. Kerber and M. Pollet). Technical Report CSRP-02-03, School of Computer Science, University of Birmingham. 2002.

• Using animation in diagrammatic theorem proving. (with D. Winterstein, A. Bundy, A. and C. Gurr). In Hegarty, M., Meyer, B. and Narayanan, H., (eds.), Theory and Application of Diagrams: Second International Conference, Diagrams 2002, Proceedings, number 2317 in Lecture Notes in Artificial Intelligence, pages 46--60. Springer Verlag. 2002.

2001

• Mathematical Reasoning with Diagrams: From Intuition to Automation. CSLI Press, Stanford, CA, USA. 2001.

• Experiments with an agent-oriented reasoning system. (with C. Benzmueller, M. Kerber and V. Sorge). In Baader, F., Brewka, G. and Eiter, T., (eds.), Proceeding of the KI 2001: Advances in Artificial Intelligence, number 2174 in Lecture Notes in Artificial Intelligence, pages 409--424. Springer Verlag. 2001.

• Agent based mathematical reasoning. (with Benzmueller, C., Kerber, M. and Sorge, V.) Electronic Notes in Theoretical Computer Science, 23(3):21--33. 2001. Also appeared in Benzmueller et al, 1999.

• Learning method outlines in proof planning. (with M. Kerber and C. Benzmueller). Technical Report CSRP-01-08, School of Computer Science, University of Birmingham. 2001.

• Towards learning new methods in proof planning. (with M. Kerber and C. Benzmueller). In Kerber, M. and Kohlhase, M., (eds.), Symbolic Calculation and Automated Reasoning: The Calculemus 2000 Symposium, pp. 141-156. A K Peters. 2001. Also appeared at CADE-17 Workshop, 2000. Also available as Technical Report CSRP-00-09.

• Resource guided concurrent deduction. (with C. Benzmueller, M. Kerber, and V. Sorge). In Kerber, M. and Kohlhase, M., (eds.), Symbolic Calculation and Automated Reasoning: The Calculemus 2000 Symposium, pp. 243--244. A K Peters. 2001. Also appeared at AISB 2000.

2000

• A proposal for automatic diagrammatic reasoning in continuous domains.. (with D. Winterstein and A. Bundy). In Anderson, M., Cheng, P. and Haarslev, V., (eds.), Theory and Application of Diagrams: First International Conference, Diagrams 2000, Proceedings, number 1889 in Lecture Notes in Artificial Intelligence, pages 286--299. Springer Verlag. 2000.

• Towards learning new methods in proof planning. (with M. Kerber and C. Benzmueller). In Colton, S., Martin, U. and Sorge, V., (eds.), Proceedings of the CADE-17 Workshop on The Role of Automated Deduction in Mathematics, pp. 1--11. 2000. Also appeared at Calculemus 2000. Also available as Technical Report CSRP-00-09.

• Towards learning new methods in proof planning. (with M. Kerber and C. Benzmueller). Technical Report CSRP-00-09, School of Computer Science, University of Birmingham. 2000. Also appeared at Calculemus 2000.

• Resource guided concurrent deduction. (with C. Benzmueller, M. Kerber and V. Sorge). In Sloman, A., (ed.), Proceedings of the AISB-2000 Workshop: How to Design a Functioning Mind, pp. 137--138. Society for the Study of Artificial Intelligence and Simulation of Behaviour. 2000. Also appeared at Calculemus 2000.

1999

• Towards concurrent resource managed deduction. (with C. Benzmueller, M. Kerber, and V. Sorge). Technical Report CSRP-99-17, School of Computer Science, University of Birmingham. 1999.

• Agent based mathematical reasoning. (with C. Benzmueller, M. Kerber and V. Sorge). In Armando, A. and Jebelean, T., (eds.), Proceedings of the FLoC 1999 Calculemus Workshop: Systems for Integrated Computation and Deduction.

• Analogy and automated reasoning. Technical Report CSRP-99-14, School of Computer Science, University of Birmingham. 1999.

• On Automating Diagrammatic Proofs of Arithmetic Arguments. (with A. Bundy and I. Green). Journal of Logic, Language and Information. 8(3):297-321. 1999. Also available as Department of Artificial Intelligence Research Paper No. 910.

• On Automating Diagrammatic Proofs of Arithmetic Arguments. Unpublished PhD thesis. Division of Informatics, University of Edinburgh. 1999.

1998

• Verification of Diagrammatic Proofs. (with A. Bundy and I. Green). In Meyer, B., (ed.), Proceedings of the 1998 AAAI Fall Symposium on Formalising Reasoning with Visual and Diagrammatic Representations, pp. 23--30. American Association for Artificial Intelligence, AAAI Press. 1998. Also published in the Proceedings of ``Thinking With Diagrams 1998'' Workshop. Also available from Edinburgh as DAI Research Paper No. 924.

1997

• Automation of Diagrammatic Reasoning. (with A. Bundy and I. Green). In Pollack, M.E., (ed.), Proceedings of the 15th IJCAI, vol. 1, pp. 528--533. International Joint Conference on Artificial Intelligence, Morgan Kaufmann Publishers. 1997. Also published in the ``Proceedings of the 1997 AAAI Fall Symposium''. Also available from Edinburgh as DAI Research Paper No. 873.

• Automation of Diagrammatic Proofs in Mathematics. (with A. Bundy and I. Green). In Kokinov, B., (ed.), Perspectives on Cognitive Science, vol. 3, pp. 168--175. New Bulgarian University. 1997. Also available from Edinburgh as DAI Research Paper No. 835.