7 ms·

Show HN: Automatically interpret and validate nested natural logic arguments

53 points by parhamp 9y ago

brudgers 9y ago
I was confused because the source file was referred to as "the executable" and did not have a conventional .py extension.
- parhamp 9y ago
  NLI is a clickable python file. When you click on it you enter a command line interface.
  - brudgers 9y ago
    Thank you. I don't usually launch Python files (or programs in general) by clicking on them, so it did not occur to me.
deleted 9y ago
[deleted]
tunesmith 9y ago
You might be interested in ACE: http://attempto.ifi.uzh.ch/site/ http://attempto.ifi.uzh.ch/site/
- parhamp 9y ago
  Thank you!
jxy 9y ago
Reinventing Prolog?
- parhamp 9y ago
  Similar but prolog is much broader and more general purpose of course.
ominous 9y ago
Used ANTLR for something similar. Quick googling yields: http://stackoverflow.com/questions/24935419/antlr-4-taking-decisions-from-a-parse-tree 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!
- parhamp 9y ago
  Awesome! I'll research about that. Thank you!
zmonx 9y ago
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.
- parhamp 9y ago
  That is a very useful comparison. Thank you.
  - zmonx 9y ago
    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-Introduction.html#CLPB-Introduction 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.
barrystaes 9y ago
Concerning `(I study) OR (I'm sick)` in readme example am i correct in thinking that that OR is a XOR here?
- parhamp 9y ago
  All ORs are inclusive disjunction.
jimsmart 9y ago
"Divide and conquer recursive implementation" - so is that backward-chaining inference then? Or something different? https://en.wikipedia.org/wiki/Backward_chaining https://en.wikipedia.org/wiki/Backward_chaining
- parhamp 9y ago
  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.

53 points by parhamp 9y ago

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

parhamp 9y ago
NLI is a clickable python file. When you click on it you enter a command line interface.
- brudgers 9y ago
  Thank you. I don't usually launch Python files (or programs in general) by clicking on them, so it did not occur to me.

deleted 9y ago

[deleted]

tunesmith 9y ago

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

parhamp 9y ago
Thank you!

jxy 9y ago

Reinventing Prolog?

parhamp 9y ago
Similar but prolog is much broader and more general purpose of course.

ominous 9y ago

Used ANTLR for something similar. Quick googling yields: http://stackoverflow.com/questions/24935419/antlr-4-taking-decisions-from-a-parse-tree 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!

parhamp 9y ago
Awesome! I'll research about that. Thank you!

zmonx 9y ago

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.

parhamp 9y ago
That is a very useful comparison. Thank you.
- zmonx 9y ago
  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-Introduction.html#CLPB-Introduction 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.

barrystaes 9y ago

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

parhamp 9y ago
All ORs are inclusive disjunction.

jimsmart 9y ago

"Divide and conquer recursive implementation" - so is that backward-chaining inference then? Or something different? https://en.wikipedia.org/wiki/Backward_chaining https://en.wikipedia.org/wiki/Backward_chaining

parhamp 9y ago
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.