Ghazi Bouselmi's Pages


Here you can find out who I am. Well, also my CV, my publications 

LinkedIn : http://www.linkedin.com/in/ghazibouselmi  View Ghazi Bouselmi's profile on LinkedIn

The challenge definition can be found here "Elementary Wattson". The code is again a bit too dense, it had to be compressed to fit in the maximum 50KB allowed by HakerRank.


19-06-2017 : first draft : grammar definition and input tokenization.

21-06-2017 : bug fixes, first matching/substitution functions, manual proving tests.

23-06-2017 : bug fixes, matching/substitution functions.

26-06-2017 : bug fixes, first success on reccursive proving on some simple cases: still not fully operational.

26-06-2017_bis : bug fixes, fix for infinite inference loops; 20% success rate.

27-06-2017 : nasty bug fix: error in merging lists of constraints/variables instantiation; 40% success rate ( 80% if ignoring the sorting of the results).

    => TODO: proper handling of equality assertions while proving in premises.

The next attempts are aimed at handling equality assertions prior to the proving procedure, as well as solving out-of-memory errors & dead loops.

02-07-2017


The grammar:

<operation> ::= <rule> | <query> | <command> | <no-op>
<no-op> ::= <NOTHING> 
          | "%" <comment>
<command> ::= "quit" "!"
<query> ::= "(" <complex-term-list> ")" "?"
<rule> ::= <simple-term> "."
         | "{" "(" <complex-term-list> ")" "=>" <simple-term> "}" "."
<complex-term-list> ::= <complex-term>
                      | <complex-term> "," <complex-terms-list>
<complex-term> ::= <simple-term> 
                 | <equality-assert> 
<equality-assert> ::= "<" <simple-term> ["=" | "/="]<simple-term> ">"
<simple-term> ::= <name> 
                | <var> 
                | <relational-term>
<var> ::= "#" <number>  <var>  -- this is used internally for var renaming
            | "#" <name>
<relational-term> ::= "[" <name> ":" <simple-term-list> "]"
<simple-term-list> ::= <simple-term> 
                     | <simple-term> "," <simple-term-list>