Logic Project (2013-2014):

---

Write a program in the language of your choice (C, C++, Java, Scheme or Prolog) that can take as parameters: the name of a file containing a propositional formula written in tptp syntax and the name of an optional output file.

This program should be able to decide the satisfaisabilty of the given formula using the resolution method and to write the result to standard output. (Your program should return true if the formula is satisfiable and false otherwise.)
If the name of an output file is given, the program should be able to output a file containing the list of clauses obtained from the given formula, a refutation example if the formula is unsatisfiable and the result of the decision.

• Syntax (subset of tptp syntax):
  
  
  
  
• We will use <lower_word> as defined in tptp syntax to represent a propositional variable.
  
  

  <lower_word>	::- <lower_alpha><alpha_numeric>*
  <numeric>	::: [0-9]
  <lower_alpha>	::: [a-z]
  <upper_alpha>	::: [A-Z]
  <alpha_numeric>	::: (<lower_alpha>|<upper_alpha>|<numeric>|[_])

  
  
• Remark : constants true and false are represented by $true and $false in tptp syntax.
  
  
• Example 1:
  
  Satisfaisability of
  p ∧ [(¬p ⇒ ¬q) ⇒ (p ⇒ q)]
  
  $ ./resolution ex1 ex1.sol
  -> The formula is satisfiable.
  
    -> ex1, ex1.sol
  
  
• Example 2:
  
  Satisfaisability of
  ¬([(p ∧ q) ∨ (r ⇒ s)] ⇒ [(p ∨ (r ⇒ s)) ∧ (q ∨ (r ⇒ s))])
  
  $ ./resolution ex2 ex2.sol
  -> The formula is unsatisfiable.
  
    -> ex2, ex2.sol
  
  

Additional details :

• If there is no parentheses, use these two rules to remove the ambiguity :
  
  
  1. Operator precedence : (in decreasing order)
     
     1. ~
     2. &
     3. |
     4. <=, =>, <=>, <~>
  2. When an operand is surrounded by two operators of the same precedence, we group the operand with the operator to his right.
     
     
  3. Examples:
     
     p & q | r    is logically equivalent to    (p & q) | r
     
     p => q => r => s    is logically equivalent to    p => (q => (r => s))
     
     

Remarks:

• You will work in teams of 2 students.
  (Don't forget to send an email with your group composition before 3rd December 2013, 23:59.)
• Your code should compile and work on Linux.
  (ms800 computers will be used as reference.)
• Pack your work in a compressed tar archive named logic_name1_name2.tar.gz (thanks).
• Your archive should contain your source code and a small report in PDF format.
  Your report will explain all your non-trivial choices and everything you find useful for correction.
• Mail your work to lens@montefiore.ulg.ac.be by 20th December 2013, 23:59 from your ULg email, with [INFO-0051 Project] as subject.
  Include your co-worker’s e-mail address as CC.
• Your program should be easy to build. If necessary, you could provide an INSTALL file to explain how to build it; list libraries to install, ...
  But, keep it simple, something like make should suffice !
• Parts of the correction will be automatized. So the name of your program should be resolution and work as described in the examples.
  (For example: for Java program, you could provide a script named resolution to launch your program, ...)
• Project submission due: 20th December 2013, 23:59

  <-- Back to course page