Show HN: Automatically interpret and validate nested natural logic arguments | Hacker News Reader

Show HN: Automatically interpret and validate nested natural logic arguments

github.com

53 pointsparhamp18 comments

Nice! For comparison, here is how one could approach this task in Prolog. First, let us introduce a few suitable operators, so that we can naturally state the given facts:

    :- op(700, xfy, and).
    :- op(700, xfy, ==>).
    :- op(750, xfy, or).
    :- op(700, fx, not).

With these operators, the given knowledge could be represented as follows:

    fact('I go to school' and 'I study' and 'I exercise').
    fact('I exercise' ==> 'I\'m healthy').
    fact('I study' or 'I\'m sick').
    fact(not 'it rains today').
    fact('I study' and ('I go to gym' or 'I drink a coffee')).
    fact('it rains today' or ('I exercise' and 'I study')).
    fact('I\'m healthy' ==> ('I\'m happy' or 'I\'m fit')).

Now, all it takes is an interpreter for such domain-specific rules. We can easily implement one in Prolog. Here is a starting point:

    true(C)      :- fact(F), conjunction_conjunct(F, C).
    true(B)      :- fact(A ==> B), true(A).
    true(A or _) :- true(A).
    true(_ or B) :- true(B).

    conjunction_conjunct(C, C).
    conjunction_conjunct(A and B, D) :-
            (   conjunction_conjunct(A, D)
            ;   conjunction_conjunct(B, D)
            ).

With this knowledge base and the given deduction rules, we can query for example:

    ?- true('I study' and 'I exercise').
    true .

    ?- true('I study' or 'I\'m sick').
    true .

    ?- true('I go to gym').
    false.

    ?- true('I\'m healthy').
    true .

    ?- true('it rains today' or 'I\'m healthy').
    true .

We can also use this interpreter to ask the most general query, and it enumerates statements it can derive:

    ?- true(T).
    T =  ('I go to school'and'I study'and'I exercise') ;
    T = 'I go to school' ;
    T =  ('I study'and'I exercise') ;
    T = 'I study' ;
    T = 'I exercise' ;
    T =  ('I exercise'==>'I\'m healthy') ;
    T =  ('I study'or'I\'m sick') ;
    T =  (not'it rains today') ;
    T =  ('I study'and('I go to gym'or'I drink a coffee')) .

Note that a more direct formulation is possible too with Prolog. However, an important advantage of the interpreter-based approach is that it lets us stay very close to the task description. Further, we can easily extend this interpreter with more features that can be implemented on top of Prolog.

That is a very useful comparison. Thank you.

Great! One alternative way to reason about these rules is to recognize that these statements can be modeled as propositional formulas, which can be easily solved with Prolog by using a constraint solver over Boolean variables. For example, in SICStus Prolog, such a constraint solver is available as a library:

https://sicstus.sics.se/sicstus/docs/4.3.1/html/sicstus/CLPB...

This of course requires a slightly different way to encode the task, using logical variables:

    ?- sat(School*Study*Exercise),
       sat(Exercise =< Healthy),
       sat(Study + Sick),
       sat(~Rain),
       sat(Study * ( Gym + Coffee)),
       sat(Rain + (Exercise * Study)),
       sat(Healthy =< (Happy + Fit)).

As an answer, we get:

    School = Study, Study = Exercise, Exercise = Healthy, Healthy = 1,
    Rain = 0,
    sat(Sick=:=Sick),
    sat(Gym=\=Gym*Coffee#Coffee),
    sat(Happy=\=Happy*Fit#Fit).

Since CLP(B) is complete, these are all the consequences that can be derived from the initial knowledge. Note that for example `Gym = 1` is consistent with the initial assumptions, it just doesn't follow from them.

To obtain ground solutions, you can use labeling/1 on the remaining free variables, showing all possible ways in which truth values can be assigned to them.

Very interesting! Do you know how is the constraint solver library implemented? Does it use a different general implementation than the regular prolog statements?

There are several different ways to implement such solvers on top of Prolog.

One way is to simply extend the Prolog engine to handle such constraints natively. Many basic constraints are implemented in this way. In fact, you can regard even (=)/2, i.e., unification, as one such constraint, and all Prolog systems implement it, typically as one of their virtual machine instructions. The same method naturally extends to other constraints like freeze/2 and (in)/2, which are often implemented natively. See the system descriptions of GNU Prolog, as one example for a system that handles the CLP(FD) constraint (in)/2 natively.

For application programmers, Prolog systems typically provide an interface in the form of attributed variables are metastructures, so that any programmer can implement a custom constraint solver on top of Prolog by attaching attributes to variables. For example, in SICStus Prolog, there is a hook called verify_attributes/3, and you can provide a custom user-defined specification that handles your own constraints.

In practice, the implementation of constraint solvers on top of Prolog typically involves a combination of both approaches, with some low-level constraints implemented natively (i.e., as part of the engine), and some higher-level constraints implemented via the general interface on the Prolog level.

There are of course also other ways to do it, such as writing a Prolog meta-interpreter that interprets your code as if the Prolog engine supported such extensions. This is likely among the slower ways to provide such extensions, while a native implementation is among the fastest, and using general interface predicates will likely be somewhere between these extremes.

You might be interested in ACE: http://attempto.ifi.uzh.ch/site/

Thank you!

Used ANTLR for something similar. Quick googling yields: http://stackoverflow.com/questions/24935419/antlr-4-taking-d...

Further reading, you seem to do quite a bit more.

> I came across this paragraph while studying "Discrete Mathematics and It's Applications"; therefore, I got inspired to automate this task using computers.

Congrats, going from reading to an idea to a project to a public repo!

Awesome! I'll research about that. Thank you!

"Divide and conquer recursive implementation" - so is that backward-chaining inference then? Or something different?

https://en.wikipedia.org/wiki/Backward_chaining

The validator part of the program almost uses backward-chaining implementation. The "list" of goals" for the backward-chaining is created by the definer part of the program which uses a recursive function.

Concerning `(I study) OR (I'm sick)` in readme example am i correct in thinking that that OR is a XOR here?

All ORs are inclusive disjunction.

Reinventing Prolog?

Similar but prolog is much broader and more general purpose of course.

I was confused because the source file was referred to as "the executable" and did not have a conventional .py extension.

NLI is a clickable python file. When you click on it you enter a command line interface.

Thank you. I don't usually launch Python files (or programs in general) by clicking on them, so it did not occur to me.

Reply on news.ycombinator.com