lip-midterm-2011

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

— |
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)