User Tools

Site Tools


lip-midterm-2011

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

lip-midterm-2011 [2015/10/08 15:20] (current)
Line 1: Line 1:
 +====== LiP midterm project 2011 ======
  
 +
 +==== Submission policy ====
 +
 +  * You must declare your group by **Nov 14, 2011**. ​
 +    * The policy for group collaboration is described [[honesty-policy|here]]
 +    * To declare a group, fill the [[https://​docs.google.com/​spreadsheet/​viewform?​formkey=dG9fYkRHLURYaXVvVkszbFhVNE11OVE6MQ|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 [[https://​docs.google.com/​spreadsheet/​pub?​hl=en_GB&​hl=en_GB&​key=0AinitsakPo0wdG9fYkRHLURYaXVvVkszbFhVNE11OVE&​single=true&​gid=11&​output=html|here]].
 +  * You must submit your project by **Nov 28, 2011**, 23.59 GMT +1 (strict!).
 +  * To submit a project: ​
 +    * Register to the [[http://​moodle.unica.it/​course/​view.php?​id=84|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|honesty policy]].
 +
 +<note warning>​The moodle server will //not// accept submissions after the deadline! ​
 +The deadline is set to **Nov 28, 2011**, 23.59</​note>​
 +\\
 +
 +==== The project ====
 +
 +This project requires to write an Ocaml theorem prover for the [[wp>​Propositional_calculus|classical propositional calculus]].
 +
 +  * project specifications {{:​midterm-2011.pdf}}
 +  * project skeleton {{:​cpc-skeleton.v2.tar.gz}} (updated 15 Nov 2011)
 +
 +\\
 +
 +
 +==== FAQs ====
 +
 +**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 {{:​cpc-skeleton.v2.tar.gz|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)