Part MMDCCXV
Future of Informatics - Chapter 6
Chapter 6: NEW, INFORMATICS DRIVEN, GENERAL
METHODOLOGY
CHAPTER 6:
NEW, INFORMATICS DRIVEN,
GENERAL METHODOLOGY
for SCIENCE, TECHNOLOGY, MEDICINE, ...
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 2/126
CONTENTS
Current main methodologies of science, technology, etc.
Basic components of the new methodology.
Power of the new methodology
Case study I - Modelling and simulation.
Case study II - Visualisation
Case study III - Algorithms design and analysis;
complexity theories impacts
Case study IV - Automated reasoning, theorem provers
and checkers
Grand challenges of new methodology
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 3/126
PROLOGUE
PROLOGUE
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 4/126
CHANGING THE MAIN PARADIGM of SCIENCES
We are currently witnessing an important change in
Science.
From
Galilean, Mathematics-driven, science,
that dominated science since its modern beginnings, and
during which the paradigms, concepts, methods, tools and
results of Mathematics have dominated,
to
Post-computer, Informatics-driven, science
at which paradigms, concepts, methods, tools and results
of Informatics dominate.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 5/126
LANGUAGES in WHICH NATURE IS WRITTEN
Galileo: Nature is written in the language of
mathematics.
Wolfram: Nature is written in the language of
computation.
New view: Nature is written in the language of
information processing.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 6/126
CURRENT MAIN BASIC METHODOLOGIES
There are currently two basic methodologies sciences,
technologies,.... have:
Experimental methodology (with observations and
experiments as main tools)
Theoretical methodology (with reasoning, deduction
and proofs as main tools)
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 7/126
ORIGINS
Modern science was borned when two basic
scientiﬁc methodology, experimental and
theoretical, started to be clearly formulated and
developed.
This happened in 17th century
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 8/126
ORIGINS of MODERN SCIENCE
Modern science and its two main methodologies are
usually seen as having its origin in 17-teen century in
critical rationalism of Descartes (1596-1650);
practical empiricism of Galileo Galilei(1564-1642); and
breathtaking contributions of Isac Newton (1642-1727).
Galileo’s main position was a concentration on:
making carefully chosen observations and experiments;
measuring things quantitatively and using quantitative
methods to process results of observations and
experiments,
thinking mathematically and
submitting theoretical outcomes/hypothesis to the
nature veriﬁcation/experiments.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 9/126
DEEP THOUGHTS of FOUNDERS
Measure what is measurable, and make measurable
what is not.
Galileo Galilei
All truths are easy to understand once they are
discovered. The point is to discover them.
Galileo Galilei
The Bible shows the way to go to heaven, not the way
heaven go.
Galileo Galilei
We cannot teach people anything, we can only help
them discover it within themselves.
Galileo Galilei
I think, therefore I am. R. Descartes
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 10/126
GALILEO GALILEI
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 11/126
INFORMATICS as a BASIS of a NEW METHODOLOGY
Informatics, as a symbiosis of a scientiﬁc and a technology
discipline, develops also basic ingredients of a
fundamentally new, in addition to deduction/theory and
observations/experiments, the third basic methodology for
all sciences, technologies, medicine, and society in general.
This new, informatics-based, methodology provides a new
way of thinking and new languages for science and other
areas, extending the Galilean
experiments/mathematics-based approach to science and
technology to new heights.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 12/126
NEW, INFORMATICS-DRIVEN, METHODOLOGY
Informatics-driven methodology subsumes and
extends the role and improves tools mathematics
used to play and oﬀer in advising, guiding and
serving other scientiﬁc and technology disciplines
and society in general.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 13/126
BASIC FEATURES of INFORMATICS-DRIVEN METHODOLOGY BRIEFLY
- I.
Modeling - Design of information processing models of
nature, men made, and virtual phenomena and
processes.
Simulation - Utilization of information processing
models to study natural, men-made and virtual
phenomena and processes.
Visualisation and animation of data, objects and
processes.
Virtualization - of systems and processes including
designs of the virtual reality systems and worlds.
Mining of information and knowledge from huge data
streams and sets.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 14/126
BASIC FEATURES of INFORMATICS-DRIVEN METHODOLOGY BRIEFLY
- II.
Design of systems for mechanized problem solving,
reasoning, learning and proofs designing as well as
proofs checking.
Searching (sophisticated searching as an alternative to
deep knowledge based reasoning)
Design of artiﬁcial systems, especially artiﬁcial
intelligence and life systems, as a way to understand
natural and nature-made systems.
Development of methods to design, analyse and verify
complex (information processing) systems.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 15/126
BASIC FEATURES of INFORMATICS-DRIVEN METHODOLOGY BRIEFLY
- III.
Design of algorithms, study of their performances and study of the inherent
complexities of computational, communication and description systems, as a way to
get a deep understanding of various phenomena and their interrelations.
Design, analysis and comparison of descriptional languages and systems and of the
relations between objects and their speciﬁcations.
Study of the real world through the study of all (also virtual) information processing
worlds.
Development of tools to mechanized research results creation and presentation.
Development of platforms for worldwide cooperation of research and development
communities.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 16/126
FEATURES of INFORMATICS-DRIVEN METHODOLOGY - MORE
DETAILS - I.
Modelling: - concepts, theory, tools and methodologies for speciﬁcation, design,
veriﬁcation and analysis of information processing models, especially of
very and ultra complex human-made and nature-created systems and
processes.
Simulation: - theories and methods of design, validation and veriﬁcation of
simulations, as well as of the display of their outcomes using imaging,
visualisation and animation tools.
Visualisation: - and animation theories, methodologies and tools.
Virtualization: - formalization, digitalization, (multilayer) generalization, (structural)
composition/decomposition, reduction as well as approximation and
other abstraction-driven methodologies and tools the importance of
which has been veriﬁed in the development of mathematics;
Design of AI systems: - The design of (productive, clever, cooperative, emotionally
intelligent and trustworthy) robots and other intelligence intensive
systems;
Design of artiﬁcial human limbs, organs and bodies; that match or outperform those of
human bodies.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 17/126
FEATURES of INFORMATICS-DRIVEN METHODOLOGY - MORE
DETAILS - II.
Data, information and knowledge mining: An application of data mining, pattern
matching, information retrieval, knowledge discovery and hypothesis
formation as well as of learning systems to huge sets or streams of data
provided by sensors or obtained due to the digitalization processes.
Automatization of reasoning: The design of systems for (automated) problem solving,
reasoning, theories creating, proof checking and theorem proving and of
other systems to deal with the tasks that used to belong to the human
domain only;
Design techniques: The development of methods to specify, design, analyse, verify,
modify and maintain very complex, parallel and distributed (information
processing) systems.
Algorithm design and analysis techniques: The development of methods to design
algorithms and protocols, to analyse their performance and to explore the
inherent complexity of computational, communication and description
problems, as well as to study complexity classes and their mutual
relations - as a way to get a deeper understanding of various phenomena
concerning eﬃciency and of their interrelations.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 18/126
POWER of NEW METHODOLOGY - I.
It brings new dimension to both old methodologies;
It brings into new heights an enormous power of
modeling and simulations;
It utilises an enormous power of visualisation;
It utilizes an enormous potential that the study of
virtual worlds brings for understanding of the real world;
It utilises an enormous power of (sophisticated) search
techniques.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 19/126
POWER of NEW METHODOLOGY II
It utilises the observation that designs of information
processing models (robots) bring deep understanding of
the real life phenomena;
New, informatics-driven, methodology, allows us also to
change the centuries old vision of the science.
Namely, the vision that science is to achieve its goals
mainly by discovering, isolating and studying very
primitive phenomena and processes.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 20/126
POWER of NEW METHODOLOGY - III.
New informatics-based methodology develops not only
tools to exploit better the existing knowledge, but also
contributes to the development of new tools to discover
new knowledge.
New methodology is used, as a very powerful and
inspiring one, also in all areas of scholarship, learning
and art.
Power of this new methodology is so large also for such
areas of society as politics and justice that one can
expect quite soon materialisation of the famous
Leibniz’s vision of an ending of future legal disputes :
”Gentlemen, let us calculate”.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 21/126
POWER of NEW METHODOLOGY - IV.
New methodology starts to make hard some (most) of
the soft-sciences.
New methodology provides intellectual frameworks and
tools to consider investigation also of complex and
large systems, in their full complexity.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 22/126
REDUCTIONISM versus HOLISM - I.
Reductionists view the entire universe, from its beginning
in time and from particles (or Planck scale) to galaxies, as
being governed by simple rules that are comprehensible by
human mind.
Design of microscopes and telescopes, that allowed to see
and explore microcosmos and macrocosmos, and their
enormously increased performances, that were behind of
many discoveries, much supported the reductionists view
of science.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 23/126
REDUCTIONISM versus HOLISM - II.
Reductionism lead to the view that physics is the only
fundamental natural science, chemistry is applied physics,
life is created by complex chemical reactions and various
particular steps in the biological evolution, as speciesation
and emergence of humanity, are mainly due to various
random events and historical circumstances.
Non-reductionists position is to a large extend based on
the possibility of computers to model interactions of huge
number of simple elements and to build computer models
so complex that they are not understandable by human
mind and that this brings very new tools for science to ask
and to answer new questions.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 24/126
CASE STUDY I -MODELLING and SIMULATION
CASE STUDY I
-MODELLING and SIMULATION
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 25/126
DEVELOPMENT of GOALS of SCIENCE - DRIVING
METHODOLOGIES - I.
Classical Greek Period - methodology was driven by
philosophy. The starting and basic assumption was that
phenomena of nature are not under the control of
Gods, and that human mind is powerful enough to
discover basic qualitative axioms (truths) and
deduction rules. The goal was to understand CAUSES
OF PHENOMENA of nature and to ﬁnd out WHY
THINGS HAPPEN.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 26/126
DEVELOPMENT of GOALS of SCIENCE - DRIVING
METHODOLOGIES - II.
Galileo time - methodology was driven by mathematics and by a belief that nature
should be the source and veriﬁer of our basic and derived knowledge.The starting
and basic assumption was that God created mathematically expressible world and let
it to run according to mathematically expressible rules. The goal of science was to
discover that rules (and by that to demonstrate geniality of the God).
Understanding developed that it is not absolutely necessary to know the causes of
phenomena, but that is to a large extent suﬃcient to know explicitly important
RELATIONS among some quantitative characteristics OF PHENOMENA. They can
be suﬃcient to make useful and important predictions concerning the behaviour of
the phenomena of physical nature and to understand HOW THINGS HAPPEN.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 27/126
VIEWS of GALILEO
Galileo: ”It does not seem expedient to me to
investigate what may be the cause of acceleration; the
chief concern must be to explore the law according to
which acceleration takes place.
But hitherto I have not been able to discover the cause
of those properties of gravity from phenomena and I
frame no hypothesis ...... To us it is enough that
gravity does really exists, and act according to the laws
which we have explained, and abundantly serves to
account for all the motions of the celestial bodies, and
of our see.”
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 28/126
DEVELOPMENT of GOALS of SCIENCE - DRIVING
METHODOLOGIES - III.
Post-computer era - methodology is driven by
informatics . The starting and main assumption is that
we often do not need to know neither causes of
phenomena nor explicitly relations between their
important quantitative characteristics, it is suﬃcient to
design an (evolving - capable to learn) oraculum, an
information processing MODEL OF PHENOMENA,
that can be used to answer, or even visually
demonstrate, suﬃciently well, important questions
about the phenomena.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 29/126
WISDOMS
Theories (Models) are lies that tells you true.
The art is a lie that helps us to see truth.
Pablo Picasso
An important question is: how complex can be simple
systems and how simple can be complex systems?
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 30/126
CASE STUDY - I. MODELING and SIMULATION
CASE STUDY - I.
MODELING and SIMULATION
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 31/126
MODELS
Models are always idealisation, approximation, guesses
because our knowledge of nature is always incomplete and
approximate at the best.
For models of phenomena of nature we have always to ask
how much are they based on observation and measurement
of accessible phenomena; how much are they based on
informed judgement and how much on convenience?
Models are most useful when they are used to challenge
existing formulations, rather than to validate or verify
them. Models always capture only some essences of the
phenomena they model - one should not assume that they
could capture the whole phenomena.‘
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 32/126
MODELLING and SIMULATION - I.
Modeling and simulations are key methods in such
disciplines as earth-sciences, environmental sciences,
(system) biology, astronomy, economics, social sciences
where one needs an understanding of complex
phenomena produced by interactions of various
processes and/or neighbouring elements.
Using simulation one can follow processes that are
otherwise invisible because of being too small, or too
slow, or too large, or too fast, or too dangerous.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 33/126
MODELLING and SIMULATION - II.
Simulations and modeling provide a completely new
view of reality that is the closest to reality that we can
have.
More complex modelled systems are and more
modiﬁable they are, for example by changing (or even
reversing) the ﬂow of time, or by zooming, or changing
the ﬂow and amounts of various resources, better
understanding of the reality can be obtain through
them.
In general modeling and simulations allow in very
eﬀective way to use virtual worlds to get deep insights
into the real world.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 34/126
MODELLING and SIMULATION - III.
Some complex phenomena of nature, society or of
people cannot be dealt with using experimental
methods due to the practical or even ethical
considerations. Modeling and simulations are then the
main available methodology to study them.
Modeling and simulation of the human brain is very
challenging tasks. It is expected to bring huge beneﬁts
for medicine (to treat brain diseases and disorders via
drugs and implants, to deal with memory, hearing and
vision problems,... ) and also for informatics (to inspire
the design of computers with novel types of parallelism,
connectionism and distributivness as well as of the AI
systems of novel types).
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 35/126
A BIT of HISTORY - I.
The ﬁrst large scale and inﬂuential computer simulation
was done in 1953 by E. Fermi, J. Pasta and S. Ulam in
Los Angelos laboratory - to understand behaviour of
large non-linear systems and their supposed tendency to
decay to states of ever greater disorder.
One of the basic questions concerning
simulation/modelling is for which natural phenomena
and processes we can do simulation/modelling by
systems that are signiﬁcantly simpler.
A variety of interesting results have been obtained
concerning classical simulation of certain classes of
quantum phenomena, especially circuits.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 36/126
A BIT of HISTORY - II.
The Blue Brain project of ´Ecole Polytechnic in
Laussane, which started in 2005, aims at the simulation
of the entire human brain down to the molecular level.
One of the most powerful current computer system,
Roadrunner, with a theoretical (demonstrated)
performance 1.7 (1.1) petaﬂops and occupied space
260 m2
, has been developed by the IBM for Los Alamos
National Laboratory to model the decay of US nuclear
arsenal.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 37/126
SIMULATION and MODELLING of CELLS
Cells can be seen as well-organized autonomous systems of many discrete interacting
components and biology accumulated huge amounts of knowledge about their basic
components.
This is especially true for the main components/macromolecules of cells: nucleic
acids polymers - DNA and RNA - proteins and membranes.
However, all that provides very little insights into how cells work as a whole and how
they process information.
What is therefore needed is to understand cells and their main components, and also
other biological elements, as systems of interacting components that abstract from
their chemistry.
To do that through continuous mathematical models would require to simulate huge
amounts of diﬀerential equations and that is unfeasible.
A way out seems to be to create automata models of cell behaviour in the form of
several discrete, concurrent, asynchronous and heterogeneous models of interacting
elements.
The interaction models of the above type are some of the most diﬃcult for
Informatics to handle and analyse, and so deep results of the concurrency theory and
of other areas of scientiﬁc Informatics need to be used.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 38/126
BRAIN MODELING
In US, during period 1991-2004, they run big project
”Human brain project” oriented on simulation of the
brain.
In Europe, in 2013, European commission launched 1,2
milliard EUR project entitled ”Human Brain Project”
oriented on brain simulation, see Chapter 10, with
following goals: to gain fundamental insides into what
it means to be human; to develop new treatments for
brain diseases and to develop revolutionary new ICT see
Chapter 9.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 39/126
EMERGENCE of NEW SIMULATION METHODOLOGY - I.
An understanding that modeling can be seen as a key
element of new methodology goes actually back also to
von Neumann who said:
The sciences do not try to explain, they hardly try to
interpret, they mainly make models. By a model is
meant a mathematical construct which, with the
addition of certain verbal interpretations, describes
observed phenomena. The justiﬁcation of such a
mathematical construct is solely and precisely that is
expected to work.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 40/126
EMERGENCE of NEW SIMULATION METHODOLOGY - II.
The above vision can nowadays be better formulated by
the following ”improvement” and ”modernisation” of von
Neumann thought.
The sciences do not try to explain, they hardly try to
interpret, they mainly make models. By a model is
meant an informatics system which, with the addition
of certain verbal interpretations, describes observed
phenomena. The justiﬁcation of such models/systems
is solely and precisely that is expected to work.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 41/126
MODELS and REALITY
Simulations and modeling provide a completely new view
of reality that is often closest to reality that we can have.
More complex such models are and more modiﬁable such
simulations are, for example by changing (or even
reversing) the ﬂow of time, or by zooming, or changing the
ﬂow and amounts of various resources, better
understanding of the reality can be obtain through them.
In general modeling and simulations allow in a very
eﬀective way to use virtual worlds to get deep insights into
the real world.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 42/126
USEFULNESS of HUGE MODELS
Through models we can create systems that can have
enormous predictive and explanatory value in spite of the
fact they are behind human potential to understand them
fully and globally.
We can however, using informatics tools that enhance our
intellectual capabilities, to understand them locally and to
make them to give us answers to important inquires
concerning phenomena they model.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 43/126
SUCCESS STORIES of MODELLING
Computer modeling and simulation of big molecules
and their dynamics is one of the big success stories of
computer modeling and simulation with big impacts on
design of useful molecules and drugs. Several factors
are behind. Powerful (parallel) computers, good sets of
test data and deep knowledge and expertise available.
All that open new windows to see the world of
molecules and gave rise also to new ﬁelds such as
protein dynamics.
One of the big goal of modeling is to understand how
biological systems work. For example cells. Biological
systems can be seen as well-organized autonomous
systems of many discrete interacting components.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 44/126
FUNDAMENTAL QUESTIONS CONCERNING MODELLING
Which processes can be simulated suﬃciently well by
systems that are (much) simpler than systems to be
simulated?
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 45/126
EXAMPLES of MODELLING and SIMULATIONS
Simulations of battles, impacts of natural or men-made
disasters, earth and atmosphere processes and so long
require the largest computer power available;
Simulations for entertainment industries, especially
motion movies, computer and video games, belong to
the most interesting, stimulating and challenging ones.
Improvement in the area of computer technology, but
also in the design of algorithms and software systems
open usually new domains where modeling and
simulations are feasible.
Technically, simulations can be deterministic or
randomized, steady-state or dynamic, discrete or
continuous.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 46/126
CASE STUDY II - VISUALISATION
CASE STUDY II - VISUALISATION
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 47/126
WISDOMS
A picture is worth of thousand words.
Anonymous
Of all our inventions for mass communications, pictures
still speak the most universally understood language.
Walt Disney
Pictures and shapes are but secondary objects and
please or displease only in the memory.
Francis Bacon
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 48/126
ESSENCE and GOALS of VISUALISATION
Visualisation is science, technology and art to use graphic
to represent and display data, information and knowledge
via images - graphic is here a communication medium.
Rendering is the process of generating an image (of two,
three or more dimensional objects or processes) from their
high-level descriptions in a strictly deﬁned formal language
using computer programs.
A high level description/representation of an image uses
various (of a lower level) primitive elements. In a
schematic drawing, they may be line segments, curves; in a
3D rendering they may be triangles and polygons in space
and in a graphical user interface they may be windows and
buttons. Descriptions should contain geometry viewpoint,
textures, lighting and shading information.prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 49/126
THREE GOALS of VISUALISATION
On one side visual representations are to take the
advantage of the human eye’s broad bandwidth into the
mind to allow users to see, explore and understand large
amounts of information and complex processes at once.
On the second side, visualisation helps us to see those
parts of our cosmos and microworld that are invisible by
our unaided eyes.
On the third side, visualisation can help us to get new
understanding of phenomena not only of the real world,
but also of the world of formal science, mathematics and
information processing worlds and to develop in these areas
new knowledge, hypotheses and theories discovery tools.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 50/126
MANDELBROT SET - I.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 51/126
MANDELBROT SET - II.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 52/126
MANDELBROT SET GENERATION
Mandelbrot set is a set of values of c in a complex plane
for which the orbit of 0 under the iteration of complex
quadratic polynomial
zn+1 < − − z2
n + c
remains bounded.
That is a complex number c is a part of the Mandelbrot
set if, when starting with z0 = 0 and applying the iteration
repeatedly, the absolute value of zn remains bounded
however larger n is.
Treating real and imaginary parts of complex numbers as
coordinates pixels of points are colored depending on how
fast sequence created by iteration converges.prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 53/126
MANDELBROT
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 54/126
HISTORY of VISUALISATION
Cave paintings can be see as ﬁrst attempts for
visualisation.
Geographical maps of the world were very important
products of visualisation (since the third century BC).
William Playfair (1786) is usually mentioned as one
deﬁning various types of diagrams to visualise data
(line graphs, bar charts, pie charts,...).
In 1815 a geological map of England was published by
William Smith - a map that was claimed to change the
world (of visualisation).
Visualisation of fractal and elements of nonlinear
phenomena, especially attractors brought again a new
dimension to visualisation.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 55/126
JOHN SNOW’s MAP of 1984 CHOLERA OUTBREAK in SOHO
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 56/126
SMITH’s GEOLOGICAL MAP of GREAT BRITAIN
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 57/126
PLAYFAIR’s VISUALISATION
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 58/126
ANOTHER VIEWS of VISUALISATION
Visualisation can also be seen as a way of utilising
methods derived from the study of human perception,
graphical design, art and usability analysis.
Understanding of the human perception and of the
potential of imaging technology are the key extreme
factors in the development of visualisation principles,
forms, methods and tools and also in using visualisation.
Visualisation is of importance also because we are visual
beings who use sight as one of our key senses for data and
information understanding and knowledge discovery.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 59/126
A MORE TECHNICAL VIEW of VISUALISATION
In a more technical way, one can say that the goal of
visualisation systems is to transfer logical description of
complex information (logical elements and their relations
as well as operations for their manipulations), by encoding
their elements and their relations through perceptual
elements and their relations.
The encoding has to be done in such a way that
good/better understanding of complex information can be
visually obtained - one can therefore transform logical
descriptions of complex information to perceptual
elements, procedures and their accompanying graphics.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 60/126
VISUALISATION as a TOOL - I.
Visualisation is nowadays one of the key tools to bring
new quality into the learning and knowledge discovery
process in practically all areas of human and societal
activities.
An original idea was to make static visualisations. New
methods and technology allow to create dynamic and
interactive visualisations and also visualisation displays
in such a form that they can be well processed and
understood not only by humans, but also by machines computers,
robots and so on.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 61/126
VISUALISATION as a TOOL - II.
While early visualisations were static objects, printed on
paper or other ﬁxed medium, modern visualisations are
very dynamic processes, with the user controlling
virtually all stages of the procedure, from data selection
and mapping control to color manipulation and view
reﬁnement.
While most of the visualisations are two dimensional,
they often try to depict more-dimensional objects and
not only the four-dimensional ones where time is the
fourth dimension, but even more dimensional. 3D
printers bring again a new dimension into the attempts
to depict three dimensional objects and their relations.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 62/126
VISUALISATION versus COMPUTER GRAPHIC
Computer graphics and visualisation have diﬀerent goals though visualisation uses
graphics much.
Visualisation is the application of graphics to display data by mapping data to graphical
primitives (points, lines, areas and volumes) and rendering the display.
Computer graphic is predominately focused on creation of the interactive synthetic
images and animations of three-dimensional objects most often where visual realism is
one of the primary goals.
Visualisation does not emphasize visual realism as much as eﬀective communication of
information.
Moreover, many type of visualisation do not deal with physical objects and those that do
are often communicating attributes of the objects that are not normally visible - such as
material stress.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 63/126
TYPES of VISUALISATION
There is a variety of important types of visualisation.
Scientiﬁc (data) visualization
Many-dimensional objects visualization
Flow visualizations
Geo-visualization
Information visualization
Software visualization
Music visualizations
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 64/126
WHY IS VISUALISATION of SCIENTIFIC DATA of IMPORTANCE
Main reasons why such scientiﬁc simulations are of large importance are the following
ones:
Visualisations usually compress a lot of data into a
single image where spatial distribution of data and
coloring could much speed up comprehension of data
and their analysis;
Visualisations create images that allow to reveal easily
correlations between diﬀerent quantities, both in space
and time;
Visualisations allow to see data selectively and
interactively - all in real time;
Visualisations can furnish new space-like structures and
by an observation of their creation and changes in time
one can get important insights into their dynamics;prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 65/126
ATTRACTOR
An attractor is a set toward which a variable, moving according to a dictates of a
dynamical system , evolves over time.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 66/126
SCIENTIFIC DATA VISUALISATIONS APPLICATIONS
Visualisation is of large importance and can even be the
key tool in huge amount of applications. It is even possible
for an application to be totally driven by its visualisation.
The main application areas of visualisation can be seen as
follows:
In the natural sciences (physics (especially astronomy, cosmology,...): biology (cell
and molecular biology);...)
In the earth and environmental sciences.
In formal sciences;
In applied sciences;
In medicine - medical reconstructions for diagnoses and at surgeries
In health care, transport, communication, economics,..
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 67/126
CURRENT VISUALISATION TOOLS
Currently there are in widespread use several software
tools that allow to exhibit complex three-dimensional
data sets, graphs of very sophisticated functions and to
use graphics in powerful new ways to display data.
Examples of such tools are Geometer’s sketchpad,
Mathematica, Maple, Matlab.
Such tools allow to see things more clearly, in more
details and in a new way.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 68/126
SLIP CASE
Automobile company Volve used to work with clay
models to design car bodies and used to be a long
process.
In the early 1980s, company created their team of
experts to ”computerize” the process, but they failed.
More successful was the team headed by brilliant
mathematician Bjorn Dahlberg, holder of prestigious
Salem Prize in harmonic analysis.
Dahlberg used sophisticated techniques from
diﬀerential equations, diﬀerential geometry, linear
programming, convex surface theory, harmonic analysis
and other parts of mathematics to design software SLIP
that revolutionized car surface design process.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 69/126
DE-VISUALISATION MOVEMENTS - I.
In the Golden era of Greek mathematics visualisation of geometrical objects played
an important role.
An introduction of analytical geometry around 1640, that initiated exploration of
many dimensional objects, changed view on importance of visualisation.
For long time visualisation did not have large importance because visualisation tools
were primitive.
There was also a sort of antivisualisation movement at the beginning of 20th
century, represented especially well by an attempt of so called Bourbaki movement
in France (after 1930), to make consequently picture-less presentation of all
fundamental mathematics.
It was only (namely) due to advances in computer and printer technologies that
visualisation started to play a very important role again.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 70/126
CASE STUDY III - ALGORITMISATION AND COMPLEXITY
CONSIDERATIONS - I.
1. Finding a new data structure or an algorithm can
revolutionize the way scientists think about a problem and
can even create a research area. Some examples:
Strassen’s exponentially faster matrix multiplication
algorithm (1969).
Discovery of NP-complete problems by Cook (1971).
Freivalds’ matrix multiplication testing randomized
algorithm (1979);
Shor’s quantum factorization algorithm (1994).
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 71/126
CASE STUDY III - ALGORITMISATION AND COMPLEXITY
CONSIDERATIONS - II.
2. Study of inherent complexity (computational,
communication and descriptional) of phenomena and
especially feasibility issues is an important methodology to
inﬂuence and guide research directions.
Complexity considerations played the key role especially in the following two areas:
Quantum information processing - it was due to complexity outcomes that it got
clear that this area may have big potential. The complexity theory keeps having
deep impacts on the whole development in quantum information processing and
communication. One can even say that one of the goals of the quantum complexity
theory is to challenge our basic intuition how the physical world behaves.
Security - in a broad sense - computational complexity consideration plays key role
in modern secret key and also in public-key cryptography and in all other areas of
security. , secrecy, anonymity, privacy and trust.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 72/126
WHY von NEUMANN DID NOT DISCOVER QUANTUM
COMPUTING
von Neumann is one of the fathers of both quantum
physics and modern computers. It is therefor natural to
ask why he did not come with the idea to develop
quantum computers.
Very likely it is because:
No complexity theory was known (and needed)
The concept of randomized algorithms was not known.
No public key cryptography was known (and needed).
Progress in physics and technology was far behind what
would be needed to make even rudimentary
implementations.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 73/126
ALGORITHMS GENERATING INDUSTRIES
Google’s 35 billion-euro business model largely rests on
algorithms such as Page ranking - a ﬁx-point algorithm
that made WEB searches practical.
The music industry has been revolutionized by
standards such as MP3 and its deﬁning algorithms and
data structures.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 74/126
FAMOUS ALGORITHMS - I.
Binary search
Dynamic programming
Euclid algorithm
Fast Fourier transform
Gauss elimination algorithm
Finite element methods
Monte Carlo algorithms
Newton method
QR-algorithm to compute eigenvalues
Random walk algorithms
Runge-Kuta method
Simplex method for linear programming
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 75/126
FAMOUS ALGORITHMS - II.
Dijkstra’s short path algorithm
Krylov subspace iteration method
Metropolis algorithm
Page ranking algorithm
Quicksort (T. Hoare, 1962)
RSA encryption and signature
Shor factorization algorithm
Viterbi algorithm
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 76/126
POWER of COMPLEXITY THEORY as a METHODOLOGY - I.
Extraordinary power of methods and outcomes of the computational complexity
theory, as of a tool for advances of science, has been especialy well demonstrated in
the development of quantum information processing and communication.
It was mainly due to the outcomes of the quantum complexity theory that an
understanding has emerged that quantum computers could pay oﬀ. Physics had at
that time no tools to see that quantum computers could pay of.
The complexity theory keeps having deep impacts on the whole development of the
area of quantum information processing and communication including quantum
cryptography.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 77/126
POWER of COMPLEXITY THEORY as a METHODOLOGY - II.
One can even say that one of the goals of the quantum complexity theory is to
challenge our basic intuition how the physical world behaves and to understand two
of the great mysteries of the 20th century: what is the nature of quantum
mechanics and what are the limits of computation.
The complexity theory approaches can also lead us to ask better questions about the
quantum nature – nontrivial, but answerable questions – questions that put old
quantum mysteries in a new light. Quantum computational complexity also allows
us to demonstrate that some physical phenomena are not possible - by showing that
possibility of these phenomena would allow us to solve eﬃciently complete problems
for some computational complexity classes that are believed to be larger than the
classes P or BPP or BQP.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 78/126
CLASSIFICATION of IMPOSSIBLE - COMPLEXITY THEORY
APPROACH - I.
Some of the ways to show that some quantum event or phenomenon E is impossible:
To show that E would imply superluminal
communication.
To show that E would violate NO-cloning theorem.
To show that E would imply that problems from some
class (likely) larger than P would be solvable in
polynomial time
(and that also allows to classify impossible tasks).
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 79/126
CLASSIFICATION of IMPOSSIBLE - EXAMPLES
Abrams and Llyod (1998) showed that under the
assumption that quantum mechanics is non-linear,
more exactly that Weinberg’s model of quantum
mechanics is valid, one can solve in polynomial time
NP-complete problems.
Aaronson (2004) has shown that if arbitrary one-qubit
nonlinear gates can be implemented without an error,
then PSPACE-complete problems can be solved in
polynomial time.
Aaronson has also shown that if so-called post-selection
is allowed, then PP-complete problems can be solved in
polynomial time.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 80/126
THE ROLE of QUANTUM COMPLEXITY THEORY
One of the goals of quantum complexity theory is to challenge our basic intuition
how physical world behaves.
Quantum complexity theory is of great interest because one of its goals is to
understand two of great mysteries of 20th century: what is nature of quantum
mechanics and what are the limits of computation.
It would be astonishing if a merge of such important areas would not shed light on
both of them and would not bring new great discoveries.
Taking complexity theory perspective can lead us to ask better questions about
quantum nature – nontrivial, but answerable questions, which put old quantum
mysteries in a new light even if they fall short of answering them.
One way quantum complexity theory obtains insights into the quantum world is
through the study of main quantum complexity classes BQP, QMA and their
complete problems.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 81/126
CASE STUDY IV - PROOFS and AUTOMATED REASONING
PROOFS
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 82/126
WHAT IS A PROOF?
The concept of proof is one of the most basic ones in modern science.
Any discovery and development of a broader view of this concept, as well as of tools to
make or verify proofs, can therefore have far-reaching impacts on science.
Some citations:
A nice proof makes us richer (Jurij Manin).
A proof is whatever convinces me (S. Even)
The glory attached to the creativity involved in ﬁnding proofs, makes us to forget
that it is much less gloriﬁed procedure of veriﬁcation which gives proofs their value.
(O. Goldreich)
Proofs depend much on the audience. We prove things in a social context and
address them to a certain audience. W. P. Thurston
Proof is lingua franca of mathematics.
Proof is a rhetoric device for convincing someone else that a mathematical
statement is true.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 83/126
WISDOMS
There are proofs that date back to Greeks that are still
valid today.
Andrew Willes
In a sense, mathematicians have been most advanced
by those who distinguish themselves by intuition rather
than by rigorous proofs.
Felix Klein
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 84/126
PROOFS and THEIR DEVELOPMENTS - I.
Introduction of the concept of the proof, and deductive
mathematics, is often considered as the main
contribution and feature of Greek mathematics from its
Classical period, especially due to Euclid’s Elements.
Euclid was the ﬁrst who systematically used precise
deﬁnitions, axioms and strict rules of logic and who
systematically proved every statement.
This idea was already almost completely abandon
during Alexandrian period of Greek mathematics.
Actually for almost 2000 years achievements of the
classical Greek period, concerning methodology of
mathematics, were virtually ignored, as not much
useful.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 85/126
PROOFS and THEIR DEVELOPMENTS - II.
Cicero said: The Greeks held the geometer in the
highest honor; accordingly, nothing made more brilliant
progress among them than mathematics. but we have
established as the limit of this art its usefulness in
measuring and counting.
The Greek virtue of insisting on exact concepts and
proofs can now be sen as a defect so far as creative
mathematics was concerned.
At the end of 17th century mathematicians had
virtually dropped the idea of clearly deﬁned concepts
and deductive proofs. Mathematics was so inspired by
developments of science and vice verse that a fusion of
mathematics and vast areas of science was detectable
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 86/126
PROOFS and THEIR DEVELOPMENTS - III.
In the 18th century mathematics and physics virtually
merged, and the physical meaning of the mathematics
guided the mathematical steps and often supplied
partial arguments to ﬁll in non-mathematical steps.
The concept of a proof in mathematics, as of a device
to communicate truth of some assertion, can be seen
as an equivalent of the concept of reproducible
experiment in physics and chemistry.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 87/126
PROOFS and THEIR DEVELOPMENTS - IV.
The above period of mathematics, in which
mathematicians did not care about foundations of their
work is sometimes called heroic age of mathematics.
Some views of that time:
Such subtleties as the Greeks worried about we no
longer need.
Why to go to the trouble of proving by complicated
reasoning things which one never doubts in the ﬁrst
place, or of demonstrating what is more evident by
means of what is less evident.
On a more philosophical basis, mathematicians,
believed that they are unearthing the mathematical
design of universe and therefore they were conﬁdent in
the truth of their outcomes.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 88/126
PROOFS and THEIR DEVELOPMENTS - V.
Descartes, one of founders of modern science, believed
that axioms of mathematics are true and mathematical
reasoning is sound on the conviction that God would
not deceive us, so that to deny the truth and clarity of
mathematics would be to deny God.
Actually from 200 B.C. till 1870 almost all mathematics
rested on an empirical and pragmatic basis.
At the end of 17th century mathematicians had
virtually dropped the idea of clearly deﬁned concepts
and deductive proofs.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 89/126
PROOFS and THEIR DEVELOPMENTS - VI.
At the end of 17th century mathematics was so inspired
by the developments of science and vice verse that a
fusion of mathematics and vast areas of science was
detectable and mathematics started to rely more and
more on scientiﬁc results to justify its own procedures.
In the 18th century mathematics and physics virtually
merged, and the physical meaning of the mathematics
guided the mathematical steps and often supplied
partial arguments to ﬁll in non-mathematical steps.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 90/126
PROOFS and THEIR DEVELOPMENTS - VII.
By 1900 the goal of establishing mathematics
rigorously was formulated by Hilbert. The rigorization
was (believed to be) achieved by axiomatising various
branches of mathematics.
At the end of the 19th century a variety of strange
functions have appeared as well as paradoxes in set
theory and it got clear that a level of rigor in
deﬁnitions, theorems and proofs has to be increased
At the beginning of the second half of 20th century it
has been discovered that Hilbert’s notion of proofs is
too strong - some simple stated theorems could have
proofs only longer than number of particles in universe.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 91/126
PROOFS and THEIR DEVELOPMENTS - VIII.
The existence of culture of theorems and proofs can be
seen as rigorous and well-tested standard for formulation
and recording ideas and discoveries that have as a
consequence the fact that mathematical ideas and
discoveries stood up under the test of time.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 92/126
MATHEMATICS VERSUS PHYSICS from PROOFS POINT of
VIEW
In one of the recent papers: J.Borwein et all (1995):
Experimental mathematics: A discussion, the
preoccupation of mathematics with proofs is questioned:
Mathematics is seen as consisting of two parts
theoretical mathematics - speculative as theoretic
physics
rigorous mathematics - giving evidence (using proofs)
as experimental physics does.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 93/126
VIEWS of ZEILBERGER - I.
Computers have already started doing to Mathematics what the telescopes/microscopes
did to astronomy/biology.
In the future not all mathematicians will care about absolute certainty, since there will be
so many exciting new facts to be discovered: mathematical pulsars and quasars that will
make Mandelbrot set to look like a Galilean moon.
We will have (both human and machine) professional theoretical mathematicians who will
develop computational paradigms to make sense out of the empirical data and who will
keep Fields medal along with (both human and machine) experimental mathematicians.
Will there still be a place for mathematical mathematicians?
Dorov Zeilberger
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 94/126
HILBERT’s CONCEPT of PROOFS
The currently dominating view of the proof is due
to Hilbert:
A proof in a formal system F is a sequence of
statements such that each of them is either
an axiom of F;
or it can be derived from previous statements of
the sequence using one of the ﬁnitely many
deduction rules of F
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 95/126
DIFFICULTIES WITH the HILBERT’s CONCEPT of PROOF
G¨odel Incompleteness result. For any suﬃciently
powerful formal systems there are correct statements
the truth of which cannot be proven in that system.
Chaitin Incompleteness result: In any proof systems
one can show randomness only a ﬁnitely many random
strings.
Computational complexity result There are simple
Boolean formulas each proof of which has to be longer
than the number of particles in universe.
Proof puzzle What is more diﬃcult
to ﬁnd a proof or to verify a proof
This is a problem equivalent to the P=NP problem.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 96/126
VERY LONG PROOFS - I.
1799 Ruﬃni published a more than 500 pages proof of ”Abel-Ruﬃni theorem”
- in 1824 N. Henrik published another 6 pages proof.
1974 Thomson published more than 700 pages classiﬁcation of ”N-groups”
1974 Deligne published more than 700 pages proof of ”Ramanuyan and Weil
conjecture”
1974 Appel and Haken published 741 pages proof of ”4-colour theorem” with
strong computer support.
1980 Almgren published 1728 pages proof of ...
1983 Gorenstein, Lyon and Aschbacher published 890 pages proof of
”Tichotomy theorem”
1983 Hejbal published a 1322 pages proof of ”General Selberg trace formula”.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 97/126
VERY LONG PROOFS - II.
2000 Almgren published 955 pages proof of ”Regularity theorem”.
2004 Aschbacher and Smith published 1221 pages classiﬁcation of
”Quasi-thing groups”
2004 Classiﬁcation of ﬁnite simple groups has 10,000 to 20,000 pages
As a very long proof has been considered
in 1900 a proof having 100 pages;
in 1950 a proof having 200 pages;
in 2000 a proof having 500 pages.
In many cases traditional proofs may be set aside in favour of experimentation by
testing of thousands or millions of examples by computers.
There are attempts to make a proof in a distributed way using thousands of provers
and it is expected that that can take even 20 years.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 98/126
VIEWS of ZEILBERGER - II.
I can envision an abstract of a paper (around 2100) that
reads, ”We show in a certain precise sense that ..... is true
with probability larger than 0.99999 and that its complete
truth could be determined with a budget of $ 10 billions.”
As absolute truth becomes more and more expensive, we
could sooner or later come to accept the fact that only
few non-trivial results could be known with old-fashioned
certainty.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 99/126
PROBABILISTIC PROOFS
Three new types of proofs have played a crucial role in
theoretical informatics in the last 15 years:
Interactive and non-interactive (one- and many-prover)
proof (systems)
Zero-knowledge proof systems.
Probabilistic (holographic) proof (systems).
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 100/126
PROBABILISTIC PROOF SYSTEMS
The concept of probabilistic checkeable proofs (PCP), or
transparent or holographic proofs, is another
great/shocking idea concerning proofs.
Informally, PCP proofs are proofs that are written down in
such a way that one needs to look only to (very) few
randomly chosen bits of it in order to ﬁnd out whether the
proof is correct with (very) high probability.
The hard task is, however, to encode a given proof in such
a way that randomized checking is possible.
Famous PCP-Theorem says that every NP-complete
problem/language admits a probabilistically checkeable
polynomially long proof.prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 101/126
PCP THEOREM
Intuitively, the PCP-theorem says that for some ﬁxed (and
universal) constant k, for every n, any mathematical proof
of length n can be rewritten as a (diﬀerent) proof of length
poly(n) that is formally veriﬁable on 99% by a randomized
algorithm that makes only k queries to the proof.
One can also prove that each proof can be rewritten in
such a way that it is enough to check 11 randomly chosen
bit in order to verify the proof with probability at least 1
2.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 102/126
AUTOMATED and SEMI-AUTOMATED PROOF SYSTEMS and
PROOFS CHECKERS - I.
A view of proofs as ”whatever that convinces me” has
started to be recently again pursueded.
The development of proof assistance systems and proof
checkers has started already in 1966.
Proof checkers are getting faster and faster more
powerful to such an extend that they have a chance
signiﬁcantly increase proving power of human.
Proof checkers started to proof theorems beyond the
proving power of mathematicians at that time.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 103/126
AUTOMATED and SEMI-AUTOMATED PROOF SYSTEMS and
PROOFS CHECKERS - II.
First famous result that created a lot controversy was computer assisted proof (741
pages) of the four colour theorem in 1976.
Another famous result was the proof of Robbin’s conjecture in 1996 that had
resisted attempts for proofs for 60 years.
The outcomes of proof checkers started to indicate that the concept of creative
thinking may need to be challenged - proof checkers can take very diﬀerent path to
come to the same conclusions.
As a consequence it has been discovered that there is a very thin line between
mechanical and creative actions.
Some proofs are so complex that they can be designed and checked only with the
help of computers and proofs checkers.
It starts to be feasible the situation that most of the proofs could be done by proof
checkers to such an extend that the main role of mathematicians will be shifted to
hypothesis and theorems formulation.
As the result, mathematics research, as it is known today, as proof-centered, may
disappear to a large extend. Mathematicians may focus mainly on hypothesis and
theorem formation and proofs will be left to theorem provers.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 104/126
ROBBINS CONJECTURE
In the 1930s, Herbert Robins conjectured that 10 usual
simple axioms of Boolean algebra are equivalent to the
following three axioms
x ∪ (y ∪ z) = (x ∪ y) ∪ z
x ∪ y = y ∪ x
x ∪ y ∪ x ∪ ¯y = x
(Last axiom is called ”Robbins equation”).
The conjecture was shown to be true ﬁrst by William
McCune from the Argonne National Laboratory in 1996
using the prover EQP (Equational Theorem Prover).
A human readable proof was later produced by Allen L.
Mann in 2003.prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 105/126
PROOF CHECKERS
Some proof checkers or proof assistant, as Mizar, try to
imitate usual informal proofs and automate their most
technical parts.
Some other, as Metamath, work in a very diﬀerent way,
and can be used with every sort of formal systems Metamath
makes no assumption about the used logic it
is a substitution algorithm.
One of the goals at the design of proof checkers is to
proof as many, and as diﬃcul as possible, theorems there
are yearly competitions in that.
Another goal is to design as small as possible, but still
powerful, proof checkers.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 106/126
AUTOMATED THEOREM PROVERS
There is currently a variety of automated theorem
provers. Perhaps the most known are provers ”E” for
full ﬁrst order logic, Otter (that developed into Prover
9), Vampire, Waldmeister.
Most famous success (already in 1996) was the proof
(after 8 days of work) of the already mentioned
Robbins conjecture.
Since that time a variety of theorem has been proven in
(semi)groups, projective geometry and various logics.
Intel and other companies use automated theorem
provers regularly to verify correctness of their
implementation of various operations (as division).
Another applications of theorem provers are in software
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 107/126
PROOF ASSISTANT
Proof assistants allow to take a usual proof and to turn
it into the formal proof.
Coq - a proof assistant which can automatically extract
an executable program from speciﬁcations.
HOL Light - a proof assistant for classical ﬁrst order
logic.
There is nowadays a whole industry of the people who
use computers to search axiomatic systems for new true
statements and their proofs.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 108/126
FOUR-COLOR PROBLEM STORY
It is the problem to decide whether each only-countries map on the sphere can be
colored with 4 colors only.
The problem was formulated in 1852 and published in 1878.
In 1879 A. Kempe published a proof that 4 colors are enough - in 1890 proof was
found to be wrong.
Problem got famous, but only partial solution were found - for example that 4 colors
are enough for maps with at most 25 countries.
In 1974 K. Appel and W. Haken from University of Illinois claimed that they solved
positively 4-colors problem using 1200 hours of university supercomputer.
There is still controversy whether such a proof can be accepted because no human
can check it and several errors have been found (and always corrected) in the
program used.
In 1994 another computer assisted proof of four-color theorem has appeared and so
far no error was found in the program used.
In 2004 the 1994 proof was checked using a ”mathematical assistant”.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 109/126
FlysPecK PROJECT
FlysPecK project has as the goal to make formal proof (computer made with all
details formally veriﬁed) for Thomas Halles’ solution of Kepler’s conjecture.
The Kepler conjecture from 1611 asserts that the density of packing of congruent
spheres in 3D is never greater than π/
√
18.
Conjecture remained unsolved for almost 400 years until it was ”solved” in 1998 by
Halles using a lot of computer computations.
To verify Halles’ proof a group of 12 prominent mathematicians was established in
1999. After 4 years of work they declared that they are 99% sure that the proof is
correct.
In 2005 Halles started an initiative to make a complete formal version of his proof.
It is expected that to turn the usual Halles’ proof into a formal proof will require
about 20 years of work of scientists from all over the world and will cost at least 5
millions of dollars.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 110/126
KEPLER’s CONJECTURE
In 1961 Kepler formed his conjecture that no arrangement
of equally sized spheres ﬁlling space has a greater average
density (74%), than that of face-centered cubic packing or
face-centered cubic packing. (Random packing has density
65%.)
In 1831 Gauss showed that Kepler’s conjecture holds if
only regular packing arrangements are considered.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 111/126
OPTIMAL PACKING of BALLS
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 112/126
CASE STUDY V - ARTIFICIAL LIFE
Basic question: Is life characterized by what it does or
by what is made of?
The goal of the artiﬁcial life research is to help to
broaden the empirical database of the biology as a
science.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 113/126
MAIN APPLICATIONS of INFORMATICS BASED
METHODOLOGY
20th-century science has been very successful, especially because its leading
sciences, physics and astronomy, could work and make use of the laws well
expressible through mathematical language using formulas and equations.
After a shift of emphasis to the other areas of science with very complex systems,
for example in case of life-, earth- and atmosphere-sciences, it started to be clear
that it is not feasible to search for their understanding through the usual
mathematical concepts as formulas and equations.
In particular the situation has changes very signiﬁcantly with a shift of emphasis in
science to sciences that have to explore very complex phenomena not exhibiting
regularity, symmetry and periodicity. For example, phenomena being described using
nonlinear dynamics. Phenomena where quite clearly the approaches oﬀered by
mathematics are no longer adequate.
The possibility to obtain huge amounts of data and to perform huge amounts of
computations and to model very complex phenomena and to very complex
visualisations have also radically changed science and technology, and ....
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 114/126
GRAND CHALLENGES of INFORMATICS DRIVEN
METHODOLOGY - I.
The development of tools to do modeling, simulation
and visualisation of complex phenomena and processes.
The development of methods and tools to specify,
design, analyse and verify huge software systems.
The development of tools to mechanized reasoning,
learning and computation.
The development of tools to discover the underlying
simplicity in complex systems.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 115/126
GRAND CHALLENGES of INFORMATICS DRIVEN
METHODOLOGY - II.
The development of methods and tools to manage huge data streams and sets.
Truth-worthiness of the available digital networks information. This is already a
huge problem and its size and importance are rapidly increasing, due to the
decentralisation of the process of internet information creation.
Openness problem for produced information and knowledge. A big challenge is to
deal with scientiﬁc, engineering and methodological problems related to the task of
digitalization and storing of increasingly growing amounts of available information
and knowledge in a proper form that would allow its searching, mining, retrieving
and veriﬁcation by anyone and anytime in a reasonable time. In other words, a huge
challenge is to provide world-wide open access to all available information.
To make informatics thinking, methodologies and tools a basis of current education
process on all levels and in all areas.
To personalise learning processes.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 116/126
APPENDIX
APPENDIX
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 117/126
WHAT G¨ODEL’s INCOMPLETENESS THEOREM ACTUALLY
TELLS US?
G¨odels incompleteness theorem, that is usually seen as
putting some limits on mathematics actually says ”In
order to get more you have to assume more”.
What does that actually (practically) implies in the era
of super supercomputers?
Adding one (some) additional axioms and to make
deductions from them is technically, likely, not too
much. However, due to the limiting capability of
human brain it can be a lot?
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 118/126
INFORMATICS and PHILOSOPHY - I.
Another big challenge for scientiﬁc Informatics is to
revitalise philosophy of science and to ﬁnd out what are
goals, methods and tools of science in the new,
informatics driven, era of science.
Revolutions in physics and biology at the end of 19th
century were accompanied by intensive philosophical
discussions concerning goals, methods and tools of
science.
At the end of 20th century philosophy of science was
almost dead.It was not fashionable to talk about
science. The mode shifted to doing science.
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 119/126
INFORMATICS and PHILOSOPHY - II.
Now with new scientiﬁc methodology most of the old
questions come up in a new setting.
For example, the goal of the science was to get an
understanding of nature through understandable
models and reductionism was the main method.
It is getting clear that some key phenomena of nature
and society are so complex that any reasonable and
useful model of them has to be too complex to be fully
understandable by people.
It seems that our goals have to change - we can and
have to be, in some cases happy with models that are
too complex to be fully understandable by people if we
would be able to work with them, with the help of
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 120/126
INFORMATICS and PHILOSOPHY - III.
Informatics driven methodology is starting to have big
impacts also on the philosophy of science. On the way
we see goals of science, the character of scientiﬁc
research, scientiﬁc methods, ways knowledge is
produced, character of knowledge and of the scientiﬁc
truth, level of precision we drive for and are happy with
and so on.
For example, one of the basic assumption of science
was a belief that natural science should concentrate on
the study of simple systems that can be suﬃciently well
speciﬁed by very few qualitatively diﬀerent parameters
and so they can be handled by human mind.
Physics has been then the most successful because
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 121/126
NEW TYPES of SCIENTISTS
New methodology creates also a new class of scientists - in
addition to theoreticians and experimentalists we have
scientists that understand and master informatics-driven
methodology and have diﬀerent approach to and use
diﬀerent tools for knowledge acquisition, presentation
(especially visualisation).
prof. Jozef Gruska IV054 2715. Future of Informatics - Chapter 6 122/126