VERIFICATOR

  
 

     
     
   
               
               
 
GEBRUIKSAANWIJZING. Dit programma biedt de mogelijkheid om modellen voor predicatenlogica te construeren om vervolgens predicaatlogische formules te evalueren op zo'n model.

MODELCONSTRUCTIE. Het model wordt geconstrueerd in het grote gele vlak met behulp van de knoppen rechts daarvan. De indicatie Individual geeft aan dat in eerste instantie de individuen ingevoerd kunnen worden. Kies deze door de knoppen Arch, Fonz, Hank resp. Luke aan te klikken.

EIGENSCHAPPEN. Om de gekozen individuen eigenschappen toe te kennen klik PROP aan. De indicatie bovenaan verandert ter verduidelijking in Property. U kunt de uitverkoren individuen voorzien van twee eigenschappen: pijprokend (P) en haardragend (H). Kies een individu met de corresponderende naam-knop en wijs hem de gewenste eigenschap toe door op HAIR of PIPE te klikken. Vervolgens wordt in het model de eigenschap ingetekend.

RELATIE. Er kan één relatie toegekend worden. Dit wordt in het model mbv pijlen weergegeven. Dit geeft aan dat een individu een tweede individu kent, 		  waarbij de pijl van kenner naar gekende loopt. De pijlen kunnen toegevoegd worden door de indicatie op Relation te zetten door op REL te klikken. Vervolgens zorgt het aanklikken van twee individuen mbv de naam-knoppen voor een pijl van de eerst aangeklikte naar de tweede.

RANDOM MODELLEN. De gebruiker kan ook het programma zelf modellen laten kiezen mbv de knop RANDOM MODEL. Men kan ook alleen de individuen, de eigenschappen en de relatie laten kiezen. Stel de indicatie op Individual, Property of Relation en kies daarna de knop RANDOM.

RUIMEN. Men kan individuen weer uit het model weghalen. Kies hiertoe met de knop -IND. De indicatie geeft nu Individual aan. Klik vervolgens op de naam-knop van het individu dat moet worden weggenomen. Om het hele model te legen kan men de knop CLEAR MODEL gebruiken. Om alleen eigenschappen of de relatie te legen verander de indicatie naar Property of Relation en klik op CLEAR. Indien de indicatie op Individual staat dan heeft CLEAR hetzelfde effect als CLEAR MODEL. 		  FORMULES. Invoeren van formules verloopt hetzelfde als bij de waarheidstabulator. De constanten a, f, h en l verwijzen direct naar de individuen respectievelijk Arch, Fonz, Hank en Luke. Verder kan er ook gebruik gemaakt worden van het gelijkheidspredicaat =. U kunt de formule verbeteren dmv terugwaartse eliminatie van symbolen mbv de knop <-. Verwijdering van de hele formule kan mbv de knop CL.

EVALUATIE. Evaluatie van een formule geschiedt mbv de knop EVAL. Groen licht wil zeggen dat de ingevoerde formule waar is, rood licht dat deze onwaar is. Als het blauwe lampje oplicht is er sprake van foutieve invoer.

VRIJE VARIABELEN. Formules met vrije variabelen zijn ook toegelaten. Na evaluatie kan dan ook het oranje lampje oplichten. Dat wil zeggen dat de waarheidswaarde afhangt van de waarde die toegekend wordt aan de vrije variabelen. Deze mogelijkheden worden bijgehouden rechtsonder op de blauwe veldjes. Links worden waardetoekenningen gegeven die de formule waar maken, en rechts de toekenningen die de formule falsifiëren. Door op POS resp. NEG te klikken kunnen alle ondersteunende c.q. afwijzende toekenningen bekeken worden.
TERUG