prvy stret usera s is : clovek si na zaciatku uploadne databazu z ktorej chce tvrdenia (.mm files)
vyhlada si axiomu/tvrdenie a potom sa mu zobrazi graf
nejak odlisit axiomy/tvrdenia
hlbku nerozlisovat farebne
malo by to byt usporiadane hierarchicky po hlbke
moznost vydiet tvrdenia potrebne na dokazanie vybraneho tvrdenia / moznost vidiet tvrdenia ktore boli dokazane Z vybraneho tvrdenia
import export zvoleneho grafu (tvrdenia)
teorie tam musia byt
scenar prace s teoriami :
nacita si databazu
zaklikne si co chce robit :
-u1 - z danych teoremov ukaze (tvrdeni ktore si navolil) vsetko co bolo dokazane z danych tvrdeni ktore boli zvolene (uzivatel si vie specifikovat do akej hlbky chce ist) (default do nekonecna)
-u2 - tiez obmedzenie na hlbku, pojde dole k axiomom …
-u3 - pouzivatel si moze zvolit viacere teorie (mozme ratat ze dve pre jednoduchost) (moze byt medzi dvoma teoriami nejaky prienik), prienik sa ukaze farebne, (zobrazenie jak u2 s viacerimi teoriami a zobrazeniim prieniku) (da sa to skombinovat s uloho u2 ak ma uzivatel zvolenu len jednu teoriu tak mu ukaze u2 ak viac tak bude mat prieniek cize u3 je u2 s prienikom viacerich teorii )
- cize len u1 a u2 a prieniky ak mame viac teorii
ak prejdem miskou nad node tak mi to ukaze
clovek prida tvrdenia do teorie pomocou searchbaru v ktorom bude vyhladavat keywords alebo id (keywords z popisu daneho tvrdenia)
vyhladavanie v grafe
import teorie nemusi byt, iba graf, cize aj teorie, ach …, toto ma nizku prioritu (aspon daco)
vediet si ulozit vlasne tie teorie ktore sme si vyklikali (do nejakeho suboru ktory sa da imp)
moje skarede poznamky zo stretnutia :
prvy stret usera s is : clovek si na zaciatku uploadne databazu z ktorej chce tvrdenia (.mm files)
vyhlada si axiomu/tvrdenie a potom sa mu zobrazi graf
nejak odlisit axiomy/tvrdenia
hlbku nerozlisovat farebne
malo by to byt usporiadane hierarchicky po hlbke
moznost vydiet tvrdenia potrebne na dokazanie vybraneho tvrdenia / moznost vidiet tvrdenia ktore boli dokazane Z vybraneho tvrdenia
import export zvoleneho grafu (tvrdenia)
teorie tam musia byt
scenar prace s teoriami :
zaklikne si co chce robit : -u1 - z danych teoremov ukaze (tvrdeni ktore si navolil) vsetko co bolo dokazane z danych tvrdeni ktore boli zvolene (uzivatel si vie specifikovat do akej hlbky chce ist) (default do nekonecna) -u2 - tiez obmedzenie na hlbku, pojde dole k axiomom … -u3 - pouzivatel si moze zvolit viacere teorie (mozme ratat ze dve pre jednoduchost) (moze byt medzi dvoma teoriami nejaky prienik), prienik sa ukaze farebne, (zobrazenie jak u2 s viacerimi teoriami a zobrazeniim prieniku) (da sa to skombinovat s uloho u2 ak ma uzivatel zvolenu len jednu teoriu tak mu ukaze u2 ak viac tak bude mat prieniek cize u3 je u2 s prienikom viacerich teorii )
clovek prida tvrdenia do teorie pomocou searchbaru v ktorom bude vyhladavat keywords alebo id (keywords z popisu daneho tvrdenia)
import teorie nemusi byt, iba graf, cize aj teorie, ach …, toto ma nizku prioritu (aspon daco)
databaza moze byt lokalne v backende a nemusi byt
teorie su low level priorita ?? niesu uz po novom
info o grafe (nejaka tabulka, statistiky)
sedi v i5