LogiCS | Peter Skočovský

The main idea I'm interested in is how methodologies of Computer Engineering can be improved with formalization. Currently, Computer Engineering methodologies are quite informal and programmers often wonder why the code doesn't do what they want, when (or because) they didn't express this formally. Math, in particular Computer Science, has developed numerous formalizms that are supposed to be used in Computer Engineering, programmers just don't seem to be picking them up. I'm interested in improving this situation by developing methodologies that apply the existing formalizms to the problems with which the programmers actually struggle.
In particular, currently, I'm looking into how Description Logics can be used to formalize development of database applications. This is one of the areas for which Description Logics are tailored, however they are missing a number of natural features of databases, as finiteness, close world assumption, or possibility to change a database (change of the data, change of the schema, or change of the constraints).
In general I'm interested also in how higher level languages can help with development of programs that are automatically correct, or in how formal verification can help to understand what already existing programs actually do.

MSc: European Masters Program in Computational Logic (Technische Universität Dresden, Free University of Bozen - Bolzano, Technische Universität Wien, Universidade Nova de Lisboa)
BA: Information Technology (Brno University of Technology)

Yevgeny Kazakov, Peter Skocovský: Enumerating Justifications Using Resolution. IJCAR 2018: 609-626
Yevgeny Kazakov, Peter Skocovsky: Enumerating Justifications using Resolution. Description Logics 2017
Paula-Andra Busoniu, Johannes Oetsch, Jörg Pührer, Peter Skocovsky, Hans Tompits: SeaLion: An eclipse-based IDE for answer-set programming with advanced debugging support. TPLP 13(4-5): 657-673 (2013)