If you're too impatient to read this entire document, please check out the examples. But please read this thoroughly at least before submitting any bug reports.
PLoP is basically a tool for evaluating truth values of formulas in given structures. In addition to that, it also can check whether an input file conforms to a specific assignment.
This is the tool that is used for checking your submissions. And you can and should use it also by yourself to be sure that your answers are valid and correct before you submit them. This way, you get immediate feedback e.g. in case there are some syntax errors in your answer.
The tool is supposed to be run from a command line. It needs  as a bare minimum  one command line argument; the file about to be evaluated. It takes other command line arguments as well, but there's more information about that later on.
Please read the examples simultaneously while glancing at the specifications. The input file syntax is meant to be intuitive and easy to digest. You most likely don't want to read the document thoroughly  the examples should give you enough insight to be able to solve the assignments. If you have problems, then review the specification more carefully.
The following example is a standalone input file  you can evaluate it by invoking the PLoP giving this file's name as the only argument.
(* Example 1: Input file. *) % These are singleline comments. (* These are multiline comments. You can ignore them both; that's what PLoP does anyway. :) *) (* Plop files start first with FORMULASsection. In this section, you define the formulas. *) true all x. P(x). false ex x. ~P(x). (* After the formulas, the STRUCTUREsection begins. And the universe definition must start this section. *) universe = {a,b,c}. (* And then the definitions of predicates, functions and constants  in any order you like. *) predicate P = {a,b}.
As an example of evaluating the input above in any of HUT CC's Unixmachines, follow these steps:
use otter
and after that plop example1.txt
(assuming that you gave the file the name "example1.txt"). As a result of running PLoP with the example file, you should see output similar to this:
Formula #1 Intended: true. Evaluated to: false > FAILED Formula #2 Intended: false. Evaluated to: true > FAILED
If you have some questions this example didn't answer, you can find the detailed specification of the input file format here.
The formulas must be entered at the top of the input file. Next, let's see how you should write formula definitions. For reference, check out the connective table.
(* Example 2: formulassection. *) (* Every input file that is to be evaluated should start with at least one formula definition. The definition starts with the keyword "true" (if the formula *should* evaluate to true) or the keyword "false" (if the formula *should* evaluate to false). These keywords are case insensitive; you could write them like e.g. "TrUe" or "falSE" or with any mixed case, if you think that it'd be aesthetically more pleasing. :) It is your job then to make them to evaluate to the specified truth value  if the formula evaluates to something else, the checker reports that the formula evaluation failed. Of course, if you're just evaluating some formulas without the assignment  as we do here right now  you can ignore the outcome. After the keyword comes the formula itself. And the formula is terminated with a dot. (Note that quantifiers are also terminated with dot!) *) % Let's write first a formula with some predicates that have no % arguments: true P1 & Q1 > (R1  P1). % Next, one with predicates that have lots of arguments, so we get to % play with the quantifiers too: false all x. ((ex y. (P2(x,y) & Q2(x,y))) & ex y. ex z. ex s. ex t. P5(x,y,z,s,t)). % Define next the structure in which the formulas will be evaluated. universe = {one, two, three, four}. predicate Q1 = {}. predicate P1 = {<>}. predicate R1 = {}. predicate P5 = {<one, two, four, two, one>}. predicate P2 = {<one, three>, <two, three>}. predicate Q2 = {<three, three>, <two, two>, <one, one>}.
This example consists of a single file too, so you can evaluate it just like you evaluated the example 1.
As you evaluate this example, the output should be similar to this:
Formula #1 Intended: true. Evaluated to: true > PASSED Formula #2 Intended: false. Evaluated to: false > PASSED
Read the chapter about formulassection for more information.
Next, let's check how the predicate and constant definitions work.
(* Example 3  predicates and constants *) % First, some example formulas. true all x. (P(x,a) > (Q(x) & R(a) & T(a))  S). universe = {a,b,c,d,e}. (* Next we will define the predicates and constants. Any variable that isn't bound can be considered a constant. Hence, the "a" in the formula is a constant. Constant definition is easy. Write first the "CONSTANT"keyword, then the name of the constant, equation mark, and then the bound variable. Note that even though "a" is an element in the universe, you must still define the constant  otherwise the formula won't be evaluated! *) constant a = c. (* Now, let's define the predicates. Predicates with no arguments can be either true or false. "{}" means false, and "{<>}" means true. *) predicate S = {}. (* Predicates with one or more arguments are defined by stating all argument permutations for which the predicate evaluates to true. As an example, here we want the predicate R to evaluate to true if and only if given the element "c" as argument: *) predicate R = {c}. (* When listing the permutations of a predicate with one argument, you can write it in two ways: *) predicate Q = {a,b,d,e}. predicate T = {<c>, <e>, <b>}. (* But a definition of predicate with two or more arguments must be written in the latter style! *) predicate P = {<a,c>, <b,d>, <e,a>, <e,e>}. (* The predicates could also be defined as set equations  for example, let's define the predicate R: *) %predicate R = T difference Q. % Commented out for now.
This is a single file example, so evaluate it like the example 1. As you evaluate this example, the output should be similar to this:
Formula #1 Intended: true. Evaluated to: true > PASSED
Read the chapters about predicates and constants for more information.
Now it's time to glimpse the functions. Function definitions work almost like predicate definitions.
(* Example 4  functions *) true all x. (P(F1(x)) & P(F2(F2(x))) & P(F3(x,C))). universe = {a,b,c,d}. predicate P = {a,b}. constant C = c. (* Function maps an argument list of elements to one element in the universe. These mappings can be defined using two different notations for 1argument functions: *) function F1 = {a = b, b = c, c = d, d = a}. function F2 = {<a> = b, <b> = c, <c> = d, <d> = a}. (* For a function with 2 or more arguments, you must use this notation: *) function F3 = {<a,a> = a, <a,b> = a, <a,c> = a, <a,d> = a, <b,a> = b, <b,b> = b, <b,c> = b, <b,d> = b, <c,a> = c, <c,b> = c, <c,c> = c, <c,d> = c, <d,a> = d, <d,b> = d, <d,c> = d, <d,d> = a}. (* Note also that you MUST define the mapping for every possible argument list! (Wildcards make this job a little bit easier  see the next example) *)
This is a single file example, so evaluate it like the example 1. As you evaluate this example, the output should be similar to this:
Formula #1 Intended: true. Evaluated to: false > FAILED
Read the chapter about functions for more information.
The wildcards can be used to shorten the definitions considerably. As an example, let's see how the previous example's function could be shortened:
(* Example 5  wildcards. *) function F3 = { % First, we'll use the *wildcard, that expands to all elements in % the universe. <a,*> = a, <b,*> = b, <c,*> = c, % Next, let's use the sequencewildcard. With this, we can define % sequences of elements and individual elements. <d,[ac]> = d, % Third kind of wildcard just copies the first specified argument % (its use in this context is quite artificial): <d,#1> = a }.
This isn't a complete file, so you can't evaluate it. But you can replace the definition of the function F3 in the example 4 with this one  they should evaluate to same truth value.
Read the chapter about wildcards for more information.
This example introduces you to assignment files. Before we go into details, let's first briefly discuss how you can solve the assignments easily  the easiest way is to follow this simple scheme:
assign2a
, copy it to a file with name
solution2a
. Then you can compare your answer to the
original assignment later on, after you've made your modifications to
the solution2a
file.
solution2a
file. For testing whether your solution works,
evaluate that file just like in example1.
assignment
parameter, like so: /p/edu/T79.3001/bin/plop solution2a
assignment assign2a
. If this results in output that tells you
all formulas passed the test, you can submit your solution. The following is an example of an assignment. After that is shown how you can check your answer against the assignment.
(* Example 6: assignment. *) true all x. P(x). universe = {a,b,c,d}. predicate P = ... . % Fill this yourself!
(* Example 6: answer. *) true all x. P(x). universe = {a,b,c,d}. predicate P = {a,b,c,d}.
Let's save these files with names example6.asgn
and
example6.answ
. First, you should try if the answer
evaluates to the intended truth value:
/p/edu/T79.3001/bin/plop example6.answ
. You should
see the following output:
Formula #1 Intended: true. Evaluated to: true > PASSED
The next step is to evaluate your answer against the assignment, like
this: /p/edu/T79.3001/bin/plop example6.answ assignment
example6.asgn
. You should see the same output:
Formula #1 Intended: true. Evaluated to: true > PASSED
If, however, you had changed your answer so that it wouldn't be consistent with the assignment any more, the last stage would have noticed it. For example, change the answer's formula's quantifier like this:
(* Example 6: answer. *) true ex x. P(x). universe = {a,b,c,d}. predicate P = {a,b,c,d}.
Now, when you try to check your answer against the assignment
(/p/edu/T79.3001/bin/plop example6.answ assignment
example6.asgn
), you get output like this:
 ERRORS:  Error while comparing to the assignment file: The answer file's formula #1 isn't compatible with the corresponding assignment file's formula.
Read the chapter about assignment files in general for more information.
In this example we will examine the assignments more closely, and especially the universe definition and the predicate and constant definitions.
(* Example 7: assignment  universe, predicates and constants. *) % First we need some example formulas. true all x. P(x,c). false ex x. ~R(x). false all x. Q(x). false all x. T(x). (* Next line tells you to come up with a universe that has exactly four elements, and it's first and second elements are a and b. Had there not been the [4], you could have made as big universe as you would have wanted to. *) universe = {a,b,...}[4]. (* Now the assignment wants you to figure out to what element the constant c is mapped to. So replace the "???" with one element. *) constant c = ???. (* And next the predicates. The first one states that you have to define the predicate P using table definition (i.e. P = {<tuples>}.)  that's what the {...} means in this context (actually, it says that you have to use 0 or more tuples). *) predicate P = {...}. (* But you can define the predicate R any way you wish  as a table or a set equation  since the ... is not inside the braces. predicate R = ???.  on the other hand  would accept only set equation answers. *) predicate R = ... . (* Next, you have to define the predicate Q by using only one tuple. *) predicate Q = {<...>}. (* The next line states that you need to define the predicate T with at least three tuples. Two of these tuples have to be the elements "a" and "b". *) predicate T = {<a>,<b>,<...>, ...}.
(* Example 7: answer  universe, predicates and constants. *) true all x. P(x,c). false ex x. ~R(x). false all x. Q(x). false all x. T(x). (* Let's add two elements to the universe, "c" and "d". *) universe = {a,b,c,d}. (* Define the constant c to map to "a". *) constant c = a. (* Then we define the predicate P as a table: *) predicate P = {<*,a>}. (* Note that you can change the order of the predicates compared to the assignment. For now, we first want to define the predicate Q. We use here only one tuple as the assignment requires. *) predicate Q = {<d>}. (* Next, let's define T like this (three tuples, which was the minimum). *) predicate T = {c,a,b}. (* And now we can use the predicates Q and T to define the predicate R. *) predicate R = Q union T.
Try to check your answer now against the assignment, as instructed in example 6. PLoP should print out something like this:
Formula #1 Intended: true. Evaluated to: true > PASSED Formula #2 Intended: false. Evaluated to: false > PASSED Formula #3 Intended: false. Evaluated to: false > PASSED Formula #4 Intended: false. Evaluated to: false > PASSED
Read the chapters about assignments and universe, predicates and constants for more information.
In some assignments you get a fixed structure, but the formulas aren't completely defined. We will next look at some assignment formula examples.
(* Example 8: assignment  formulas. *) (* This kind of structure  the ??? without a following connective  means that you have to add at least one quantifier in its place. *) true ??? (P(x) > Q(x)). (* The next means that you have to figure out which variables are quantified. *) true all ???. ex ???. (R(x,y)). (* The ??? followed or preceded by connective means that you have to write a piece of a formula in its place. This formula can contain arbitrary many connectives and predicates etc. *) true all x. (??? > P(x)). (* So the next one means that you have to write one formula which evaluates to true. *) true ???. % The structure is now completely fixed. universe = {a,b,c}. predicate P = {a,b,c}. predicate Q = {a,b,c}. predicate R = {<*,c>}.
(* Example 8: answer  formulas. *) (* The first one obviously needs an "all x."quantifier: *) true all x. (P(x) > Q(x)). (* In the next formula, we have to figure out which of the variables is universally quantified. *) true all x. ex y. (R(x,y)). (* Here we can write for example this kind of formula in place of the ???: *) true all x. (Q(x) > P(x)). (* And the last one is really trivial... *) true ex x. ex y. R(x,y). (* You can even define additional formulas below these, if you wish. They won't be evaluated while checking your answer against the assignment. So, even though the next one causes the evaluator to print "FAILED", it doesn't matter while checking against the assignment. Hence, this solution would pass. *) true all x. all y. R(x,y). % And we haven't touched the structure. universe = {a,b,c}. predicate P = {a,b,c}. predicate Q = {a,b,c}. predicate R = {<*,c>}.
So when you try and evaluate the example answer above alone, as instructed in example 1, the output will be like this:
Formula #1 Intended: true. Evaluated to: true > PASSED Formula #2 Intended: true. Evaluated to: true > PASSED Formula #3 Intended: true. Evaluated to: true > PASSED Formula #4 Intended: true. Evaluated to: true > PASSED Formula #5 Intended: true. Evaluated to: false > FAILED
But when you compare this example answer against the assignment, as instructed in example 6, the PLoP will print output like this:
Formula #1 Intended: true. Evaluated to: true > PASSED Formula #2 Intended: true. Evaluated to: true > PASSED Formula #3 Intended: true. Evaluated to: true > PASSED Formula #4 Intended: true. Evaluated to: true > PASSED
And thus you know that your answer will pass the test (at least with this example structure).
Read the chapter about formulas in assignment for more information.
Functions are almost like predicates, but they contain also the mapping from the argument tuple to the corresponding element in the universe.
(* Example 9: assignment  functions. *) % We need first some formulas. true all x. all y. P(F(x,y)). universe = {a,b,c}. predicate P = {a}. (* The answer now needs one tuple that starts with "a", one already defined tuple with unspecified mapping, one arbitrary tuple which maps to "a", and you can define more tuples freely (note that the mapping needs to be defined for all possible tuples). ??? in the mapping means that you need to figure out the mapped element. *) function F = {<a,...> = a, <b,a> = ???, <...> = a, ...}.
(* Example 9: answer  functions. *) % We need first some formulas. true all x. all y. P(F(x,y)). universe = {a,b,c}. predicate P = {a}. (* Given the requirements in the assignment, we can easily complete the function F like this: *) function F = {<*,*> = a}.
Now, if you check the answer against the assignment, as instructed in example 6, the PLoP should say something like:
Formula #1 Intended: true. Evaluated to: true > PASSED
Read the chapter about functions in assignment for more information.
All keywords are case insensitive. This includes the connectives, section names etc. etc. The names of the variables, constants, predicates and functions, however, are case sensitive.
The input file essentially consist of two distinct parts.
true all x. P(x).
universe = {one, two, three, four}.
predicate P = {<two>, <three>}.
function F = {<one>=four, <[twofour]>=one}.
constant C = one.
The parts must be in the following order:
PLoP eats the same syntax as the Tabeditprogram's File/Set Root Node dialog box. You can read about the syntax from there, under the Entering a sentencesection  just write a normal file with your favorite text editor, and give it to the PLoP as an input file. For those who don't have time to read manuals, below is a brief reference table of the connectives and their syntax in PLoP.
Every formula begins with either a TRUE
 or a
FALSE
keyword. That tells the evaluator  and more
important, to you  what the intended truth value of that
formula is. In assignment, you then have to complete the partial
definitions in such a way that the formula evaluates to the intended
truth value.
After the TRUE
or the FALSE
keyword comes
the formula itself. It consists of atoms and connectives. Atoms may
contain terms. The naming conventions of atoms and terms is described
in here.
Since the formulas may contain whitespace (tabulators, newlines,
spaces), the formula must be terminated with a dot (.
).
Connective  Syntax  Precedence 

Not  ~  Highest 
Universal quantifier  ALL variable.
or (ALL variable)  Highest 
Existential quantifier  EX variable.
or (EX variable)  Highest 
Conjunction  formula & formula  Medium 
Disjunction  formula  formula  Medium 
Implication  formula > formula or
formula > formula  Lowest 
Equivalence  formula <> formula  Lowest 
You can use as much of parenthesis as you like to change the precedence and to group the formulas as you see fit. Also, chained implications and equivalences are not allowed, naturally.
An example of a formula: TRUE ALL x. ((P(x)) <> Q(x) &
R(F(C,F(C,C)))).
Formulas may contain whitespace, i.e. spaces,
tabulators and newlines anywhere between the separate tokens. Hence,
they must end with dot.
The equivalence predicate  written in input file as =

is a special type of binary predicate. First of all, it is
builtin. You can use it anywhere without ever defining it (in fact,
it couldn't even be defined, since all names must begin with a letter
ranging from "A" to "Z" or with an underscore "_"). Secondly, it's
infixoperator, unlike the other predicates, which are
prefixoperators. That means that instead of writing
=(term,term)
, you should write
term = term
. Feel free to use parenthesis
around the equivalence predicate, as it enhances the readability a
lot.
All of the names given to functions and terms must consist of nothing but upper or lowercase alphabets ranging from "A" to "Z" and numbers from "0" to "9" and the underscore "_". A name can not start with a number.
In order to keep the formulas easier to read, the names given to predicates, variables, constants and functions must be distinctive. Although it would be lexicographically all right to have e.g. a predicate with name "P" and a function with the same name "P", the formula could easily end up to be totally unreadable to a human. Hence, this restriction is enforced.
Names given to the atoms and terms are case sensitive. You can therefore define e.g. a predicate "Pred" and a function "pred".
In assignment file, there might be partially defined formulas. Your
job then is to complete the formulas. These formulas contain the
special question token ???
somewhere
in them.
The token ???
can be in place of a
term (inside a predicate, that is), as a quantifier sequence, as a
quantifier's variable, or in place of any atom. In the first case, you
can complete the formula by writing any term in place of the question
token. In the fourth case, complete the formula by replacing the
question token with any formula or with any atom.
For example, if the assignment file has a formula like TRUE ALL x. (P(x) & ???).
, you can complete
that formula with e.g. TRUE ALL x. (P(x) & P(F(x)) 
Q(x)).
or with e.g. TRUE ALL x. (P(x) & R).
And if the ???
is inside an atom, you
can replace it with any term. E.g. the assignment TRUE ALL x. P(???).
could be completed
e.g. by TRUE ALL x. P(C).
(leaving the quantifier in
vain) or e.g. by TRUE ALL
x. P(f1(f2(f3(f1(f2(f3(x))))))).
The number of ???
tokens specifies the
arity of the predicate as well. Hence, if the assignment has a
predicate P(???,???)
the valid answer
predicate must have two arguments too.
If the ???
token appears in the
assignment in such place that it isn't immediately preceded or
followed by a connective, but it is followed by something else, then
you must write one or more quantifiers in its place. For example,
either true all x. (P(x,y)).
or true all x. ex
y. all z. (P(x,y)).
is a syntactically valid answer for true ??? (P(???,???)).
With quantifiers, the token ???
can be
in place of the quantified variable: ALL
???.
. In this case, just figure out which variable the
quantifier quantifies, and write its name in place of the ???
.
The universe definition must come right after the formulas. The definition
can be described with the following regular expression: UNIVERSE
= {element (,element)*}.
i.e. the universe can
define as many elements as necessary. Elements are separated with
comma, thus forming a list. The element list must be written inside a
pair of braces. The definition must end with a dot.
The universe should  in theory  be a set, but because of the wildcards, the order of the elements is significant. So whenever you change the order of the elements in the universe, you must pay attention to change your wildcards accordingly, if necessary.
The names of the elements must be strings consisting of numbers from "0" to "9" and upper or lowercase letters ranging from "A" to "Z" and the underscore "_". Names are case sensitive.
In assignment file, the universe might be only partially defined. In
this case, the last element of the universe is ...
. This means that you should complete
the definition. Don't remove any of the predefined elements or change
their order!
Additionally, the assignment file may specifically tell you how many
elements it expects. In this case there's a [number]
at the end of the
definition, before the dot. For example: UNIVERSE = {a,b,c,...}[5].
Complete the assignment by introducing new elements at the end of the
list. If the size of the universe is specified, introduce as many
elements as necessary to fill up that requirement. For example, the
following universe would complete the partial definition:
UNIVERSE = {a, b, c, first_user_defined,
second_user_defined}.
After the universe definition, there can be arbitrary number of constant, predicate and function definitions. Their relative order matters only if there are some predicates defined as set equations.
Constants are terms with arity (number of arguments) of 0. They are
thus mapped one element in the universe. This mapping is defined in
the following fashion: CONSTANT name =
element.
It is impossible to say whether a term with 0 arguments is a variable or a constant. Hence, all terms in a formula, that aren't defined as constants, are considered to be variables. If a quantifier tries to bind a constant, it is an error. It's also an error, if there are free variables in a formula.
The assignment file might contain constants whose mappings are left
unspecified: CONSTANT name =
???.
In this case, simply complete the definition by inserting
a suitable element in place of the ???
.
For example, an assignment's unspecified constant definition CONSTANT C = ???.
can be completed with
CONSTANT C = element.
 the element
must
then be listed in the universe, of course.
The predicates can be defined in two different ways: by a truth table (for which arguments the predicate is true) or by a set equation consisting of other predicates and set operators.
The definition of a predicate's truth table is similar to the notation
used in the course handouts. The definition consists of the keyword
PREDICATE
, predicate's name, =
and the set
of argument elements or element tuples with which the predicate
evaluates to true, and the definition ends with dot. A tuple is a list
of elements, separated with comma, and enclosed in angle brackets,
like this: <a,b,c,...>
. These tuples can be of any
length.
Because the truth table is a set, the order of the single tuples or elements is insignificant in that set.
The form of the set of elements or element tuples depends on the predicate's arity.
{}
, which means that the predicate
is false, or {<>}
, which means that the
predicate is true. {(element (,
element)*)?}
, or with a set of tuples, as described
by the regexp {(<element> (,
<element>)*)?}
. These mean the same thing. For
example, if the definition is PREDICATE P = {a,b,c}.
or PREDICATE P = {<a>, <b>, <c>}.
,
it means that the predicate P is true, if the given argument is in
that set, i.e. if the argument is a
, b
or c
. Note that you can't mix elements and
tuples into one set; use only tuples or only elements in the
set.PREDICATE Friend = {<jack, janet>, <dave,
dwight>}.
And an example of a 5argument predicate:
PREDICATE Royal_flush = {<A,K,Q,J,10>,
<K,A,Q,J,10>, ...}.
Another way to define predicates is by writing a set equation. The set equation consists of other predicates connected by set operators. The set relations are listed in the table below. Note that the differenceoperator can't be chained.
Operator  Syntax  Precedence 

Complement  COMPLEMENT set_eq  Highest 
Union  set_eq UNION set_eq  Medium 
Intersect  set_eq INTERSECT set_eq  Medium 
Difference  set_eq DIFFERENCE set_eq  Lowest 
The set equation can be defined as follows: Any predicate is a set equation. Any set equation operator that operates a set equation or a pair of set equations is a set equation.
The set equations can be parenthesized in order to make the equation more readable or to change the precedence of operators.
Please note, that all of the predicates in a set equation must have the same arity, and that a predicate used in the set equation must be defined earlier. The latter restriction prevents infinite recursion in set equations.
Hence, e.g. these examples are valid set equations: PREDICATE P
= Q.
, PREDICATE P = COMPLEMENT Q.
, PREDICATE
P = Q UNION S.
, PREDICATE P = S DIFFERENCE ((Q) UNION
COMPLEMENT S).
 assuming that the arity of P
is
equal to the arity of Q
and S
, and that the
predicates used in the set equations are defined earlier.
Assignments might contain partially defined predicates. If a predicate
definition contains a question token ???
or a list completion token ...
, then you must complete the definition.
...
:
If a list completion token is found inside a tuple, then you can
complete that tuple with a list of elements. For example, a predicate
can be partially defined like PREDICATE P =
{<...>, <a,...>, <a,...>}.
, you must define in
the answer a predicate whose truth table set contains three tuples,
two of them starting with element a
and one freely
completable tuple. Note that the assignment doesn't restrict the
maximum length of the tuples, but you have to make sure that their
length equals to the predicate's arity. For example, if the predicate
P takes 3 arguments, a definition PREDICATE P = {<a,b,c>,
<c,a,b>, <a,c,c>}
would be a syntactically correct
answer. Note that the order of the tuples in the set can be
modified freely, compared to the set of the assignment.
If a list completion token is found at the end of the set, then you
can add as many tuples (or elements in case of a predicate with arity
of 1) to the set. For example, a 1argument predicate P might be
partially defined in the assignment file: PREDICATE P = {a,b,c,...}.
Then you can
define in the answer a predicate like PREDICATE P =
{b,c,a,d}.
Note that you don't have to add any tuples
(or elements) into the partial definition. For example
PREDICATE P = {a,b,c}.
would also be a
syntactically correct answer.
These two can also be mixed in a definition. You might encounter
assignments like e.g. the following: PREDICATE P = {<a,b,...>, <...>,
...}.
This just means that the predicate you define in the
answer must have at least two tuples, of which one begins with
<a,b
.
The third case where the list completion token can be found is this:
PREDICATE P = ... .
(note the fourth
dot that ends the definition). In this case, you can define this
predicate in the answer file as a truth
table or as a set equation.
???
:
The question token in predicate definition always means that this
definition must be completed as a set
equation. The token can be replaced with any set equation. For
example, an assignment PREDICATE P =
COMPLEMENT Q UNION ???.
accepts answers like PREDICATE P
= COMPLEMENT Q UNION S.
or PREDICATE P = COMPLEMENT Q
UNION (S DIFFERENCE (Q UNION S UNION T)).
Note that PREDICATE P = ???.
means,
that you have to write a set equation from scratch  table definition
doesn't satisfy the assignment.
Definitions of functions are much like the truth
table definitions of predicates. The difference is that after each
argument tuple or element, there must be the mapping definition:
= element
. It means that the function maps to the
given element with that argument tuple (or element).
Note also that you have to define all of the mappings  that
means, there must be a mapping for every permutation of the argument
tuple in the given universe. E.g. if the universe is
UNIVERSE = {a,b}.
, then for 2argument function you have
to define a mapping for all argument tuples <a,a>
,
<a,b>
, <b,a>
,
<b,b>
. As an example: FUNCTION F =
{<a,a> = a, <a,b> = b, <b,b> = a, <b,a> =
a}.
Note that here the order of the argument tuple and mapping
element entries is insignificant as well.
There's also another way to define the functions. You can just
simply list all of the mappings in an ordered set, so that the first
element in that set is the mapping for the first argument tuple in the
tuple permutation set. E.g. if the universe is UNIVERSE =
{a,b}.
, then you could define the function FUNCTION F =
{a, b, a, a}.
 this is the same thing as the example function
F
defined above. The first permutation tuple would then
be <a,a>
, the second <a,b>
, third
<b,a>
and so forth.
Examples (assume that the universe is defined like UNIVERSE =
{a,b,c}.
):
FUNCTION F = {a = a, b =
b, c = c}.
or the same thing: FUNCTION F = {a,b,c}.
FUNCTION F = {<a,a> = a,
<a,b> = c, <a,c> = c, <b,a> = c, <b,b> = a,
<b,c> = c, <c,a> = a, <c,b> = a, <c,c> =
a}.
or FUNCTION F = {a,b,a,c,b,c,a,a,c}.
As you can see, creating the function definitions can get tedious with
even rather small universes and functions with low arity. Hence, you
might want to use wildcards instead of
writing all permutations by hand. You can read a more indepth
discussion about wildcards later on, but as
an example, let's write the 2argument function with the help of
wildcards: FUNCTION F = {<*, #1> = a, <a, [bc]> =
c, <b, [a,c]> = c, <c, [ab]> = a}.
The assignment file might define some functions only partially, and
you must then complete the definition. The partial definitions contain
the list completion token ...
, and
just like with predicates, this token can
be found inside a tuple or inside a set.
As an example, the partial definition FUNCTION F = {<a,...> = b, <a,b,c> = c,
...}.
is completed by replacing the partial tuple with one
starting with <a,
and having 3 elements, and by
defining the rest of the mappings (as specified by the ...
at the end of the set).
The partial definitions might also contain the question token ???
in place of the target element of any
mapping. This kind of partial definition is completed by replacing the
question token with some element in the universe. As an example, if
the assignment defines a function FUNCTION F
= {a = a, b = ???}.
, you can define a function FUNCTION F
= {b = b, a = a}.
in the answer.
These two can also occur in the same partial definition, e.g. a
definition FUNCTION F = {<a,a> = a, <a,b> = b,
<b,a> = a, <b,b> = b}.
is a syntactically correct
answer for the assignment FUNCTION F =
{<a,...> = ???, <a,a> = ???, ...}.
Note that you can use the ordered set definition in the answers to the partially defined functions. The assignment can never have these ordered sets defined only partially, but it doesn't mean that you couldn't use them as an answer.
Wildcards are special tokens that can be used in defining predicates or functions. You can replace any element in the definition with a wildcard  but not the function's mapping's target element though. The wildcards then expand into a set of elements.
There are three kinds of different wildcards that you can use.
*
: This wildcard expands to all possible elements in
the universe. For example, in universe UNIVERSE =
{a,b,c}.
, writing a tuple <a,b,*>
is the
same thing as writing the three tuples <a,b,a>,
<a,b,b>, <a,b,c>
. [element ( element)? (, element (
element )? )*]
:
With this wildcard, you can list ranges of elements in the
universe. The range definition, in the form
element1element2
expands to all
elements that are in the universe between element1
and element2
, including the endpoints. For example,
[ac]
in the universe UNIVERSE =
{b,d,c,f,g,a,e,h}.
would expand to the elements
c
, f
, g
and
a
. And [a]
would expand to just the
element a
.
You can also combine the range definitions into the sequence
wildcard with comma. For example, [a,b]
will expand
to the elements a
and b
, and
[ah,f,bd]
in our example universe would then expand
into elements b
, d
, f
,
a
, e
and h
.
As an example, a predicate definition PREDICATE P =
{<[ac,e],[b,c]>}.
is the same thing as the
definition PREDICATE P = {<a,b>, <b,b>,
<c,b>, <e,b>, <a,c>, <b,c>, <c,c>,
<e,c>}.
assuming that the universe is UNIVERSE
= {a,b,c,d,e}.
#number
:
This wildcard copies the previous argument, i.e. the tuple
element, indexed by the number
. The number
must be smaller than the index of the copyargumentat
wildcard. Then the wildcard expands to a tuple that has the same
element in its place as the element in the tuple with that index.
This wildcard is useful only when used in combination with the
other wildcards. For example, a tuple <a,b,#2>
just expands to the one tuple <a,b,b>
. However,
the tuple <*,#1>
expands to the tuples
<a,a>
, <b,b>
,
<c,c>
and <d,d>
, if the
universe is UNIVERSE = {a,b,c,d}.
 that would be a
compact definition e.g. for an equivalence relation.
As an example, a predicate definition PREDICATE P =
{<[ac,f],#1>}.
is equivalent to the definition
PREDICATE P = {<a,a>, <b,b>, <c,c>,
<f,f>}.
in universe UNIVERSE =
{a,b,c,d,e,f}.
.
There are two types of comments recognized: totheendofline
comments and multiline comments. The first type of comment begins
with %
and the comment then goes on to the next newline
character. Multiline comments begin with (*
and end with
*)
. The syntax of these, too, follows the Tabedit's
definitions.
Everything inside a comment in the input file is simply ignored. The lexer drops the input and doesn't generate lexical tokens out of anything inside a comment.
In this course, you get some assignments that are essentially valid input files  lacking only the complete definitions of some parts. It is your task to complete the assignment files so that a) they can be evaluated, and b) the given formulas evaluate to the specified truth value.
You are not allowed to:
???
). During the evaluation of your
answer, the checker might want to change the structure to
something else in order to test your formulas in other structures
too. And these structures wouldn't contain the atoms or terms that
you had added  thus, your formulas would fail the test
immediately.You are allowed to, if you wish, add some extra formulas at the end of the formula list. These extra formulas are then ignored silently by the checker during the evaluation of your answer. But you can use the extra formulas for e.g. dividing a large formula of the assignment into smaller parts and checking what the smaller parts evaluate to.
You can read more about the assignment's formulas, universe, constant, predicate and function definitions from the respective sections.
The assignment file might contain partial definitions in three different structures:
In assignment file, there can be one or more formulas. The order of the formulas is significant: the first formula in the assignment must be matched by the first formula in the answer file. The checker tries to match the first assignment formula with the first answer formula, and if it fails, it reports an error. Then it tries to match the second ones to each other, then the third ones etc. When it reaches the end of formulas in the assignment file, the checker ignores the rest of the formulas  if there are any additional formulas left  in the answer file.
Note that, however, when only evaluating, not checking, all of the formulas are evaluated.
The elements in the universe of an answer file must be in the same
order as in the assignment file. If the universe is partially
defined, e.g. UNIVERSE =
{a,b,c,...}.
, the universe in the answer file must begin
with the same elements, e.g. in this case UNIVERSE =
{a,b,c
.
The order in which the predicates, functions and constants are defined in the answer file isn't important. The order can be changed compared to the assignment file, as long as the definitions remain still legal (this applies only to the predicate's set equation definitions). The only thing that matters is that all of the predicates, functions and constants that can be found in the assignment file, are also present in the answer file, and that there are no additional predicates, functions or constants defined in the answer file.
The order of the tuples (or elements) in the predicate table definition is insignificant. As long as the sets are equal (in mathematical sense) to the assignment's, the answer is valid.
With functions, the order of the entries in the table definition is also insignificant. The answer can also define a function by the ordered set. As long as the resulting mappings are identical, or fulfill the assignments requirements, the answer is considered to be valid.
In some assignments your job is to complete a set of formulas. The checker will in these cases generate new structures and try to evaluate your answer also in these new structures. Some of these structures might also be broken  i.e. in these structures the correct answers will fail. These additional structures are used in the checking process in order to e.g. fail tautological answers. Your solution should be valid in every structure imagnable.
The checker also makes it possible to enforce some restrictions for the formulas. For instance, it might be required that your formulas are written into implicative form. These requirements are generally clearly stated in the assignments.
In some cases, the checker also ignores some of the formulas completely. This usually happens with the "broken" structures.
The PLoP can be found already installed in any of the HUT Computing Centre's UNIXmachines. If you wish, you can install it to your own computer as well (assuming that J2RE is available for your computer). The first two subsections describe how to get the PLoP running, either at HUT CC or in your own computer. Rest of this section discusses about the different modes of PLoP operation and the command line parameters available to you.
The HUT Computing Centre's UNIXmachines (connect via SSH to one of the UNIXmachines; some are listed in here, or log in to one of the CC's Linuxmachines) have the necessary environment already setup. This is the easiest way to use the PLoP, as you don't need to install or setup anything yourself.
Once logged in, you can invoke the PLoP by typing in command
/p/edu/T79.3001/bin/plop
. Try it, it should say
something like "No input files.". If you first run the command
use otter
, you don't have to write the full path anymore
 plain plop
works.
The plop script runs the command java jar
/p/edu/T79.3001/bin/Plop.jar
with the given parameters. You
can run the PLoP this way too, if you please. Then you can give also
some parameters for the java command as well. (Though this should not
be necessary at all, so don't worry about it. Use the script!)
You should give the PLoP then some parameters. For example, if you
want to evaluate a file "./test.txt", then you should type in command
/p/edu/T79.3001/bin/plop ./test.txt
.
Later on, the phrase "invoke PLoP" should be understood as to type in
the command /p/edu/T79.3001/bin/plop
with the specified
parameters (or after calling use otter
, plop
is enough).
First of all, you need Java 2 Runtime Environment (J2RE) version 1.3.1 or newer to be able to run the PLoP. If you don't have it already installed, you can download it (or some newer version) from this official Java site (follow the "Get it Now"link). Read the installation instructions carefully, and proceed with the install only if you feel confident enough to install Java. If you aren't able to install Java, then just use the preinstalled one at one of Computing Centre's UNIXmachines.
Please note that PLoP isn't still thoroughly tested! If you run PLoP on your computer, you do so on your own responsibility! The safest option is to run it on one of the Computing Centre's UNIXcomputers. And to minimize the possible damages if you decide to run it on your computer, never run PLoP logged in as a system administrator (e.g. root in UNIX), if applicable.
Once you have the Java installed, you should open a console (in UNIX)
or a dosprompt (in Windows) and try to execute javacommand
java version
. If it works, then you're ready to start
PLoP. First, download the Plop.jarpackage. Save
the Plop.jarfile to somewhere  just make sure you remember the
path. Then, you can invoke the PLoP by executing java jar
path_toPlop.jar
. Now, you should see some output like
"No input files.".
You should give the PLoP then some parameters. For example, if you
want to evaluate a file "test.txt", then you should type in command
java jar path_toPlop.jar test.txt
.
Later on, the phrase "invoke PLoP" should be understood as to type in
the command java jar path_toPlop.jar
with the
specified parameters.
Once you have written your answer to a file using your preferred text
editor, you can then evaluate it. Just invoke PLoP with the text file
name as an argument. PLoP then evaluates the file and prints out any
warnings and errors and the result of the evaluation. Normal
invocation has the parameters of the form [options]
answer_file_name
.
If you have defined predicates, constants or functions that don't
exists in any of the formulas, you can turn off the warnings by
invoking PLoP with nowarnAboutUnusedPredicates
,
nowarnAboutUnusedFunctions
and
nowarnAboutUnusedConstants
options accordingly. The
first parameter is useful only when there's a predicate defined with
set equation that needs other predicates  that aren't used in the
formulas  in the equation. Otherwise, it is recommended to keep the
warnings on. After all, you aren't supposed to add any of your own
predicate, function or constant definitions to the answer.
If you use wildcards to specify the function mappings or predicate
truth tables, two different wildcards in the same definition might
expand to intersecting sets of tuples. In this case, the PLoP prints
out a warning. These warnings can also be turned off with option
nowarnAboutDuplicateTruthTableEntries
for predicates
and with option nowarnAboutDuplicateMappings
for
functions.
You can get some brief help about the recognized options by invoking
PLoP with help
option. To check the version of the
PLoP, use option version
. With these two options, you
don't need to specify an input file.
You can test your answer's conformance to the assignment by giving the
answer file as first parameter and the assignment file as the second
parameter, prefixed by the assignment
option. Thus,
the assignment checking invocation's parameters are of the form
[options] answer_file_name assignment
assignment_file_name
.
PLoP will then print out the errors (if the answer doesn't conform to the assignment file) or the result of the evaluation.
First of all, make sure you are using the latest version of the
PLoP. The computing centre's vipunen.hut.fi machine should always
have the latest PLoP installed, so invoke the PLoP there with
version
parameter. If you have older PLoP in use,
please try the latest version, which you can download here. If the
problem persists, then read on.
Before submitting bug report, please first check if the issue has already been discussed in the faqsection of this manual.
Send the bug reports to the address t79144
at
tcs.hut.fi
. Please start the subject line with
[plopbug]:
appended with the bug
description. For meaningful bug reports, you should also
describe or include the command line parameters (or the
complete invocation) you used, the input file(s) you used, the output
you got, the computer you used (if not CC's machine, then the
operating system) and the version of java runtime library
installed (you can figure it out by executing java
version
), or if the error appears with the checker, tell us
your student number.
Version  Changelog 

1.0.0  Initial version 
Q: When I check my solution myself with the plop, it prints
PASSED
to all formulas, but when I submit it, the checker
prints output like this:
Failed (thread stopped) Test failed!
A: This output means that the evaluation of your solution takes so much time, that the checker process decides to stop the evaluation  your solution wouldn't probably be correct anyway.
The error message should be corrected to something more informative in future (x > 1.0.0) versions.
Q: When I check my solution against the assignment like this
plop solution3c assignment assign3c
, I get an error
message like this:
 ERRORS:  Error while comparing to the assignment file: The truth table of the predicate "InitOne2" has been altered. Error while comparing to the assignment file: The truth table of the predicate "InitZero1" has been altered.
I get this error message even though I haven't modified the structure at all; it is an exact copy from the assignment file!
A: This is a bug in the plop version 1.0.0. If the assignment's structure contains predicates which have been defined with empty sets, the comparsion between assignment and even a correct answer will fail.
If you submit a correct answer, it will be succesfully checked though, and you can pass the assignment. This bug only prevents you from testing the solution by hand. The bug will be fixed in the next future release.
Q: When I try to evaluate my answer with plop, it says something like this:
Error in input! plop.M at plop.ab.<init>(Unknown Source) at plop.A.<init>(Unknown Source) at plop.Plop.a(Unknown Source) at plop.Plop.main(Unknown Source) Token: .
A: The parser of the plop version 1.0.0 has some problems with
formulas that have syntax errors in quantifiers. In this case, your
answer most probably contains a line with a quantifier like all
.x
or something like that.
This is a bug in plop, and will be fixed. You can avoid this problem by fixing the syntax errors in your input.
Q: When I check my solution myself, I get PASSED
, but
when I submit my solution, the output from the checker says something
like this:
 ERRORS:  Error: Formula #1 doesn't comply with requirements: Formula isn't implicative (The condition of the implication is not a conjunction of atomic formulas (a negation was also seen).).
A: The checker system might enforce some additional restrictions for
the solution. In this case, it requires the formula #1 to be in
special implicative form. You can check if your solution passes these
additional restrictions by giving the checker e.g. the option
implicative <number>
, where number
corresponds to the formula that should be restricted. You can add more
than one options like this, each for one formula.
Keyword  Description  See chapter 

% 
Begin an endtotheline comment  Comments in input files 
(* 
Begin a commentsection  Comments in input files 
*) 
End a comment section  Comments in input files 
TRUE 
Begin a formula whose intended truth value is true  The formulassection 
FALSE 
Begin a formula whose intended truth value is false  The formulassection 
UNIVERSE 
Begin the universe definition  Universe definition 
PREDICATE 
Begin a predicate definition  Predicate definition 
FUNCTION 
Begin a function definition  Function definition 
CONSTANT 
Begin a constant definition  Constant definition 
??? 
Used in place of a definition in assignment file  About assignment files in general 
... 
Used in place of a definition in assignment file  About assignment files in general 
. 
End a definition  The PLoP input file structure 
~ 
Negation  Connectives 
& 
Conjunction  Connectives 
 
Disjunction  Connectives 
> 
Implication  Connectives 
> 
Implication  Connectives 
<> 
Equivalence  Connectives 
( 
Left parenthesis  The formulassection 
) 
Right parenthesis  The formulassection 
ALL 
Universal quantifier  Connectives 
EX 
Existential quantifier  Connectives 
* 
Wildcard  Wildcards 
# 
Wildcard  must be followed by a number  Wildcards 
[ 
Wildcard  begin a sequence definition  Wildcards 
] 
Wildcard  end a sequence definition  Wildcards 
 
Separator in sequencewildcard definitions  Wildcards 
= 
This keyword has many meanings: it can be an equivalencepredicate, and it is also used in definitions  The PLoP input file structure 
{ 
Begin a set or a table  The PLoP input file structure 
} 
End a set or a table  The PLoP input file structure 
, 
Separator, used in e.g. sets, tuples and wildcards  The PLoP input file structure 
< 
Begin a tuple  The PLoP input file structure 
> 
End a tuple  The PLoP input file structure 
UNION 
Unionoperator in predicate set equations  Set equation definitions 
INTERSECT 
Intersectionoperator in predicate set equations  Set equation definitions 
DIFFERENCE 
Differenceoperator in predicate set equations  Set equation definitions 
COMPLEMENT 
Complementoperator in predicate set equations  Set equation definitions 
The PLoP command line parameters consist of options and the files to
be evaluated: [<option parameters>] <answer>
[assignment <assign>]
. The only option the PLoP needs
is the answer file  file to be evaluated, except when invoked with
the help
or version
option parameters.
In the following the option parameters are listed. Note that some start with "no", which means that that option is switched off. And in case of conflicting option parameters, the last of these parameters in the command line is dominant.
Parameter  Description 

help 
Print a help message. 
version 
Print version information. 
timeout <milliseconds> 
How many milliseconds the checker is allowed to run for each input file. 0 means infinity (default: 0) 
implicative <formula number> 
Set the requirement for implicative form on for the specified formula. 
 
Escape an option. I.e. the next parameter is a filename. 
checkFunctionMappings 
Check that function is defined for all inputs (default) 
nocheckFunctionMappings 
Do not check that function is defined for all inputs 
automaticNameConstants 
Automatically make constants of unbound variables whose names are equivalent to some element in the universe 
noautomaticNameConstants 
Do not automatically make constants of unbound variables whose names are equivalent to some element in the universe (default) 
warnAboutUnusedPredicates 
Print warnings of defined predicates that aren't used in the formulas (default) 
nowarnAboutUnusedPredicates 
Do not print warnings of defined predicates that aren't used in the formulas 
warnAboutUnusedFunctions 
Print warnings of defined functions that aren't used in the formulas (default) 
nowarnAboutUnusedFunctions 
Do not print warnings of defined functions that aren't used in the formulas 
warnAboutUnusedConstants 
Print warnings of defined constants that aren't used in the formulas (default) 
nowarnAboutUnusedConstants 
Do not print warnings of defined constants that aren't used in the formulas 
warnAboutDuplicateMappings 
Print warnings of duplicate function mapping entries (default) 
nowarnAboutDuplicateMappings 
Do not print warnings of duplicate function mapping entries 
warnAboutDuplicateTruthTableEntries 
Print warnings of duplicate truth table entries (default) 
nowarnAboutDuplicateTruthTableEntries 
Do not print warnings of duplicate truth table entries 
Last update: $Date: 2004/12/02 17:01:16 $