Martin Suda

Education

M.S. in Computer Science (2007), Faculty of Mathematics and Physics, Charles University, Prague

Current

I am a PhD student at the Department of Theoretical Computer Science and Mathematical Logic, Faculty of Mathematics and Physics, Charles University.
My supervisor is Prof. RNDr. Petr Stepanek, DrSc..

Research Interests

I am interested in automated theorem provers for first order logic, especially modern saturation-based provers like SPASS, E or Vampire. I would like to investigate how these provers could be better adapted for use in their new application areas such as bioinformatics or large ontologies. In particular, I am currently interested in the possibility of accessing an external function (search function, database access) from the prover loop.

Projects

SPASS-XDB

Publications

A PLTL-Prover Based on Labelled Superposition with Partial Model Guidance
M. Suda, C. Weidenbach, in IJCAR 2012 (eds. B. Gramlich, D. Miller, and U. Sattler), LNAI 7364, pp. 537-543. Springer, Heidelberg (2012)

Labelled Superposition for PLTL
M. Suda, C. Weidenbach, in LPAR-18 (eds. N. Björner and A. Voronkov), LNCS 7180, pp. 391-405. Springer, Heidelberg (2012)

On the Saturation of YAGO
M. Suda, C. Weidenbach, P. Wischnewski, in 5th International Joint Conference on Automated Reasoning, IJCAR 2010 (eds. J. Giesl, R. Hähnle), LNCS 6173, pp. 441-456. Springer, Heidelberg (2010)

Progress Towards Effective Automated Reasoning with World Knowledge [PDF]
G. Sutcliffe, M. Suda, A. Teyssandier, N. Dellis, G. de Melo, in Proceedings of the 23rd International FLAIRS Conference, AAAI Press, Menlo Park, CA, USA. (2010)

External Sources of Axioms in Automated Theorem Proving [PDF]
M. Suda, G. Sutcliffe, P. Wischnewski, M. Lamotte-Schubert, G. de Melo, in Proceedings of the 32nd Annual Conference on Artificial Intelligence (eds. B. Mertsching), LNAI 5803, pp. 281-288. Springer, Heidelberg (2009)

SPASS Version 3.5 [PDF]
C. Weidenbach, D. Dimova, A. Fietzke, R. Kumar, M. Suda, and P. Wischnewski, in Automated Deduction – CADE-22 Proceedings (eds. R. A. Schmidt), LNCS (LNAI), vol. 5663, pp. 140-145. Springer, Heidelberg (2009)

Relevancy Zones for Lambda Search in Rigid Board Games [PDF]
M. Suda, in WDS'08 Proceedings of Contributed Papers: Part I - Mathematics and Computer Sciences (eds. J. Safrankova and J. Pavlu), Prague, Matfyzpress, pp. 151-158, 2008.

Effective Algorithms for Verifying Goals in Computer Games [PDF (czech only)]
M. Suda. My master degree diploma thesis (2007).

Rocnikove projekty

Studenti se zajmem o rocnikovy projekt pod mym vedenim, nejlepe z oblasti automatickeho dokazovani, ci obecneji umele inteligence, necht mne kontaktuji emailem.

Stranka s nekolika napady.

updated: 30. 6. 2012