Op eigenschap zoeken

Deze pagina biedt een eenvoudige bladerinteractie voor het vinden van entiteiten met een eigenschap met een bepaalde waarde. Andere beschikbare zoekinteracties zijn de zoekpagina voor pagina-eigenschappen en de querybouwer.

Lijst van resultaten

• Beweren en bewijzen/2011-12/feedback/loopband-deel2  + (Op zich ziet het bewijs er prima uit. Veel …
  Op zich ziet het bewijs er prima uit. Veel noeste arbeid. Netjes uitgelegd hoe die iff_e en iff_i regels werken. Alleen wel jammer dat de inhoud van Resetten blijkbaar niet van belang is. Als je die vervangt door 't is ongelijk aan t', kan precies hetzelfde script gebruikt worden. Dus blijkbaar is het niet van belang of er achter Resetten iets zinnigs of onzinnigs zit.
  er Resetten iets zinnigs of onzinnigs zit.)
• Beweren en bewijzen/2011-12/feedback/kassa-deel2  + (Prettig dat er met commentaar is aangegeve …
  Prettig dat er met commentaar is aangegeven welke goal er bewezen moet worden. (Als stond er wel ergens een 0 in plaats van VTB (a + 7100 + 1000).) Zoals gezegd is het jammer dat jullie jullie bewijskwaliteiten niet helemaal tonen. Jullie hebben op een gegeven moment een ∃ in de aanname, maar omdat de intervallen precies overeenkomen, hoeven jullie die niet eens met de exi_e regel uit te werken om vervolgens te laten zien dat er echt zo'n moment is.
  ten zien dat er echt zo'n moment is.)
• Beweren en bewijzen/2012-13/feedback/Scheerapparaat-deel2  + (Prettig dat er wat commentaar tussen staat waardoor beter te volgen is wat er op dat moment bewezen wordt. Gebruikte regels: exi_e, exi_i, dis_i1, replace, lin_solve, interval.)
• Beweren en bewijzen/2011-12/feedback/waterkoker-deel2-her  + (Qed ontbreekt, maar dat is natuurlijk niet echt essentieel.)
• Beweren en bewijzen/2012-13/feedback/Bankkluis-deel2-her  + (Technisch gesproken goed, maar jullie hebb …
  Technisch gesproken goed, maar jullie hebben waarschijnlijk ook wel gemerkt dat jullie alleen de simpele regels imp_e, imp_i, all_e, all_i en zo nodig hebben gehad. Overigens is het wel handig om zinnige namen te geven. Nu gebruiken jullie t5 voor het moment waarop de code wordt ingetoets en t3 (een later moment) voor het moment waarop de sleutel wordt ingestoken. Dat is verre van logisch en verwarrend. Als jullie zinnige namen als 'tcode' of 'tsleutel' (of 'tc' en 'ts' als jullie die andere namen te lang vinden) zouden gebruiken, is het veel makkelijker te zien wat het allemaal voorstelt.
  lijker te zien wat het allemaal voorstelt.)
• Beweren en bewijzen/2013-14/feedback/vaatwasmachine-deel1  + (Tja, er hoefde nog niets te worden gedaan, …
  Tja, er hoefde nog niets te worden gedaan, maar tauto proberen is wel erg optimistisch voor iets in predikaatlogica. Anders gezegd, als tauto het bewijs wel kon afronden, weet je eigenlijk zeker dat het niet spannend genoeg is omdat je dan slechts propositielogica gebruikt.
  je dan slechts propositielogica gebruikt.)
• Beweren en bewijzen/2011-12/feedback/grijpautomaat-deel2-her  + (Tja, het bewijs is alleen maar rondgekrege …
  Tja, het bewijs is alleen maar rondgekregen doordat er gebruik gemaakt wordt van twee keer een hypothesis, waarbij elk van die aannames zeer discutabel zijn. Zeg maar gewoon fout. Ze hebben namelijk de vorm van de standaardfout dat ∀ gecombineerd wordt met ∧ tekens.
  ecombineerd wordt met ∧ tekens.)
• Beweren en bewijzen/2012-13/feedback/Magnetron-deel2-her  + (Toen ik het had over het toepassen van Lem …
  Toen ik het had over het toepassen van Lemma's doelde ik op de manier zoals je bij 'reverse' hebt gedaan. Het was niet de bedoeling om een nieuwe tactiek aan te maken. Het eindresultaat is echter mooi; helaas weet ik niet welke bron je gebruikt hebt om deze tactiek zo te definiëren. Verder zou ik ook graag uitleg hebben gekregen over hoe die tactiek nu werkt. Misschien zit er wel iets illegaals in deze tactiek? (Is niet zo, maar ik had het wel leuk gevonden als jij dat had opgemerkt.) Het voordeel van zo'n lemma is dat je dat lemma eerst moet bewijzen. Maar hoe bewijs je dat deze tactiek alleen maar eerlijke stappen gebruikt?
  lleen maar eerlijke stappen gebruikt?)
• Beweren en bewijzen/2012-13/feedback/Alarmsysteem-deel2-her  + (Twee onmogelijk te bewijzen takken: *Zoals …
  Twee onmogelijk te bewijzen takken: *Zoals ik al drie keer heb aangegeven, zul je geen relatie tussen a en b (a=b+30 of b=a+30) kunnen bewijzen omdat je beide variabelen als onbesproken hebt geïntroduceerd. *Als de negatie van een existentiële uitspraak in de aannames staat, kun je normaliter niet bewijzen dat deze existentiële uitspraak waar is. De exi_e-regel is niet te bewijzen. Verdere onhandigheden: * Je splitst een formule met con_i op en voegt direct daarna met con_e1 het zojuist afgesplitste deel toe. Als resultaat moet je dat twee keer bewijzen i.p.v. één keer. * Als gevolg van die onmogelijke existentiële uitspraak (hierboven) voer je een neg_e-regel uit. Die regel moet je eigenlijk alleen uitvoeren als je al ziet dat er een tegenspraak in de '''aannames''' zit. Dat de conclusie de aannames tegenspreekt is misschien een hint, maar dan moet je op zoek naar de tegenspraak in de aannames.
  p zoek naar de tegenspraak in de aannames.)
• Beweren en bewijzen/2013-14/feedback/elektrischegitaar-deel2-her  + (Verantwoord gebruik van hypothesis. Wel gebruik gemaakt van replace, lin_solve, interval en apply, maar niet van exi_e of dis_e.)
• Beweren en bewijzen/2011-12/feedback/frituurpan-deel2  + (Waarom hebben jullie gekozen voor Z_scope? Op zich is het bewijs natuurlijk wel goed, maar er zit geen enkele moeilijke stap in. Geen replace, lin_solve, interval...)
• Beweren en bewijzen/2013-14/feedback/buizenpost-deel2  + (Waarom unfold op alle onderdelen? Kennen j …
  Waarom unfold op alle onderdelen? Kennen jullie de 'unfold onderdeel in aanname' niet? Daarmee zijn bewijzen veel overzichtelijker omdat je alleen de noodzakelijke onderdelen openklapt. En die interval in het begin is ook nergens voor nodig. Dat commando heb je pas nodig als je iets over de afzonderlijke grenzen moet bewijzen. Verder staan er twee Hypotheses in het bewijs die nergens worden uitgelegd. (En op de slides stond dat dat moest!) Erger is dat de tweede Hypothesis een beetje onzinnig is: x <=y is niet echt gelijk aan x+a <= y+a, maar x+a <= y+a is een gevolg van x<=y. Hadden jullie dit met een → geschreven, was het simpelweg bewijsbaar geweest met all_i, imp_i en lin_solve. En dan had je kunnen laten zien dat je een lemma kunt toepassen.En je had lin_solve gebruikt. Nog een slak om zout op te leggen: antisymmetrie is een wiskundig begrip dat niet veel te maken heeft met wat jullie antisymmetrie noemen. Positief is dan weer wel dat jullie een dis_e nodig hebben. En op zich is het bewijs in orde. Er staat zelfs netjes in commentaar aangegeven waar de tweede tak begint.
  aangegeven waar de tweede tak begint.)

• Beweren en bewijzen/2011-12/feedback/fiets-deel2  + (Wel weer goed dat jullie de gebruikte iff_e regels uitleggen.)

• Beweren en bewijzen/2011-12/feedback/frisdrankautomaat-deel2  + (Zoals verwacht een tamelijk simpel bewijs. Er zit geloof ik een keer een replace in om de zes seconden tijdsverschil in een stuk van vijf en van een te hakken, maar dat is ook zo ongeveer het moeilijkste wat er in zit.)
• Beweren en bewijzen/2011-12/feedback/Verwarmingssysteem-deel2-her  + (alle stappen zijn formeel correct, alleen …
  alle stappen zijn formeel correct, alleen gebruik je op één punt de inconsistente aanname, namelijk bij con_e2 (v = (v - 12)). Omdat je kunt bewijzen dat v gelijk is aan v-12, kun je hier de moeilijkheden van het bewijs omzeilen. Ik zie uit de rest van het bewijs dat je wel serieus bezig bent.
  ijs omzeilen. Ik zie uit de rest van het bewijs dat je wel serieus bezig bent.)
• Beweren en bewijzen/2013-14/feedback/geautomatiseerd-subwayrestaurant-deel2  + (duidelijk gestructureerd met lemma’s en commentaren.)
• Beweren en bewijzen/2013-14/feedback/Schiphol Bagage Sorteersysteem-deel2  + (eenvoudig, maar voldoende afwisselend, en met hier en daar een behulpzaam commentaar.)
• Beweren en bewijzen/2012-13/feedback/Flessenautomaat-deel2  + (het was wel fijn geweest als er meer aanda …
  het was wel fijn geweest als er meer aandacht was geschonken aan de layout van de formules in het Coq-script. Ze zijn vaak breder dan de linkerkolom en toch niet verdeeld over meerdere regels. Positief is dat jullie lemma's definiëren en gebruiken. Echter, bij die lemma's gebeurt ook iets raars. Er staat een forall o:O in de formule terwijl er helemaal niets met o gedaan wordt. De enige reden dat dit gedaan wordt is denk ik omdat de specificatie van in dit geval Sensor niet volgens de systematische methode is gedaan, waardoor er een forall o:O over de hele conjunctie staat terwijl die alleen voor de eerste twee eigenschappen van belang is. Dit heeft tot gevolg dat jullie op een gegeven moment de eigenschap 'O' moeten bewijzen. Dat kan dan toevallig via assumption, maar wat betekent het dat jullie 'O' moeten bewijzen? Gebruikte regels: dis_e, dis_i1, dis_i2, apply, imp_e, imp_i, con_i, con_e1, con_e2, replace, lin_solve, interval, all_e, all_i.
  e, lin_solve, interval, all_e, all_i.)
• Beweren en bewijzen/2011-12/feedback/Brandsysteem-deel2  + (omslachtig (maar niet incorrect) door herhaalde en overbodige invoering van dezelfde aanname.)
• Beweren en bewijzen/2012-13/feedback/Kruimeldief-deel2  + (onaf. Je legt de vinger precies bij het ontbrekende punt. Je zou namelijk aan de specificatie van het Stof_Reservoir zoiets moeten toevoegen als: Als de stofzak niet geleegd wordt, dan wordt de teller niet gereset.)
• Beweren en bewijzen/2012-13/feedback/Stoplicht-deel2  + (onaf. Onvoldoende. In de laatste tak moet …
  onaf. Onvoldoende. In de laatste tak moet je iets bewijzen o.a. op basis van aanname H32b. Dat bewijs verloopt vrijwel precies zoals het bewijs op basis van aanname H32a. Coq is niet alleen magie. Ik verzoek je te proberen om te begrijpen wat je moet bewijzen: Er bestaat een tijdstip w in (v-20, v-8) waarop knop2 is ingedrukt, en je moet bewijzen dat één van de lichten voor auto’s op tijdstip v rood staat. Dat is echt bijna de situatie van aanname H32a (het enige verschil is dat daar knop1 was ingedrukt). Dan bedenk je eerst via welke onderdelen het bewijs verloopt en merk je dat H20 helemaal niet gebruikt wordt, dus dat dis_e overbodig is.
  ebruikt wordt, dus dat dis_e overbodig is.)
• Beweren en bewijzen/2012-13/feedback/verwarmingsysteem-deel2  + (onnodig ingewikkeld: „isI s0 /\ ingT s0 > kamerT s0” bewijs je door con_i. en daarna con_e1 (ingT s0 > kamerT s0). te doen, dus heen en terug naar dezelfde formule?)
• Beweren en bewijzen/2012-13/feedback/Halon-Systeem-deel2-her  + (ontbreekt geheel)
• Beweren en bewijzen/2013-14/feedback/Schiphol Bagage Sorteersysteem-deel1  + (tauto werkt alleen bij bewijzen in propositielogica, niet in predicaatlogica.)