Publications

Always in need of updating!
Last updated: Feb 2014.


2014

  • MixR paper.
    (pdf)
  • Spreadsheets paper.
    (pdf)

2013

  • Designing Inference Rules for Spider Diagrams.
    Stapleton, G., Jamnik, M. and Urbas, M. (2013).
    VLHCC 2013. IEEE. Forthcoming.
    (pdf)

2012

  • Diabelli: A heterogeneous proof system.
    Urbas, M. and Jamnik, M. (2012).
    In Gramlich, B., Miller, D. and Sattler, U., (eds.), IJCAR, volume 7364 of Lecture Notes in Artificial Intelligence, pages 559--566. Springer.
    (pdf)
  • Speedith: A diagrammatic reasoner for spider diagrams.
    Urbas, M. and Jamnik, M. (2012).
    In Cox, P.T., Plimmer, B. and Rodgers, P.J., (eds.), Diagrams, volume 7352 of Lecture Notes in Artificial Intelligence, pages 163--177. Springer.
    (pdf)

2011

  • Heterogeneous Proofs: Spider Diagrams meet Higher-Order Provers.
    Urbas, M. and Jamnik, M. (2011).
    In van Eekelen, M., Geuvers, H., Schmaltz, J. and Wiedijk, F., (eds.), ITP, volume 6898 of Lecture Notes in Computer Science, pages 376--382. Springer.
    (pdf)

2010

  • Diagrammatic Representation and Inference, 6th International Conference, Diagrams 2010, Proceedings.
    Goel, A.K., Jamnik, M. and Narayanan, N.H., editors. (2010).
    Volume 6170 of Lecture Notes in Artificial Intelligence. Springer.
    (book link)
  • Heterogeneous reasoning in real arithmetic.
    Urbas, M. and Jamnik, M. (2010).
    In A.K. Goel, M. Jamnik, and N.H. Narayanan, editors, Diagrammatic Representation and Inference, 6th International Conference, Diagrams 2010, Proceedings, number 6170 in Lecture Notes in Artificial Intelligence, pages 345--348. Springer.
    (pdf)

2008

  • Diagrammatic reasoning in separation logic.
    Ridsdale, M., Jamnik, M., Benton, M. and Berdine, J. (2008).
    In Stapleton, G., Howse, J. and Lee, J., (eds.), Diagrammatic Representation and Inference, 5th International Conference, Diagrams 2008, Proceedings, number 5223 in Lecture Notes in Artificial Intelligence, pages 408--411. Springer.
    (pdf)
  • Combined reasoning by automated cooperation.
    Benzmueller, C., Sorge, V., Jamnik, M. and Kerber, M. (2008)
    Journal of Applied Logic, 6(3):318--342. Elsevier.
    (postscript, pdf)
  • Can machines reason?
    Jamnik, M. (2008)
    Research Horizons, 5:13. Cambridge University Press.
    (pdf)

2007

  • Kako sklepajo stroji? (How can machines reason?).
    Jamnik, M. (2007)
    EMZIN - Revija za kulturo, Letnik 17(3-4):88--89.
  • Lahko stroji sklepajo kot ljudje v matematiki? (Can machines reason like humans in mathematics?).
    Jamnik, M. (2007)
    Konferenca slovenskih znanstvenikov in gospodarstvenikov iz sveta in Slovenije, 5:64--67. Slovenian World Congress.

2006

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

2005

  • Computer scientist and a woman?
    Jamnik, M. (2005)
    Computing. 9 June 2005.
    (pdf)

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

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

  • Can a higher-order and a first-order theorem prover cooperate?
    Benzmueller, C., Sorge, V., Jamnik, M. and Kerber, M. (2005)
    In Baader, F. and Voronkov, A., (eds.), Proceedings of the 11th International Conference on Logic for Programming and Automated Reasoning, LPAR 2004, number 3452 in Lecture Notes in Artificial Intelligence, pages 415--431. Springer Verlag.
    (pdf)

  • Psychological validity of schematic proofs.
    Jamnik, M. and Bundy, A. (2005)
    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.
    (pdf)

2004

  • An experimental comparison of diagrammatic and algebraic logics.
    Winterstein, D., Bundy, A., Gurr, C. and Jamnik, M. (2004)
    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.
    (pdf)

  • On differences between the real plane and physical plane.
    Winterstein, D., Bundy, A. and Jamnik, M. (2004)
    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.
    (article link)

2003

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

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

  • Learning strategies for mechanised building of decision procedures.
    Jamnik, M. and Janicic, P. (2003)
    Electronic Notes in Theoretical Computer Science, 86(1):174--189.
    (pdf)

  • Can decision procedures be learnt automatically?
    Jamnik, M. and Janicic, P. (2003)
    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.
    (pdf)

2002

  • Automatic learning in proof planning.
    Jamnik, M., Kerber, M. and Pollet, M. (2002)
    In van Harmelen, F., (ed.), Proceedings of 15th ECAI, pages 282--286. European Conference on Artificial Intelligence, IOS Press.
    (pdf)

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

  • Using animation in diagrammatic theorem proving.
    Winterstein, D., Bundy, A., Gurr, C. and Jamnik, M. (2002)
    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.
    (pdf)

2001

  • Mathematical Reasoning with Diagrams: From Intuition to Automation.
    Jamnik, M. (2001)
    CSLI Press, Stanford, CA, USA.
    (Book link)

  • Agent based mathematical reasoning.
    Benzmueller, C., Jamnik, M., Kerber, M. and Sorge, V. (2001)
    Electronic Notes in Theoretical Computer Science, 23(3):21--33.
    (pdf)

  • Experiments with an agent-oriented reasoning system.
    Benzmueller, C., Jamnik, M., Kerber, M. and Sorge, V. (2001)
    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.
    (pdf)

  • Towards learning new methods in proof planning.
    Jamnik, M., Kerber, M. and Benzmueller, C. (2001)
    In Kerber, M. and Kohlhase, M., (eds.), Symbolic Calculation and Automated Reasoning: The Calculemus 2000 Symposium, pages 141--156, Natick, MA. A K Peters.
    (pdf)

  • Resource guided concurrent deduction.
    Benzmueller, C., Jamnik, M., Kerber, M. and Sorge, V. (2001)
    In Kerber, M. and Kohlhase, M., (eds.), Symbolic Calculation and Automated Reasoning: The Calculemus 2000 Symposium, pages 243--244, Natick, MA. A K Peters.
    (pdf)

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.