User Tools

Site Tools


LiP midterm project 2011

Submission policy

  • You must declare your group by Nov 14, 2011.
    • The policy for group collaboration is described here
    • To declare a group, fill the form.
    • You must declare your group even though you want to work alone (otherwise I cannot assign you an ID).
    • The groups and their IDs are displayed here.
  • 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-gXX.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

The project

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


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 Download the updated version of the skeleton.

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

File "", 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 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)