search

mcifra / prieskumnik-struktur

Prieskumník sémantiky logiky prvého rádu
https://fmfi-uk-1-ain-412.github.io/structure-explorer/
1 stars 0 forks source link

function symbol bug #12

Open kisel4 opened 6 years ago

kisel4 commented 6 years ago

Chyba je pri interpretovaní funkčných symbolov. Pri použití len niekoľkých (nie všetkých) symbolov z domény je výsledkom,, že štruktúra spĺňa formuly, hoci by nemala struktura su09 - 1

crnkjck commented 6 years ago

@mcifra, ako to vyriesime?

  1. Interpretacia funkcneho symbolu by mala zobrazovat, ze nie je uplna.

  2. Zaroven sa mi ale zda dobre, aby sa stale dali vyhodnocovat formuly, ktore neuplne interpretovany funkcny symbol bud neobsahuju alebo ich chybajuce pripady nezaujimaju (napr. formulu φ2 v priklade nezaujimaju hodnoty funkcii manzel/manzelka pre tie x, ktore nie su ani Muz ani Zena).

    Takze ak sa pri vyhodnocovani termu/formuly narazi na argumenty, pre ktore nie je funkcia definovana, malo by sa namiesto Spravne/Nespravne napisat Nemozno vyhodnotit (alebo nieco podobne). Ak sa ale na taky pripad nenarazi, term/formula by sa mali vyhodnotit ako doteraz.

Problem je, ze takto sa sice vyriesia zaujimave pripady, ale na dodefinovanie funkcie pre vsetky argumenty stale treba doplnit zvysne. V pripade prvorodene_dieta je celkovo 49 parov, ktorym treba priradit hodnotu. To sa nikomu nebude chciet. Chcelo by to nejaku moznost "dodefinovat" funkciu tak, aby sa vo vsetkym chybajucich pripadom priradil nejaky jeden vybrany prvok.

mcifra commented 6 years ago

Narhujem to vyriešiť tak, že keď je nejaký funkčný symbol použitý vo výraze s argumentami pre ktoré nie je definovaný, tak výraz nevyhodnotiť a ako si navrhol, napísať Nemozno vyhodnotit.

Nemyslím si že je dôležité, aby bola funkcia definovaná pre nejaké argumenty, keď sa nikde nepoužije.

crnkjck commented 6 years ago

Nemyslím si že je dôležité, aby bola funkcia definovaná pre nejaké argumenty, keď sa nikde nepoužije.

Definicia struktury hovori, ze definicny obor interpretacie funkcneho symbolu su vsetky n-tice prvkov z domeny. Ak to prieskumnik nevynuti, ziskaju studenti nespravny dojem. Prinajmensom kontrola v editore struktury by teda mala byt implementovana… Dohodneme to teda zajtra osobne.

crnkjck commented 6 years ago

Ďalší problém s funkčnými symbolmi – nekontroluje sa, či je prvku/n-tici prvkov priradená najviac jedna hodnota. Napr. i(f) = { (1,2), (1,3) } nie je dobre definovaná funkcia