I'm really interested in this.

I follow the field fairly closely, I've implemented an open language question answering system myself, as well as re-implemented parts of the Watson QA system form their papers. I've built NN based entailment systems, and I built a text summarisation system which still wins benchmark competitions 15 years after it was built. Also, I use Superset (AirBNB's opensource Tableau competitor) daily.

Basically, I'm not a complete neophyte in this and related fields.

But I don't have a clue what this system does.

I know Prolog and some about CCG. But the it talks about Tableau and I'm completely lost.

Can someone please explain?

This is the tableau they're talking about: https://en.wikipedia.org/wiki/Method_of_analytic_tableaux

Ha. Thanks.

I should have read the paper, not just jumped to the Github link.

Search for the author's home page, which has a link to his Ph.D. dissertation. The thesis provides a lot more background material and examples.

No need to brag, buddy.

It didn't come across as bragging to me; it provided useful context for the question. For a naive reader like me, it demonstrated to me that someone much more experienced in this area than me was confused by it. For a reader capable of answering their question, it provided a baseline of their knowledge, which is useful for determining what level of detail to go into when answering.

I'm not sure admitting my complete confusion is bragging. I apologize if it came across like that.

There wasn't a single comment on this post, despite it getting lots of upvotes. I assumed I was missing something, but I felt like my "WTF" needed some context.

It's ok to brag on Hacker News.

Their brag helped me to understand what ca I learn.

How does this differ from what prolog does?

Prolog is a programming language, and this isn't a programming language. Prolog doesn't process natural language by itself. Prolog isn't a tableau-based theorem prover.

This project is a natural-language-processing, tableau-based-theorem-proving application implemented in the Prolog programming language.

I mean how does the pruning constraint tree search applied in prolog implementations differ from the tableaux method

After some research, the tableaux method seems to require full coverage, which would only converge with the search tree if all conditions have to be exhausted.