Program kolokvií s abstrakty pro semestr Podzim 1997

30. 9. 1997: Dr. Martin Schoenhacker, Vienna University of Technology; Visualization of Algorithms; Abstract: With algorithms constantly growing in size and complexity, modern computer science faces the problem that understanding -- let alone improving -- these algorithms gets increasingly difficult. Teaching them adequately is yet another problem. And there even are algorithms that can not possibly be followed without appropriate tools, for instance in multi-processor systems. All of these tasks can be made easier by using systems capable of the visualization of algorithms and corresponding data structures.
Following a general overview, the results of various experiments conducted over the last years will be used to illustrate useful applications of visualization techniques. One of the options, a typical algorithm operating on graphs, shows the usefulness of visualization in understanding problems that are not necessarily based in computer science.
7. 10. 1997: Prof. RNDr. Jaroslav Kral, KU Praha, FI Brno; Horizontalni integrace softwaru; Abstract: Co je horizontalni integrace. Nastroje horizontalni integrace. Vyhody a nevyhody horizonatalni a vertikalni integrace. Priklad vyuziti horizontalni integrace v softwaru firmy Lawson Software. V softwaru lze pozorovat obdobne tendence, jako v jinych oblastech vyroby. Postupne se prechazi od vertikalni integrace (vse pod jednou strechou), k integraci horizontalni (pruzna spoluprace, vice subjektu). Budou zmineny vyhody a a nevyhody obou pristupu. HI v softwaru ma navic tu vyhodu, ze je mozna pouze jsou-li pouzivany technologie, ktere ovlivni budoucnost softwaru. Vyhody horizontalni integrace budou ilustrovany na komercnim podnikovem reseni firmy Lawson Software, ktera jako prvni prisla s kvalitnim resenim pro web. Jinym prikladem je integrace workflow systemu a variantni reseni datoveho skladu. Budou zmineny podminky pro dosazeni stavu, kdy si bude skladat system zakaznik sam.
14. 10. 1997: Prof. Dr. Alexander Leitsch, TU Vienna; Resolution Decision Procedures and Automated Model Building; Abstract: Resolution is frequently considered just as a method to derive the empty clause from an unsatisfiable set of clauses. But by adjusting resolution refinements to specific syntactic properties of clause classes it can be turned into a decision procedure and even into a model-building method. We show how hyperresolution can be applied as a model building procedure in form of a postprocessing after the decision procedure. The method consists of an iteration of deductive closure and clause reduction and is completely backtracking-free. The final result of the procedure is an atomic (not necessesarily ground) representation of a Herbrand model. Moreover we define an algorithmic method of truth evaluation of clauses ("model checking") over (symbolic representations of) Herbrand models -- extending the range of model checking to infinite models; this method is again based on resolution, purely proof-theoretic and symbolic. Finally we show how decision procedures, model building and clause evaluation can be extended to Herbrand models with equality and present some open research problems and new techniques.
21. 10. 1997: Dr. Pavol Sevecek, FI Brno; Slovniky nove generace
4. 11. 1997: Doc. Petr Jancar, CSc, Technicka univerzita, Ostrava; Petriho site (osobni pohled); Abstract: Po obecnem uvodu venovanem Petriho sitim jakozto prostredku modelovani, navrhu a analyzy systemu, sa autor zameri hlavne na sve vysledky v teto oblasti. Jedna sa predevsim o vysledky zkoumajici meze algoritmicke verifikovatelnosti; jejich hlavni vysledky budou neformalne nastineny.
11. 11. 1997: Dr. Jiri Sgall, MU CAV Praha; Multiparty communication complexity; Abstract: One motivation for studying communication complexity is to use it as a tool for proving lower bounds on the boolean circuit complexity. We survey these connections and models of multiparty communication complexity studied in this context. Next we show some upper bounds showing that even some seemingly very restrictive models of communication can be surprisingly powerful. We conclude by open problems that demonstrate the current state of art in this area.
18. 11. 1997: Professor Dr. Hermann Maurer, Graz University of Technology, Austria; Content management and training aspects on large Web sites; Abstract: I will review problems arising when handling large Web sites with most current Web systems. Problems are mainly due to the fact that not enough support for "content" management is provided. I will argue that many tasks that could be handled automatically require manual intervention in most systems, that automatic data and link management are not just dreams, and that the combination of powerful Web servers with existing database systems provides optimal solutions for large Webs sites, also and particular for Intranet and educational applications. I will support my claims by discussing the WWW System Hyperwave in some detail and explaining a number of concrete examples. I will demonstrate life a umber of features so far unheared of in other systems. I will finally explain how Hyperwave as add-on allows a smooth migration path from current WWW servers to more managable environments, and that not only the information provider (webmaster) but also users profit dramatically from this process.
2. 12. 1997: Doc. Pavol Voda CSc, Ustav informatiky, MFF UK, Bratislava; Computer programming as mathematics; Abstract: CL (Clausal Language) is a computer programming language with mathematical syntax (no reserved words) suitable for the teaching of introduction to
* declarative programming,
* program specification and verification,
* computability theory.
We teach the three topics in three courses in the first two undergraduate years. This is possible only because we have designed CL as a minimal language supporting exactly the unary primitive recursive functions over natural numbers. CL is not only a programming language but it also contains its own proof system where one can state and prove properties of programs. The strength of the system is I\Sigma1-arithmetic which is a simple fragment of Peano arithmetic.
The domain of natural numbers is so well-known that students have no problem understanding the meaning (semantics) of functions of CL and have a good intuition about their properties. This should be contrasted with similar system with more complex and less intuitive domains as for instance PVS which is based on typed functionals. Our experience is that the students seem not only to understand but also enjoy the presentation in CL of the above extremely important topics of computer science. We will answer some FAQ's (frequently asked questions) about CL:
** Do we lose expressivity of the language by restricting CL to the domain of natural numbers?
** Is not the coding of data structures into natural numbers artificial and expensive?
** Do we lose efficiency of computation by restricting definitions in CL to the schemas of primitive recursive functions?
Why only primitive recursive functions, why not Ackermann?
We will argue that the answer to the first three questions is a resounding NO. The question (4) will be answered by appeal to the incompleteness theorem of Godel.
9. 12. 1997: Profesor Jiri Zlatuska, CSc, FI MU, Brno; Stepping stones to an information society; Abstract: The information revolution is radically transforming many patterns along which society and enterprises have traditionally worked. These changes do not bring just minor technological improvements, but indeed a fundamental transformation of our industry-based society into an information-based one. The changes are most visible and documented within the business world, but the synergy between technological and social shifts does not stop there. This talk concerns key trends and challenges which this development puts before us.
16. 12. 1997: Dr. Jana Kosecka PhD, University of California, Berkeley; Intelligent highway systems - From theory to practice and back to theory; Abstract: In this talk I will first give a brief overview of the activities carried out under the Intelligent Highway Systems Program over the past 5 years at UC Berkeley. This has been one of the most publicized projects in computing in recent times. I will present the basic concept of the Automated Highway, the overall architecture of the system and some of the practical and theoretical issues resolution of which led to a very successful demonstration of an Intelligent Highway Concept which took place in August 1997 in San Diego and attracted a lot of media attention.
In the second part of the talk I will show that the main aim of the project: to increase highway capacity and at the same time to preserve and improve safety of individual vehicles has led to the development of novel techniques in the area of verification of hybrid systems as well as the design of a new programming language for simulations of such systems. The successful operation of automated vehicle in dynamically changing environment and in the presence of other vehicles requires coordination of information from various sensors and control of various actuators. In the third part of my talk I'll present in more detail the design of automated vehicle control system using visual sensing which was done in collaboration with HONDA R&D North America.
Talk will be accompanied by video demonstrations.