Tu powinny sie znalezc kryteria, ktorymi maja sie kierowac recenzenci przy recenzji artykulu do FM (i MML)

-- GrzegorzBancerek - 09 Dec 2005

0. W bibie obowiazkowe jest podanie przynajmniej jednej pracy niemizarowej, ktora jest mizarzona - zmienione zgodnie z sugestia PR: Sprawdzic, ze autor powoluje sie na prace (na ogol opublikowana), ktora mizarzy. Moim zdaniem, to jest powazny wymog. W tym co recenzuje tego nie robia. Jest pewien klopot jak chodzi o folklor ale tez na ogol autorzy korzystaja z czegos, np ten ostatni chinski zespolowy wklad. Ale np. w juz przyjetym GFACIRC_1 autorzy nie napisali skad zerzneli to co formalizuja, a abstrakt jest napisany tak, ze mozna odniesc wrazenie ze autorzy sami to wymyslili, co jest nieprawda. (dodane przez PR)

  • DYSKUSJA:

Założenie, że wszystkie artykuły są tylko formalizacją wcześniej gdzieś opublikowanych prac (czyli nie są oryginalnymi pracami) jest wdług mnie błedne, a zmuszanie do podawania naciąganych źródeł to przegięcie. -- GrzegorzBancerek - 12 Dec 2007

W pelni popieram powyzsza opinie, ze takie zalozenie jest bledne - problem w tym, ze nigdzie na tej stronie nic takiego nie jest napisane. Wydaje sie, ze wiekszosc prac oddawanych do MML ma charakter: a) pracy formalizujacej jakas publikacje (i to jest napisane wyzej) lub b) pracy w pelni oryginalnej (choc wydaje mi sie, ze formalizacja istniejacego wyniku tez moze byc oryginalna). Byly dyskusje, czy jesli mizarzy sie elementarne twierdzenie z podrecznika np. algebry, to nie jest naduzyciem wpisywanie tego podrecznika (swoja droga, znasz, Grzegorz, przypadek, zeby pod pozorem odrzucenia artykulu ktos zmuszal autora do dodania jakiejs pozycji bibliograficznej? A jesli autor dopisuje cos, co jest naciagane, to juz problem poziomu autora...), ale np. spojrzenie na liste cytowanych pozycji np. w artykule AOFA_000, zeby daleko nie szukac, pokazuje, ze nie takie pozycje sa dopisywane. Np. TARSKI albo "Subsets of complex numbers". Wg mnie, nie jest. Jesli zas chodzi o prace oryginalne, rozumiem, ze niektore sa na tyle oryginalne, ze caly wklad jest czysto autorski. O ile pamietam proces recenzyjny ktoregos z MKMow, to przynajmniej dwie prace byly ocenione negatywnie m.in. z powodu braku jakiejkolwiek bibliografii. Mialem sygnaly z zewnatrz zespolu okolomizarowego, ze "wy sie powolujecie tylko na mizarowe prace i zadne inne". Jesli poprzez dopisanie kilku sensownych i na temat pozycji bibliograficznych mozna zniechecac mniejsza liczbe przegladaczy FM do samego zespolu, to kosztuje to chyba mniej niz nieokreslone w czasie ulepszenia implementacyjne. -- AdamGrabowski - 12 Dec 2007

1. Typesetting: tu mam na mysli np. odpowiedni indenting zwiekszajacy czytelnosc, niepowielanie spacji i wolnych linii tam, gdzie nie jest to szczegolnie uzasadnione. Generalnie mozna radzic uzywanie Emacsa i dostepny tam automat. Tutaj tez warto zauwazyc komentarze bez zadnego znaczenia dla uzytkownikow MML

  • DYSKUSJA:

2. Sformulowanie definicji i twierdzen (m.in. dublowanie pojec, poziom ogolnosci)

  • DYSKUSJA:

3. Zbedne bloki w artykule (w tym eksportowane twierdzenia uzasadniane jedynie przez referencje biblioteczna)

  • DYSKUSJA:

4. Wydzielanie lematow, jakosc dowodow

  • DYSKUSJA:

5. Czystosc pod katem dostepnego software'u recenzyjnego

  • DYSKUSJA:

6. Jakosc bib-a (angielszczyzna, adekwatnosc do tresci, typesetting)

  • DYSKUSJA:

7. Uporzadkowanie twierdzen (podzial na sekcje, wydzielenie preliminariow)

  • DYSKUSJA:

8. Dlugosc artykulu (nie powinien byc krotszy niz 1000 linii). (PR: Te 1000 to jakas przypadkowa liczba. Proponuje, zeby w artykulach "folklorystycznych" tzn jak ktos formalizuje podrecznik "niskiego" poziomu takim limitem bylo raczej 5000 linijek.

  • DYSKUSJA:

9. Jak ktos proponuje Part I to taki artykul moze byc przyjety jak gotowe sa pozostale Parts, zeby bylo widac sens tego podzialu na czesci. :PR)

  • DYSKUSJA:

10. Slowniki - zgodnosc symboli ze znaczeniem pojec, ktore okreslaja; czytelnosc, odpowiednia dlugosc

  • DYSKUSJA:

11. Jakosc srodowiska - wykorzystanie dyrektyw

  • DYSKUSJA:

12. Odpowiednie sformulowanie definicji: mozliwie drobne wydzielanie atrybutow, unikanie duzych koniunkcji

  • DYSKUSJA:

13. Unikanie duzych alternatyw w poprzedniku (koniunkcji w nastepniku)

  • DYSKUSJA:

-- AdamGrabowski - 16 Feb 2006


Andrzej Trybulec wrote (Nov 7, 2005):

Powinnismy rozdzielic recenzjowanie:

A. Postaci 'publikacyjnej' (to co jest konieczne dla FM: tytul, tytuly sekcji, streszczenie, formaty , moze cos jeszcze

B. Recenzja samego artykulu mizarowego. Tutaj pewnie mozna dalej podzielic na recenzjowanie samego artykulu i abstraktu, ale wydaje sie, ze czesto idzie o obie rzeczy na raz.

B1. Oczywiscie recenzent powinien sprawdzic, czy wszystkie enhancery zostaly wykorzystane (nie zglaszaja beldow)

B2. Enhancery, ktorych nie ma, bo niekomu sie nie chcialo napisac, albo sa zawodne i nieropowszechniane. Np. Niepotrzebne zmienne Niedostepne zalozenia (ktorych nie mozna usuwac w przeslankach schematu) Powtorzenie stwierdzen (lacznie z delokalizacja) to niby jest, ale implementacja Milewskiego psuje artykul; no coz pogadamy na obronie - zawsze jest podejrzane, jezeli doktorant twierdzi, ze cos zrobil, a nie mozna tego wdrozyc.

Coraz bardziej istotne jest czy autor pracuje we wlasciwym srodowisku:

C1. Uwzglednienie potrzebnych rejestracji

C2. Jak jest twierdzenie rejestrujace, to czy jest rejestracja Tutaj, zwlaszcza po ostatnim wzmocnieniu rejestracji funktorowych, trzeba by chyba wprowadzic zasade, ze zamiast wprowadzac rejestracje, gdy twierdzenie rejestrujace jest w bazie, to wnioskowac rewizje artykulu, w ktorym to twierdzenie zostalo udowodnione. Czy ma to zrobic autor, czy raczej moze recenzent.

C3. Czy nowa dyrektywa 'definitions' zostala w pelni wykorzystana, to wlascieiwe jest automatyzowalne (czesciowo). A propos, zgadzam sie z kolegami, ze to powinna byc inna dyrektywa, moze 'expansions'.

D1. Czy nie jest drugi raz zdefiniowane to samo. To jest nierozstrzygalne, wiec tylko czesciowo moze byc zautomatyzowane.

D2. Niepotrzebne, nieuzyteczne, definicje. To trudna decyzja dla recenzenta, ale mamy w bazie przyklady, przede wszystkim funktory, ktore sa tylko potrzebne po to, zeby strukture zdefiniowac przez agregat.

D3. Czy sa w bazie definicje, ktore pownny byc wykorzystane, np. f.(x,y) zamiast f.[x,y] (tu pewnie i tak musimy przeprowadzic sporo rewizji, wiec mozna miec liste definicji, ktorych to dotyczy)

D4. Czy nie powinno sie wprowadzic nowe definicje, zeby skrocic zapis twierdzen (czy tez innych definicji).

WebForm
TopicClassification Select one...
ProjectGroup?

ImplementationDate? N/A
Topic revision: r12 - 2007-12-13 - 10:59:36 - AdamGrabowski
 
Mizar TWiki
This site is powered by the TWiki collaboration platformCopyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki? Send feedback