|
|
Drama manager by means of Petri Nets
Abonyi, Adam ; Brom, Cyril (advisor) ; Šerý, Ondřej (referee)
The results of virtual storytelling are used in interactive computer games or e-learning applications. The plot of a virtual story can be viewed as a distributed system, which was formalized by Carl Adam Petri in his work called Petri nets. This formalism was already used in the virtual storytelling area, but it was never used for describing a story in a virtual environment. In our work, we extend the basic Petri net model in a way which makes it easily usable for the specification of a plot of the story and for its progression. We also implement the model together with debugging tools. Moreover, we allow representing of stories using XML based format, which enables easy collaboration between the programmer and the author of the story.
|
|
|
IntelliSense Integration for Coq Theorem Prover
Abonyi, Adam ; Petříček, Tomáš (advisor) ; Bednárek, David (referee)
Computer-assisted (interactive) theorem provers are software tools that help with the development of formal proofs. While theorem provers are constantly evolving and have started to be used more often over the last decade, the development tools used for creating computer-assisted proofs have not improved as much and they do not offer features that are common to other modern development tools. This thesis aims to improve the state of the art of development tools for interactive theorem provers, namely Coq. We integrate the Coq interactive theorem prover into an existing modern development environment and bring the benefits of modern tools to interactive proving. Improving the development tools could help popularize computer-assisted theorem proving and thus improve the quality of software by simplifying formal verification and by allowing development of verified hardware.
|
|
|
Drama manager by means of Petri Nets
Abonyi, Adam ; Šerý, Ondřej (referee) ; Brom, Cyril (advisor)
The results of virtual storytelling are used in interactive computer games or e-learning applications. The plot of a virtual story can be viewed as a distributed system, which was formalized by Carl Adam Petri in his work called Petri nets. This formalism was already used in the virtual storytelling area, but it was never used for describing a story in a virtual environment. In our work, we extend the basic Petri net model in a way which makes it easily usable for the specification of a plot of the story and for its progression. We also implement the model together with debugging tools. Moreover, we allow representing of stories using XML based format, which enables easy collaboration between the programmer and the author of the story.
|
guest ::
