lip-midterm-2011

- You must declare your group by
**Nov 14, 2011**. - You must submit your project by
**Nov 28, 2011**, 23.59 GMT +1 (strict!). - To submit a project:
- Register to the LIP Moodle site (key: LIP2011KEY)
- Submit all the files of the project in tar.gz format, using the following command (where
*XX*is your group ID,*folder-name*is the name of the folder with the sources):`tar zcvf lip11a-g`

*XX*`.tar.gz`

*folder-name*

- Only the first member of the group can submit the project
- You can submit a project only once.

- You must adhere the LiP honesty policy.

The moodle server will *not* accept submissions after the deadline!
The deadline is set to **Nov 28, 2011**, 23.59

This project requires to write an Ocaml theorem prover for the classical propositional calculus.

- project specifications midterm-2011.pdf
- project skeleton cpc-skeleton.v2.tar.gz (updated 15 Nov 2011)

**Q.** The project does not compile. I get the following error:

Error: Multiple definition of the type name ide. Names must be unique in a given structure or signature.

**A.** There was a misplaced `#use cpc-syntax`

in file `cpc-parser.ml`

. Download the updated version of the skeleton.

**Q.** The project does not compile. I get the following error:

File "main.ml", line 63, characters 21-29: Error: Unbound value subseteq

**A.** You must define a function `subseteq`

such that, given two sets `x,y`

, the expression `subseteq x y`

evaluates to true if `x`

is a subset of `y`

, false otherwise.

**Q.** What does the type constructor `Ide`

in type `formula`

represent ?

**A.** A propositional formula of the form `Ide(x)`

represents a reference to a previously-defined formula named `x`

. This is useful for testing purposes, for instance you can write (in concrete syntax):

let $p1 = a -> b -> c let $p2 = (a and b) -> c |- $p1 <-> $p2

The formula in the last line is represented (in abstract syntax) as

And(Imp(Ide "p1",Ide "p2"),Imp(Ide "p2",Ide "p1"))

Note that the binary connective `↔`

is just syntactic sugar for `→ and ←`

.

In your project, you can neglect to deal with formulae `Ide(x)`

. Indeed, the function `closure`

in file `main.ml`

ensures that the formulas passed as parameter to `models`

, `cnf`

and `resolution`

are always closed (i.e. without any occurrences of `Ide`

).

**Q.** My implementation of `eval`

has type `formula * xyz → bool`

(choose your own `xyz`

), while the specification prescribes the type
`formula * (atom → bool option) → bool`

. Is it correct to use `xyz`

?

**A.** I will not consider it as an error (provided that the function `models`

works correctly and has the type required in the specification).

Note also that there is a typo at page 4, line 6:

such that f v evaluates to true if...

should be:

such that eval (f,v) evaluates to true if...

otherwise the type is different from the prescribed one.

**Q.** To construct the cnf of a formula `p`

, my implementation (1) computes the truth table of p, (2) chooses the rows where the value of `p`

is false, and (3) for each of such rows, add a clause (the atoms set to true are negated, the others are not). Is this correct?

**A.** This produces a correct result, but it is considered an error in this project. According to the specification, you must construct the cnf through a syntactic transformation of the formula. You are not permitted to construct the truth table of the formula (more precisely, you cannot use `eval`

).

**Q.** The project does not compile. The compiler says that the function `formula_of_cdf`

is undefined.

**A.** You must define a function `formula_of_cdf: formula list list → formula`

that takes as input a list of clauses, and outputs an equivalent formula.

lip-midterm-2011.txt · Last modified: 2015/10/08 15:20 (external edit)