This app evaluates predicate logical formulas on a model. MODEL CONSTRUCTION The model is to be constructed on the yellow panel. First individuals have to be brought on stage. Click Arch, Fonz, Hank and/or Luke, respectively, using the buttons on the panel next to the model screen. PROPERTIES In order to assign properties to the individuals that have been added to the domain press PROP and the indication Indidividual changes into Property. Then select the chosen individual by pressing the button carrying his name, and then the property that you wish to assign to it (HAIR or PIPE) RELATION The model can also be dressed up with a single relation, depicted by arrows, representing that an individual (where the arrow starts) knows some individual (where the arrow points at).

To add an arrow first click REL to switch the indication to Relation and then select two names. The arrow from the first to the second will be added to the model. RANDOM MODELS You may let the program choose a model randomly by clicking RANDOM MODEL. You can also limit this free choice to individuals, properties or relation only. Set the indication to Individual, Property or Relation and then press RANDOM. CLEARING Individuals can be removed by selecting -IND. The indication switches to Individual. Then click the name of the individual that you want to remove. To clear the whole model click CLEAR MODEL. To remove properties and/or the relation select Property or Relation, resp., and then press CLEAR. FORMULAS For specifying formulas you have to use the button panel below the yellow model screen.

Constants a, f, h en l refer directly to the individuals Arch, Fonz, Hank and Luke, resp. For backward deletion of symbols use <-. Clear the formula display by using CL. EVALUATION For evaluation of formulas click on EVAL after you have typed in the formula. Green flashing light means that the formula is true, red indicates falsity. Blue light signals erroneous input. FREE VARIABLES If a formula with free variables has been typed in, then the orange light may start flashing after evaluation. The truth value of the formula then depends on the value of the free variable(s). These variable assignments are registrated on the blue displays. On the left a verifying variable assignment is given, and on the right a falsifying variable assignments are given. By clicking POS or NEG other verifying and falsifying assignments. resp., will be shown.