Recently, I've tried a kind of interactive expert system by using ccg2lambda. If we input some premises and a goal, the system produce some subgoals, and I want to transform that subgoals to readable sentences for human, and then have tried to prove it interactively.
Originally it was a system presented at an event called NLP2021, but the source code is not yet available, so I am trying to reproduce it personally.
@swan314 Many years ago there existed a system called Proverb, which was very good at
putting together a verbalisation independent on what the actual proof format was (ND, Resolution, etc...).
At least they di extremely well on the Dreadsbury Mansion Problem. Let me see if I can find a reference somewhere.
@swan314 Thank you Google Scholar:
The social network of the future: No ads, no corporate surveillance, ethical design, and decentralization! Own your data with Mastodon!