Your program will read two kinds of data from two files: names and predicates. It will read a formal expression from standard input and check whether that expression is syntactically correct, i.e., built from the names and predicates that have been read, together with a few boolean operators. Then your program will read from a third file a set of basic facts assumed to be true, and check whether the formal expression itself is true. Finally, it will find out whether it is possible to make some basic facts true so that the formal expression itself becomes true (this being trivially the case if the answer to the previous question is positive), and in case it is, write a possible solution to a file. The program will use an abstract interface that you will have to implement. The interface and the client program will be provided.

Detailed description

We suppose that there is in the working directory a file names.txt that contains sequences of symbols called names. The file contains at least one name. A name follows the syntactic rules that characterize C identifiers (it is a nonempty sequence of symbols that are uppercase letters, lower case letters, digits or underscores, and that does not start with a digit). Names are separated by any non-null number of blanks, tabs and new line characters. Intuitively, names denote persons, animals, objects or whatever. The following is a possible contents for names.txt:

juliet 

paul 

fido

peter

melissa

We   suppose   that   there   is   in   the   working   directory   another   file   predicates.txt  that   contains nonempty sequences of symbols called predicates,  in  the  form predicate_name/arity

where predicate_name follows the syntactic rules that characterize C identifiers, and arity is a nonnegative integer (possibly equal to 0). The file contains at least one predicate. Predicates are separated by any nonnull number of blanks, tabs and new line characters. Intuitively, predicate names denote properties or relations between things denoted by names; the arity represents the number of things to which the property or relation applies. Di
erent predicates names may have the same arity. The following is a possible contents for predicates.txt:

taller_than/2

temperature_is_now_above_25/0 rich/1

From the names in names.txt and predicates in predicates.txt, we define as follows the formulas.

• If predicate_name is the name of a predicate of arity n and if names_1,. . . , name_n are names then predicate_name(name_1,...,name_n) is a formula, called an atom. Note that an atom contains no space.
• If formula, formula_1 and formula_2 are three formulas then

- not formula

-[ formula_1 and formula_2 ]

- [ formula_1 or formula_2 ]

- [ formula_1 implies formula_2 ]

- [ formula_1 iff formula_2 ]

are all formulas, where any number of spaces (including 0) can occur before and after the [ and ] symbols.

For example:

• temperature_is_now_above_25
• rich(melissa)
• [rich(melissa) or taller_than(paul,peter)]
• [ temperature_is_now_above_25 and
• [rich(melissa) or not taller_than(paul,peter)] ]
• [[rich(juliet) and rich(juliet)] iff [taller_than(paul,peter) iff rich(juliet)]] are all formulas, whereas
• temperature_is_now_above_30
• rich(gina)
• rich(melissa) or taller_than(paul,peter)
• [ temperature_is_now_above_25 and [rich(melissa) or
• not taller_than(paul,peter,juliet)] ]
• [[rich(juliet) and rich(juliet)] iff
• not [[taller_than(paul,peter) iff rich(juliet)]]]

are not formulas.

We suppose that there is in the working directory a third file true_atoms.txt that contains atoms, representing an interpretation. The file might contain no atom at all. No atom occurs twice in the file. Atoms are separated by any nonnull number of blanks, tabs and new line characters. The following is a possible contents for true_atoms.txt:

temperature_is_now_above_25

taller_than(paul,peter) rich(paul)

rich(fido) rich(peter)

It is then possible to establish whether a formula is true or false in the interpretation as follows:

• An atom is true just in case it occurs in true_atoms.txt.
• A formula of the form not formula is true just in case formula is false.
• A formula of the form [ formula_1 and formula_2 ] is true just in case formula_1 and formula_2 are both true.
• A formula of the form [ formula_1 or formula_2 ] is true just in case at least one of formula_1 and formula_2 is true.
• A formula of the form [ formula_1 implies formula_2 ] is false just in case formula_1 is true and formula_2 is false.
• A formula of the form [ formula_1 iff formula_2 ] is true just in case formula_1 and formula_2 are both true, or formula_1 and formula_2 are both false.